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
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
The logical endpoint for a) is machine code evaluation. There's a (rarely mentioned) PhD thesis for conversion checking with machine code evaluation by Dirk Kleeblatt.
2
3
I'm guessing you mean "On a Strongly Normalizing STG Machine: With an Application to Dependent Type Checking" by Dirk Kleeblatt? scholar.google.com/scholar?cluste - I also came across "A Compiled Implementation of Strong Reduction" which looked neat: scholar.google.com/scholar?cluste
1
I was planning on doing something similar in Pikelet, but lowering in a type-preserving way using something similar to William Bowman's work. I'm also interested in allowing uses to embed fragments of lower level IRs in higher level code, kinda like inline-assembly.
1
But the problem of metavariables is something I had not considered, because I've not yet started messing around with that kind of solving yet! So thanks for bringing it to my attention! :)