Now they use ANF because I managed to convince Zoe (not Andrew though) to look into it. They've been published cause y'all love a massive Coq proof but not the fundamental research that enables it.
Conversation
Just wanna say, thanks for all the effort on the ANF front, wrt. compiling dependent types. You and have me pretty curious about it and I'm thankful for your efforts, in spite of the setbacks. Really hoping to see this paper eventually!
1
6
:) You can read Paulette's thesis. We might go ahead and post an arxiv version. This submission isn't dead in the water yet.. all B's isn't the worst set of reviews I've come back from.
5
8
Will do! I'm wanting to make an ANF compiler for my dependently typed experiments, so I'll go to Paulette's first – I was originally looking at your thesis. I'm pretty slow at understanding this stuff and I find implementing it from a nice description is the best way I learn. 😅
2
1
You should look at Paulette's; she's scaled it up to handle if, and recursion via eliminators. Even have a sketch of how to handle match and fix, but preserving the guard condition is on you.
2
3
Dumb question, could you preserve guard conditions by elaborating to eliminators (ala Goguen et al) before compiling?
1
Yeah, but I would really worry about performance. The eliminators you'd generate could be absurd, and I FEEL like it would be easier to compile and optimize match + fix.
I think disagrees about having match+fix in the core and I need to investigate.
2
2
I hope I'm wrong because both sized types and the guard condition are a nightmare, and eliminators are so easy.
1
3
I really hope I don't need match in my core 😔
1
what do you use?
1
I was hoping to elaborate pattern matching to eliminators, but I keep hearing claims that it's bad idea for performance, and then others claiming it's not bad, if you do it right. I don't really know either way, but aesthetically eliminators seem nicer?
I agree they're aesthetically nicer, and it's easier to preserve typing for them. Maybe I'm wrong about the performance concerns. IIRC, Lean was using them, and they pay a lot of attention to performance.
1
1
I think Lean 4 moved away from eliminators, but yeah I still hope there is a way to do it ok. I still don't know if that is more an issue with the performance of their interpreter though, which uses locally nameless+optimisations rather than NbE…
1
1
Show replies
For _one_ of my languages I want to support targets which might have a non-dependent match construct (like Rust). So it might be better to preserve pattern matching in the core in that case, but I'm not sure.
1
1
So the interpretation cost isn't what I'm worried about (I hope to be able to JIT during type checking o.0), but the size of the data type + eliminator generated to get the eliminator the corresponds to a small pattern match+fix.
1
1
Show replies