Open Kmeakin opened 1 year ago
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 😓
Adds new
letrec
term. Type-checking is surprisingly easy: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 thatletrec
type-checks, but can't run itTodos
def
items. Will leave for a later PRletrec
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 PRletrec
be spelledletrec
(as in Scheme) orlet rec
(as in ML)?;
, but I cannot figure out how to do so without LALRPOP complaining about ambiguity, so for now the separator is,