Ohh, nifty!
Conversation
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?
1
1
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
Harper's "practical foundations" book? I deploy that acronym as casually as TAPL or ATTAPL ;-)
1
1
Haha! Yeah, I've yet to aquire that one, I must confess!