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
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
Yeah, anything that I use will have to extend up to CoC (with or without totality checking). I'm guessing equirecursive types at that level would still be beyond our reach?
Yes, also because inductive types and recursive types aren't quite the same thing (though it's only obvious in PFPL's presentation). I confess the soundness proofs were Cai's work, and I don't understand them well enough to speculate on extensions.
2
1
Show replies