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
For b) we need an evaluator which is also efficient, but with the property that we can quote/readback terms from it which are sufficiently "high quality" as code for metavariable solutions.
1
In Agda/Coq, quality of meta solutions is largely ignored, even though in a typical dependent program the size of meta solutions can easily dwarf programmer input size, in the elaboration output. So we get elab output overwhelmingly consisting of extremely slow or bloated code.
1
1
In smaltt, the values for b) are called "Val", and the "vEval" evaluator has the property that it never unfolds definitions from top scope, including metas, thereby keeping quoted meta solutions often asymptotically smaller than in Coq/Agda.
1
1
So in smalltt "quality" is equated with "small size" in the "Val" evaluator, which is pretty dumb but a good start. However, a key point is that we don't want to run the a) machine and the b) machine independently, because lots of computation can be shared.
1
1
So we instead "glue" the b) machine onto the a) machine, such that a) drives the overall computation, but lazily computes b) values in way such that common redexes aren't duplicated. So "Glued" evaluates both a) and (lazily) b), while "Val" only evaluates b).
1
1
In theory, you could get different glued setups of three or more machines, each specialized for different purposes, but constant overheads increase. My choice was to have just two machines, and I use b) both for fast approximate conversion checking and generating meta solutions.
1
1
Replying to
Bonjour please find the unroll here: Thread by : " "Gluing" in this sense is AFAIK my invention, I'll do writeup and likely publication at some point. I can gi […]" threadreaderapp.com/thread/1080841
Enjoy :) 🤖
1
3