Conversation

daniel gratzer
@dannygratzer
You need annotations for eta-expansion in read-back. Depending on the type you will quote [x] differently (for booleans its a normal form, but not for functions!). So you want type information when quoting most terms.
1
1
daniel gratzer
@dannygratzer
The annotations on neutrals come from implementing "do_ap" and similar things. Neutrals are not quoted in a type-directed fashion and so some components of neutrals must be normals (the argument in Ap for instance). See the neutral case of do_ap for why we annotate neutrals
1
1
daniel gratzer
@dannygratzer
They don't seem to include eta in Mini-TT (unsure if this is a compromise to handle non-termination slightly better or just for simplicity) so nothing in quotation is type-directed.
1
daniel gratzer
@dannygratzer
No problem! Well, there are a couple advantages, the biggest for the user is that more "obviously equal things" are judged equal by the system. For instance, \x. 0 + x = \x. x. But it also captures the universal properties for certain types.
1
1
daniel gratzer
@dannygratzer
I should be more careful with my examples.. that one holds in systems without eta for pi I expect. But composition with identity being the identity is an example of eta :)
1
1
daniel gratzer
@dannygratzer
Replying to
@brendanzab
I guess I was worried about how you would get the eta-long form for [loop = loop] where [loop : A -> B]. Just termination check things before you evaluate them I guess if you don't want your evaler to loop.
1
1