there’s this super deep relationship between heterogeneous substitution, normalization by evaluation, pattern unification, &c., and much of it depends on the kind of dependently-typed language you’re designing; & the design space is vast & underdescribed.
Conversation
Ohh, this is all really helpful! Might take me a while to unpack - I haven't gone as deep as you, but it rings many bells from looking at 's elaboration-zoo a while back. It's super handy to have some of these problems stated explicitly in this way though!
2
2
Yeah for sure - at the moment I've been mainly cargo-culting off the elaboration-zoo, but it's sometimes hard to understand _why_ certain choices where made, and what the other options are. I also find papers on unification rather hard to break the ice on. 😬
3
1
I always value the time others have put into this stuff, and want to learn as much as possible from those struggles, even if there's only so much that I can get my head around at a time! So your experience is super valuable to me! 🙂
1
3
1
3
additionally, we are told that the IRC crowd miss you. won't try to hard-sell it, but thought we'd mention.
1
1
Aww thanks - bit tired now tbh - I'll try to get it working - if not today, maybe tomorrow! Would be handy to have that Matrix IRC bridge at any rate. 🙂
1
1
good luck :)
1