old thread was getting a bit long: Which type annotations are you referring to? For normal forms?
Conversation
Quote Tweet
Replying to @dannygratzer @franciscof and 2 others
Currently trying to add the labelled sums from the Mini-TT paper to the language! Just curious, why do you need the type annotations in the values? They seem to manage without it in the Mini-TT paper. 
1
1
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
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
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
Ah yes, see [6.8 Variations] where they touch on this.
1
1
Cheers for the assistance, really helps! What would the advantage of having eta-expension be?
1
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
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
Replying to
Is this eta? github.com/jozefg/nbe-for
I'm guessing this is why you don't look at whether `f` is a lambda?
Replying to
Yep exactly. Same with sigma below, you just convert everything to its eta long form.
1
You mentioned that this might interact poorly with non-termination. Why might that be, and could it lead me astray given I want a more Idrisy style of language, mixing total and unsure-if total stuff?
1
Show replies