3 ms·
I've been thinking a lot about effects systems recently. A few months ago I implemented an effects system based interpreter in Haskell for an embedded DSL proto
by rebeccaskinner 2y ago
I've been thinking a lot about effects systems recently. A few months ago I implemented an effects system based interpreter in Haskell for an embedded DSL prototype for a project at work. In our case, the effects we were concerned with were all some variation of reading data, and the effects based approach allowed us to statically ensure that data would be available, and let us perform some clever optimizations to reduce the overhead of large IO operations.
We've since rewritten the system and, while we still support an optional effects based style in our DSL, it's not being used very heavily. In practice, our user found the ergonomics of the effects system quite challenging, and it introduced some type inference challenges. The biggest problem was that our use-cases ended up with functions that would have hundreds of effects, and it was fairly unwieldy and the type errors were difficult to deal with. Since we've introduced the updated version, most users prefer to user our newer features that allow them to write more traditional code even though it means they don't get composable effects.
On the other side of the experience, I've come to believe that effects systems are a good idea, but when adding them to an existing language it's probably best to make them an opt-in feature that can be used to constrain specific small parts of a program, rather than something that should be applied globally. I also think we need a bit more research into the ergonomics before they are going to appeal to a lot of users. That said, the guarantees and optimization opportunities ours gave us were really nice, and were quite difficult to achieve without building on top of the effects system (our new system is about an order of magnitude more code, for example).
- deleted 2y ago[deleted]
- chuckadams 2y agoJust curious what you think of abilities in Unison? I've yet to use Unison in anger, but from what I've peeked at, abilities look really elegant to me.
- rebeccaskinner 2y agoI like what I’ve seen of unison and I think it has some great ideas, but I haven’t had a chance to dive into it deeply enough to have a stronger opinion than that unfortunately.
- iamwil 2y agoHow did you learn how to implement an effects system? Are there resources you can share that taught you the fundamentals?
- rebeccaskinner 2y agoPersonally I didn’t do a lot of specific research when I started. I’ve read through the implementations of a few of the ones out on hackage, and a few papers, so the ideas were in the back of my mind. Here are a few papers that might be useful (sorry I don’t have links, I’m just looking through my research directory and copying title names): - Stitch: The Sound Type-Indexed Type Checker (Functional Pearl) by Richard Eisenberg - A Criterion for Kan Extensions of Lax Monoidal Functors by Tobias Fritz and Paolo Perrone - Effect systems revisited—control-flow algebra and semantics by Alan Mycroft, Dominic Orchard, and Tomas Petricek - Kleisli arrows of outrageous fortune by CONOR McBRIDE - Parametric Effect Monads and Semantics of Effect Systems by Shin-ya Katsumata - Unifying graded and parameterised monads by Dominic Orchard and Philip Wadler For a much more gentle introduction to some of the basic bits like using GADTs to accumulate effect annotations at the type level and building recursive type class instances to traverse them I’d recommend chapter 15 of my own book, Effective Haskell. From the examples in that chapter and the papers I listed I think you’d have everything you need to have a go at it.
- iamwil 2y agoThanks for the detailed response! I'll check it out.
- hinkley 2y agoIn Erlang, messages can bring state to a gen_server, and the accumulations of state are sliced very small and spread out through the system. The problem with imperative languages is the accumulation of global shared state. Worst case the interactions between those states grow factorially. Best case they grow logarithmically, but practically you will have to constantly fight against it trending toward n^1/2 instead, which is not sustainable. No I think effects need homes and letting them talk to each other is a formal introduction (friction) not the unending piles of expediencies you see in companies that will soon collapse under their own weight.