BOOOKS
Conversation
Hit me up if you ever want talk verified compilation (Appel et al. also on my bookshelf)
1
1
Oh lovely!
Trying to start getting my head around it. I'm wanting to try out type preserving compilation for Pikelet, at least up to ANF and Closure Conversion, using some of et al.'s work on doing it for dependent types!
2
2
Let me know how it goes! Would be interesting to see an implementation and where the practical issues start to come up.
1
2
One thing I'm curious about is how well ANF plays with effectful code... I want to eventually do useful stuff with Pikelet, but I'm unsure if you need CPS for that... ie. because in ANF the order of control flow is not explicit? github.com/pikelet-lang/p
Ping whose expertise here I defer to: Liam, do you have thoughts here given experience with cogent or otherwise?
1
In Cogent effects are all modelled with linear types, and because even linear types are preserved by ANF, effects aren't a concern on the cogent end because as far as we're concerned it's still all pure functions.
1
1
Show replies
The type preservation proof relies on absence of effects, and this is also true of my CPS translation. To combine effects and dependent types, you need a way to isolate effects from certain dependencies. My colleague has done some work on this sites.google.com/site/youyoucon
1
2
She develops a CPS translation for dependent type with control effects. Her work imposes a judgmental distinction between pure and impure terms. Impure cannot use certain patterns of dependencies, and are translated differently than pure terms.
1