Add `letrec` terms

[Kmeakin]

Adds new letrec term. Type-checking is surprisingly easy:

• Insert a fresh type variable for each definition
• Check each definition's pattern against its type variable
• Check each definition's RHS against its type variable

The hard part is evaluation. I think this would require lazy evaluation. At the moment any letrec definitions just evaluate to #error, so you can check that letrec type-checks, but can't run it

Todos

• Evaluating letrec definitions
• Generating fresh names when distilling letrec definitions
• Currently, you must annotate each recursive definition if it is used recursively, otherwise you will get an error about trying to apply an argument to a metavariable. I think postponing would fix this?
• Recursive top-level def items. Will leave for a later PR
• Check that letrec definitions are safe to evaluate. I believe we can use the algorithm from A Practical Mode System for Recursive Definitions. Will leave for a later PR
• Syntax bikeshedding
  • Should letrec be spelled letrec (as in Scheme) or let rec (as in ML)?
  • I'd like each definition to be separated by ;, but I cannot figure out how to do so without LALRPOP complaining about ambiguity, so for now the separator is ,

[brendanzab]

Oh wow, neat. Do you have any ideas about how this might interact with termination checking? IIUC some type theories have a type for “well founded recursion”, but this might not be the best for an actual implementation?

Syntax wise, I think I like let rec actually - unsure about a nice way to handle multiple mutually recursive bindings though. I do also wonder also if it would be better (in Fathom) to limit recursive bindings to the top level.

I wonder if we can find binary formats that might exercise this feature? Might be useful to test it on some real world stuff.

I’m unsure about merging this right now, but I really appreciate the exploration! I’ve found recursive bindings to a bit intimidating, so this stuff is very helpful! Takes a bit to understand and synthesise some of the research, and turn it into an implementation.

[Kmeakin]

Oh wow, neat. Do you have any ideas about how this might interact with termination checking? IIUC some type theories have a type for “well founded recursion”, but this might not be the best for an actual implementation?

Sometime down the line we could add recursion checking, but I don't think its a priority since our type theory is already inconsistent (we have Type : Type)

[Kmeakin]

I do also wonder also if it would be better (in Fathom) to limit recursive bindings to the top level.

I decided to do local recursive binding first, because it allows me to test out the typechecking rules without needing to implement lazy evaluation: just return #error when evaluation defs in letrec. Adding recursive def items should be simple: just adjust the type checking rules and make def items lazy

[brendanzab]

I don't think its a priority since our type theory is already inconsistent (we have Type : Type)

Yeah I had been planning to remove this at some point – just hadn’t got around to it yet! See #316 😓