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
Replying to
"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
For a), we just need a fast evaluator for open functional programs, and we can borrow standard evaluators with minor modifications. The nbe evaluator is pretty close to GHC's eval-apply STG machine, difference is less optimizations and the presence of netural values.
1
1
Show replies