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.
Conversation
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
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
E.g. if you look at what Coq's Program generates.. you wouldn't want to run that code. And Coq pulls some tricks to extract the code you wrote, not the generated code, to OCaml.
1
When does the size-blowup occur? Is that when you unfold definitions? If that's the case I'm wondering if something like glued eval (in smalltt and sixty) could help – where you 'remember' the original neutral, which lets you keep things small in the right places.
2
It's not just in unfolding, but even the generated function definition. I should come up with a good example to study when we start working on recursion properly.
1
1
Ahh, cool. Would be interested to see some of these issues more concretely! And apologies for my ignorance! 😅
No worries. It's literally my job to think about these things and try to communicate them, and that's the fun part of my job.
1
2
Yeah I love trying to communicate this stuff too! Especially if it was originally presented in a confusing way. Alas I never really get around to writing this stuff down… for all the faults/issues with academic papers, I'm so thankful for the of the paper trail you all produce!
2