old thread was getting a bit long: Which type annotations are you referring to? For normal forms?
Conversation
Replying to
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. 
Replying to
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
Show replies