robrix
commented
5 years ago I think this is going to be necessary:
- Unification solves metavariables with
Values. Values can be quoted back toCoreterms; however…- Quoted
Values are annotated with(), not with types; and we can’t synthesize types back. So I think we can’t substitute variables in type-annotated terms, which means that elaboration has to produce()-annotated terms, and therefore that we won’t have types informing erasure at every level.
If we represent type abstractions/applications in a separate piece of syntax, and possibly annotate Value.Lam with its Plicity, we should be able to quote back to Explicit :+: Core and therefore do substitution in elaborated terms.
An alternative might be to make elaboration evaluate the core term to a Value and then substitute metavariables out within that.
We’ve had good results with passes transforming one sum of terms into another, e.g. desugaring and elaboration. We could do the same thing for erasable syntax, which would include types and eventually explicit type abstractions (cf #73) & applications (cf #74). We’d generate type abstractions for implicits, too, and then stripping the erasable syntax off would just leave us with a core lambda calculus consisting of variables, abstractions, applications, and possibly other primitives (cf #45).
We might also want to define evaluation as occurring on erased terms.
cf #19 re: performing type erasure