Work on effect systems - Haskell

Welcome to the Functional Programming Zulip Chat Archive. You can join the chat here.

TheMatten

@Sandy Maguire Is there anything you would change about your approach on polysemy now?

Sandy Maguire

i think i'd get rid of tactics

Sandy Maguire

and then all of those janky Weaving things.... give the variables much better names

TheMatten

I guess you're not the only one - Weaving seems to be the culprit :big_smile:

Sandy Maguire

but more generally i think it's too complicated

Sandy Maguire

it's _sorta_ a solution to effects, but not really

Sandy Maguire

and the "not really" part adds so many warts and tons of complexity

TheMatten

I still wonder whether ability to remove effects from the stack one by one is what we want - I always thought of effect systems as "composable compilers" with one actual output

TheMatten

Once you don't need that, Weaving disappears it seems

Sandy Maguire

cool. i'd love to see that

TheMatten

We had some conversation with Ollie and he compared it to final-encoding-version of some other lib - maybe I can find it somewhere :big_smile:

Sandy Maguire

oh yeah i remember that

Alexis King

I haven’t been following this discussion at all, but: my “boring Haskell” take on effect systems is that I think monad transformers are the single largest barrier to entry to writing useful Haskell code. They are hard to understand for beginners (especially once you bring mtl into the picture), and they have subtleties that even experts don’t follow. It has been my goal for a little while to “close the book” on effects in Haskell, so to speak—I’d love for us to have a solution that we can recommend to people instead of monad transformers, without serious caveats. We’re not there yet, but I think the existing work is useful (and I’m very optimistic about my current approach).

Sandy Maguire

it's a hard problem. in the meantime i'm just going to sit here and work on my own little programs

Alexis King

@Sandy Maguire You might be interested in some of my recent efforts… I’ve gone in a different direction from when we last talked about it.

TheMatten

@Alexis King I've followed your twitter and eff/delimited-control - you mentioned that this would be probably better with specific language support if I remember right - are there some updates on that?

Alexis King

I think language support would definitely help to make things absolutely ideal, but I’m optimistic about where things have been going. I’ve been restructuring that branch a little in my spare time (though the going has been slow, since I haven’t had very much spare time!) to fix an issue with state and captured continuations, but the core approach works. Most of the difficulty is figuring out how to represent everything as efficiently as possible, but to be honest I’d bet some of what I’m doing is microoptimizations at this point. I just want to get it right!

Alexis King

The current implementation I have is essentially an implementation of a virtual machine that supports delimited control, as an embedded DSL in Haskell. It’s been fun—I don’t get to munge about with low-level things in Haskell very often. :)

Sandy Maguire

(fwiw i'm pretty much off of the haskell scene these days)

Sandy Maguire

my activity in this channel over the last hour is the most i've been engaged in the community in like two months

Alexis King

Haha, I know what that’s like. I certainly don’t have any expectations of work from you! ;)

TheMatten

Oh, nice - I'm super excited about what comes out of it. Thanks for your hard work! :slight_smile:
Over at #Polysemy we're discussing project "roadmap" - it seems like we've settled down on an idea that "we want to replace Weaving at some point" - if eff can provide some better model, it may be interesting to consider it for some bigger version bump in the future :slight_smile:

Alexis King

But yes… evaluating performance is challenging because we don’t have very many good benchmarks for this sort of thing, but I am positive for several reasons. I expect performance to be very good, significantly better than the free/freer encodings, albeit not as fast as concrete transformers, especially for microbenchmarks (but quite possibly meaningfully faster than polymorphic mtl code!). And because it’s all based on delimited control, the semantics for scoping operations are a lot nicer than they are in mtl/polysemy/fused-effects, imo. And I think the interface is as nice as polysemy’s, and possibly nicer!

Alexis King

The big downside to the approach is that you can’t really just slam in arbitrary scoped operations that want to live in IO, or in some other monad transformer stack. Algebraic operations are fine, and I’m pretty confident that I can get exceptions/bracketing working and all that good stuff, but it won’t interop nicely with everything else; you’ll have to do manual work to connect the universes.

Alexis King

One of the reasons this has been so much fun to work on is I’m doing all kinds of unsafe nonsense under the covers, but I’m trying to make it all internally type safe as much as possible, even if theoretically I could do it without all that safety and still provide a safe interface. So I’ve been getting to apply various evil tricks. :)

TheMatten

When it comes to some observations from polysemy 's UX - semantics should be less confusing and there should be easier, syntactically cheap and "safe" way to differentiate different members with same underlying effect (to replace Tagged)

Alexis King

The basic idea is that the virtual machine maintains an explicit stack of “metacontinuation frames,” which is literally a mutable stack (represented as a SmallMutableArray# under the hood), and running a handler pushes a frame onto the stack (which gets popped after the handler returns). This approach gives both really good time complexity and really good constant factors for all the common operations. send just involves a couple pointer lookups and a function call. handle just involves allocating a small bit of memory for the stack frame and writing a pointer to it into the mutable array. Operations that don’t need to muck about with the continuation or just need to abort are basically free. Capturing a continuation is more expensive in the general case, but I think I can provide a fast path for what seems to be the most common cases.

Alexis King

One of the really nice things about this approach is that its performance doesn’t depend on the GHC optimizer at all: it’s just fundamentally fast. This is a little bit of a two-edged sword because it means that GHC can’t optimize away the dispatch completely (GHC has no idea how to see through all this stuff), which looks bad for extremely contrived microbenchmarks, but I think it essentially never matters for real programs.

Alexis King

Theoretically a compiler plugin could add a custom optimization pass to do cleverer specialization, but I’m pretty sure that would be totally overkill. I don’t have numbers yet, but I’m betting this approach will do very well compared to all existing effect systems, including polymorphic mtl code. :)

Alexis King

It turns out that 100% of the implementation subtlety comes from nontrivial cases of continuation capture and restore, which probably isn’t shocking, since that’s the most complicated part. Operations that invoke the continuation immediately (like ask) are trivial, as are operations that just abort (like catch). But operations that capture the continuation, extend it somehow, and then invoke it (like NonDet’s <|>) are the subtle case.

TheMatten

@Alexis King Are there some resources on idea of metacontinuations? I have basic idea about lisp-style continuations, but wasn't able to find that much on the former.
Premise of "free-style" effect systems was that can be optimized out to underlying operations at compile-time - do you think it's not really possible to accomplish this in general, across module boundaries?

Alexis King

I asked Matthew Flatt, the primary developer of the Racket runtime, about pointers for efficiently implementing delimited control. He pointed me to metacontinuations, specifically the explanation in “Final Shift for call/cc: a Direct Implementation of Shift and Reset.” Amusingly, that paper is actually about not using metacontinuations, but the introduction provides the best explanation of what they are that I’ve been able to find in the literature. The paper ignores a lot of subtleties, like adding support for tagged prompts, but the core ideas are all there, and I was able to work up to a more general implementation from that starting point. (My implementation is actually unlike any other implementation of delimited control I know of because it’s tailored in certain ways to an effect system, but the core implementation technique is still metacontinuations.)

James King

One of the reasons this has been so much fun to work on is I’m doing all kinds of unsafe nonsense under the covers, but I’m trying to make it all internally type safe as much as possible, even if theoretically I could do it without all that safety and still provide a safe interface. So I’ve been getting to apply various evil tricks. :)

This is why I find type theory is such a good tool for reasoning about computers. There's some work going on over in the Lean VM that is using quotient types over sets to prove that unsafe mutation of memory "under the hood" is safe which can lead to some significant performance improvements.

Alexis King

Premise of "free-style" effect systems was that can be optimized out to underlying operations at compile-time - do you think it's not really possible to accomplish this in general, across module boundaries?

I think it really depends on what you mean. The approach I have right now is basically a “free style” approach from the POV of its public interface; it works very much like the polysemy interface does. And that approach has a really fast implementation of dispatch, so under some definition it’s “optimized out to underlying operations.” However, it doesn’t let GHC inline concrete implementations of those operations, which is normally not a big deal, but there are a few cases where it could provide significant speedups, such as introducing a local State effect that could be optimized into a tight loop.

I think specializing effects across module boundaries is hopeless and honestly not worth pursuing. It’s unlikely to get you very much. One of the key points of eff’s new implementation is that >>= always gets specialized, so you don’t need cross-module specialization for that. Specializing effects within a single module is more reasonable, and I think that is possible, but I don’t think it’s possible to do with RULES alone, so I think you’d probably need a compiler plugin (or support in GHC).

Alexis King

One way to think of my implementation is as an aggressively final encoding of the free-style interface. :)

Alexis King

One of the main things that led me towards this implementation path was the realization that there’s just no way to get >>= to specialize with an approach based on polymorphic monad transformers, which really, really bites you in a lot of cases. GHC really wants to be able to see through >>= calls, since if you have a sequence of >>=s that don’t actually do any effectful operations (which happens often when using combinators or writing bits of glue code), GHC will just make those calls disappear.

We really want this, but you can’t get it with mtl-style constraints (which includes fused-effects) because >>= includes part of the implementation of each effect! This sucks incredibly hard, because GHC has to make an unknown call to >>= even if you do something like pure x >>= f, since GHC doesn’t take advantage of laws and doesn’t know what >>= will do. My new implementation takes care to ensure >>= is always inlined, so those patterns have zero cost, and even if you do use effectful operations, you still never have to make an unknown call to >>=.

Alexis King

Something unfortunate about this approach is that it does still require CPSing the program (since it’s ultimately based on a continuation monad, albeit a continuation monad on steroids). That in and of itself isn’t a problem—GHC will still compile it to efficient code, since everything is a tail call by its nature—but it makes writing RULEs much more challenging. RULEs much prefer working on direct-style code.

Alexis King

I haven’t really worried about that yet, though. Performance should be good even without any rewrite rules.

James King

This is really cool, @Alexis King -- thanks for sharing!

Alexis King

Rather off-topic as “Boring Haskell” goes, I’ll admit. :)

James King

All good. I'm going to get the process of archiving these chats out to the web working again.

Ryan Gonzalez

Honestly I've been following your Twitter and the eff work, and I have no idea what any of it means or how it works but it looks absolutely amazing

Asad Saeeduddin

I added a big ole explanation in the README of https://github.com/masaeedu/monadoptics/ just now, folks interested in effect systems might find some useful ideas in there

Profunctor optics for the endofunctor category on Hask - masaeedu/monadoptics
TheMatten

@Asad Saeeduddin in that sense, interpreters are _simply_ type changing optics letting you access your effects? :big_smile:

Asad Saeeduddin

@TheMatten I ran out of steam before I got to that point, but it seems like a promising avenue of investigation

Sandy Maguire

I did something crazy; mixing 3 layer cake with SYTC for easy mocking. https://github.com/TheMatten/first-class-instances/pull/1

This thing lifts a class: class Monad m => MonadFoo m where foo :: m Int makeMockable ''MonadFoo into the following: type instance Inst (MonadFoo m_ar1R) = Dict (MonadFoo m_ar1R) newt...
Sandy Maguire

@Asad Saeeduddin you might be interested ^