Hey, is there a place I can go to to read about the ideas behind the 'gluing' stuff that you do in smalltt? Ie. you seem to split the semantic domain into 'values' and 'glued' terms. I'm guessing this is for unifying metavariables?
Conversation
"Gluing" in this sense is AFAIK my invention, I'll do writeup and likely publication at some point. I can give quick rundown here. Dep. elaboration has two core tasks: a) deciding conversion during checking b) solving metas.
2
3
By 'solving metas' do you mean filling in holes? I've always kinda got confused by the difference (if there is one) between holes and metavariables. 🤔
1
1
Most metas are tied to holes, and solving them amounts to filling holes, but there can be free-floating metas. E.g. when we infer a meta as type for something which should be a function, we need to refine it to a function going from one fresh non-hole-tied meta to another.
1
3
Thanks for the great explanations btw, slowly getting my head around it all! Also wondering if there is any good reading on metavariable solving without the gluing stuff you do - might help me understand the changes you made better.
1
1
I've found it hard to jump from simple bidirectional implementations like LambdaPi, Pie, and nbe-for-mltt to stuff that solves metas. It's something I'd really like in Pikelet.