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
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
(At some point I realized I was way out of my depth, and started working on a nominally typed language instead, at the time conceived of as "warmup". Which it has since, uh, outgrown.)
1
2
haha! Pikelet was meant to be a 'warmup' too!