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
2
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
If you have a reified effect system (for example a monad or some types of algebraic effects) then the control flow that remains abstract in ANF isn't that important to the effectful computations you're composing together, so perhaps CPS doesn't buy you much over ANF there.
1
1
Cool, I was definitely hoping to have one of those. And also linear types in the McBride/Atkey style.
But the McBride/Atkey ones seem to be more coeffecty than effecty... so perhaps it's not as applicable... interested to know what you mean by 'modelling effects with linear types;
1
I should be more precise here by saying that cogent actually has uniqueness types not linear types
1