Effects: Pikelet should actually be useful!

[brendanzab]

At the moment Pikelet doe not do anything useful. In order to be more useful, we probably need some form of way to perform effects.

Initially we could use an Io : Type -> Type wrapper type for this.

Eventually I would like us to move to something like an algebraic effect system. The limiting factor for this would be that it must be zero-cost. ie. We need to make sure that any reification of effects can be erased or partially evaluated away at compile time in a reliable way. This should result in codegen identical to if one had written code in an imperative language.

Resources

yallop/effects-bibliography has lots of links.

Here are some papers that are more specifically about integrating dependent types and effects:

• D. Ahman, Handling Fibred Algebraic Effects. (Paper, Agda code)
• D. Ahman, N. Ghani, G. Plotkin. Dependent Types and Fibred Computational Effects. (Paper)
• Y. Cong, K. Asai, Handling Delimited Continuations with Dependent Types (Paper, Video)
• C. McBride. Do be do be do. (Paper)
• E. Miquey. A Classical Sequent Calculus with Dependent Types (Paper)
• F. Nielson, H. R. Nielson. Type and Effect Systems. (Paper)
• P.-M. Pédrot. Taming Effects in a Dependent World (Slides)
• P.-M. Pédrot, N. Tabareau. Failure is Not an Option: An Exceptional Type Theory. (Paper, Slides)
• A. Rossberg. 1ML with Special Effects: F-ing Generativity Polymorphism. (Paper)

[brendanzab]

As Pikelet is dependently typed, we should probably think about how effects fit in to evaluation. Initially we could treat any effectful computation as 'stuck'. There is work being done though on trying to integrate effects into dependent type theory, under the names 'Observational Type theory' and 'Cubical Type Theory'. This is still very much ongoing research though, so it might be better to be conservative for now.

Some dependently typed languages that currently integrate effects are F* and Idris. Perhaps we could get some inspiration from there?

[clayrat]

I think OTT/HoTT/CTT aren't so much about effects, but rather about exploring the nature of equality, allowing to do proofs on functions (funext is provable in those), codata, real numbers and other tricky/infinite structures. For effects you need to look at CBPV/sequent calculus and modal types.

[clayrat]

Here are a couple of recent CBPV-style systems for dependent effects:

• https://arxiv.org/abs/1706.07997 Vakar, "In Search of Effectful Dependent Types"
• https://arxiv.org/abs/1710.02594 Ahman, "Fibred Computational Effects"
  • https://github.com/danelahman/POPL18 partial Agda formalization

[clayrat]

https://github.com/OPLSS/introduction-to-algebraic-effects-and-handlers https://arxiv.org/abs/1807.05923 Bauer, "What is algebraic about algebraic effects and handlers?"

[brendanzab]

Bunch of interesting papers here: https://www.pédrot.fr/publications.html (thanks @pythonesque, via twitter)

[brendanzab]

Some other thoughts:

• Should generative modules be treated as effectful?
• Should module loading be effectful (but in the static phase)?
• Should dynamic memory allocation be treated as effectful?
• Laziness looks suspiciously like mutation/effects... is call-by-value coeffectful? 🤔

[typesanitizer]

Since you're collecting references here, might as well save a pointer to Yallop's bibliography which can serve as a 1-stop shop for all cool papers related to effects :)

https://github.com/yallop/effects-bibliography

[brendanzab]

Yeah, great idea, forgot about that one!

[brendanzab]

Also, @aatxe informs me that:

[although] dependent call-by-push-value is also a bit ahead of the research curve AFAIK, it seems like a promising avenue for sensibly integrating dependent types and effects

https://gitter.im/pikelet-lang/Lobby?at=5c53283941775971a0b50da8