add explicit substitutions

[jonsterling]

let's add a new constructor for explicit substitutions! And we can also add some operations to wring out the substitutions.

@freebroccolo

[jozefg]

Oh nice, very Twelf-y :)

[jonsterling]

@jozefg Yeah, was chatting with Darin about it last night and he finally got it through my thick head what they did! :smile: Based on some of the Pfenning & Pientka stuff, I had got the mistaken impression that explicit substitutions have anything at all to do with meta-variables, but in fact they are totally orthogonal. It's just this cute left kan extension trick for suspended bind that you see all the time in Haskell...

I think it would be cool to add them, since we can then implement some nice abstract machine stuff pretty easily.

[jozefg]

Sounds cool! I'm curious how this plays out!

[ghost]

Sounds like a good plan. Here are some links that may be useful for implementation purposes:

• A basic lambda calculus with explicit substitutions in idris, already mentioned this one: https://github.com/freebroccolo/container-calculus/blob/master/Main.idr#L91-L121
• A Krivine machine implementation with explicit substitutions. This one uses a defunctionalized representation for substitutions (see Ctx and Kind). It is a little bit gnarly but seems pretty fast:

https://github.com/freebroccolo/substitutions/blob/master/src/Krivine.ml#L28-L58 and https://github.com/freebroccolo/substitutions/blob/master/src/Krivine.ml#L341-L388

• A partial implementation of the K-sigma machine (described here: https://ifl2014.github.io/submissions/ifl2014_submission_17.pdf). The idea is that it uses a zipper based approach on top of the Krivine machine to handle full normalization, IIRC. Been awhile since I looked at it but I remember thinking it was a nice idea.

https://github.com/freebroccolo/K-sigma-machine/blob/master/src/Machine.ml

[ghost]

I should also mention that the defunctionalized representation for these substitutions is a bit like the order-preserving embeddings (OPE) stuff that Chapman and co use in some of their papers.

[jonsterling]

Getting closer to the point where I will almost certainly want to have these. At this point, there is basically one question remaining, which is how to decide alpha equivalence for explicit substitution terms—this is clearly possible, but it may be a bit difficult to define (the coend induces a non-discrete equality for closures). I guess one dumb way to define it would be to just force the closure when we get to one.

[ghost]

I think Abel gives an algorithm in a few places. Maybe in his habilitation thesis.

One approach that I think might work would be to compute and store the strengthening of the head term and environment (deduped) in the closure as soon as the closure is created. This way, you could quickly check that the lengths of the environments for the two closures match before doing anything else. If they match, then you would check that one is a permutation of the other. After that, it should be straightforward.