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.

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)

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

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 😓