Support for capturing substitution

[TOTBWF]

When dealing with program refinement (or really any domain with the notion of a meta-variable), capturing substitution is required. For example, consider the language and judgements below.

e ::= x (variables)
        | \x.e (abstraction)
        | e e (application)
        | ?x (meta-variable)
        | ?x.e (hole)
        | ?x ~ e.e (guess)


                     pure e = b           pure e1 = l    pure e2 = r
-----------------  ------------------     -----------------------------   -------------------
pure x = true       pure \x.e = b          pure e1 e2 = l ^ r                pure ?x = true


--------------------     -----------------------------
pure ?x.e = false        pure ?x ~ e1.e2 = false

           pure e1
--------------------------------        
solve ?x ~ e1.e2 = [e1/x]e2

Informally speaking, you can solve a hole if and only if the guess does not contain holes itself. However, the meta-variable substitution must capture variables. As a concrete example:
solve ?x ~ y. \y.?x = \y.y.

As it currently stands, the only way to implement capturing substitutions (and metavariables) that I have come upon is pretty hacky, and any other way would require support in unbound itself.

In my mind, there are 2 options:

1. Add substCapturing :: AlphaCtx -> Name b -> b -> a -> a as a method on Subst
2. Add support for meta-variables directly

Seeing as the only reasonable use that I can think of for substCapturing would be for implementing
meta-variables, I think that option 2 would be the best approach, but it has its downsides as well.

Either way, I can write up a PR to implement this if it seems like something that would be a useful addition.

[lambdageek]

@TOTBWF I don't completely follow your example (maybe github isn't the best communication medium - do you have a pointer to a paper with an example language that I can take a look at. Either something from the literature or maybe a draft of something you're working on?)

However, it sounds to me like the notion of substitution that you want for meta-variables is not "plain vanilla capture-avoiding substitution" which is largely what Subst is about.

I do agree that it would be nice if unbound-generics could help with boilerplate of other notions of substitution. So I would propose another path: instead of enriching Subst with new methods, or adding a new sort of variable to the core of unbound-generics, let's look for reusable pieces of Subst that we can abstract out to give us building blocks for writing new substitution algorithms.

Does that make sense?

[TOTBWF]

I totally agree with you on abstracting out the more general notion of substitution out of Subst. As for literature, Erwin Brady's paper on Idris Elaboration should be a good example (especially page 16 and beyond). Other examples would be any other tactic based proof/program refinement systems.