Elaborator, holes, etc.!

[jonsterling]

I want to have an elaborator that supports interactive development by refinement, using holes. Eventually we can do more fancy things like unification and top-level implicit arguments (in Epigram style) too (but later!).

One thing I have been wondering is whether it will be possible to keep the core term language completely ignorant of the user-supplied names, but somehow keep track of these in the elaboration environment.

[jonsterling]

I want to write down a few thoughts and clarifications about elaboration.

It is tempting to just add a "hole" constructor to the core language, but as Conor McBride observed so many years ago, this is a really catastrophically bad idea (it is probably responsible from some strange behavior I have observed in cubicaltt 😃 ) The problem is that in this naive version of holes, valid proof refinement steps will not preserve the well-typedness of a piece of code; for instance, what is the meaning of (\x. ???) N? In the naive version, this reduces to N, but the hole actually needs to express a dependency on x.

The right way to do holes is to have a constructor in the core language that takes the name of a metavariable (which lives in the "elaboration context') together with an explicit substitution from the metavariable's native context to the "current" context. Obviously this is not the sort of thing that a user would be able to (or even should be able to!) write down, and that is by design.

Instead, this should be dealt with by the elaborator from the high-level language. In other words, holes are a construct of the source language, and metavariables+spines are the corresponding construct in the core language.

[favonia]

I would like to add spines are the right way to handle neutral terms! Right now RedPRL's auto tactic focuses on the outermost connective, which is wrong IMO.

[jonsterling]

As a quick remark, let mention something that I realized today, so I don't forget it.

@cangiuli and I were worried that the Kan version of extension types would be basically useless, since you have to introduce and instantiate them all at once (in all their dimensions); so it would be very bureaucratic to project a line from a square, etc., and that was just what we were trying to avoid anyway.

What I realized today is that since we really only presuppose that things are pretypes (not necessarily kan), partial applications actually make sense: their type is not kan, but I think it doesn't matter. In the core language, I will most likely still require everything to be all-at-once, but in the elaborator it should not be hard for me to enable partial application. In my sketch of the development calculus, I have already unleashed partial abstraction.

[jonsterling]

As an update, i have implemented a variation on Idris's development calculus, and written an example of how to elaborate user-holes/question marks in the Idris style.

[jonsterling]

I'm going to close ticket this because the elaborator is officially Unleashed 😎 Obviously it's not done, but further tasks and bugs should be reported separately.