Diving into type systems

https://discourse.elm-lang.org/t/prerequisite-knowledge-for-building-elms-type-system/10729

Evan and Rupert from the Elm community gave me some pointers when I asked about what I'd need to learn to build Elm's type system. This should serve as sufficient reading when I go to prototype HOBL for a particular domain.

I also want to check out the implementation behind Nickel, because its code (contracts) are picked up by the LSP to create additional validation (rather than having to learn a linting framework). https://www.tweag.io/blog/2024-05-16-nickel-programmable-lsp/

Finally, I'd like to understand how I'd choose between Dhall and Nickel. I think it comes down to which of the two I want more:

  1. General recursion and good type inference (gradual typing)
  2. No side effects and Static functional equivalence guarantees. This prevents XSS which is actually pretty cool.
    I'd like to play around with Dhall as a config language (say for representing lazyvim's config). In particular, I'd like to understand what recursion can do that loops (or known-terminating constructs) cannot.