I really liked your presentation, ”Compilation as Multi Language Semantics“! youtube.com/watch?v=RfVhUP
The ‘lazy compilation‘ reminded me of the normalisation-by-evaluation that's often used for compile time interpreters in dependent type system implementations…
Conversation
Almost like NbE is a bit like 'lazy closure conversion + partial evaluation' perhaps…?
I'm pretty bad at theory stuff, so it's likely I'm wrong about this, misunderstanding, or that you are already aware! Just thought I'd mention it in case it's of any use! 😅
1
1
3
Nope your not wrong; it does seem related. I’m not sure exactly how, but I have ’s dissertation on my reading list.
1
1
Oooh, exciting! Glad I'm not wildly off base, and excited to see what happens here. I think Coq has a way of falling down to ZAM in some cases? It's all seemed rather reminiscint of JIT, though with the added complication of having to support readback for conversion checking… 🤔
Hopefully will have more progress soon. Won’t be looking at its connections to dependent types for a while though.
1
1
Yeah, that's fair enough! Still exciting that the possibilities are there though. 😊
1