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!
I don't really understand equirecusive types yet though either!
1
Yeah I mentioned because my sense at the time was that equirecursive would be a nicer fit with structural types (fewer cases of "actually the same type, just encoded differently"); dunno (+ can't remember), now, if that was a good idea or not...
2
2
Show replies
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
The paper extends equirecursion up to FOmega, based on TAPL’s framework, but decidability is restricted to a fragment. A reviewer suggested us this language would be best used as a target language for elaboration, but the source language would be still an open question...
2
2
Show replies