Mmmm… iso-recursive types… 😋
Conversation
I'm guessing one can add in these folds and unfolds during desugaring or elaboration, without needing to expose them in the surface syntax? 🤔
1
Ohh, nifty!
1
1
What to do though, for structural type definitions… 🤔?
1
1
back when I was thinking about similar things this paper seemed interesting: ps.informatik.uni-tuebingen.de/research/funct [I can't remember whether I "read" it at the time without understanding much, or didn't]
cc :)
1
2
Yeah, I'll check that one out! I was trying to stay with isorecursive types though!
2
1
Before you look at that paper, aren’t you asking for equirecursive types (also in TAPL), like “I want all features of equi- but implemented on iso-“?
2
Heh, yeah, I probably am, I just don't know it! 😅
Might have another dive into TaPL again as well. Feel like I'm learning much more this time around (as opposed to several years ago!)
1