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. 😅
Conversation
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?
2
1
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
You might need to double check that though. But I was pretty surprised at the choice of locally nameless, given how fast NbE (using indices and levels) seems to be. And unsure if this interacts with stuff like eliminators. They might have their reasons though.