Bluefin, a new effect system

Announcements
#1

I’ve mentioned my new effect system, Bluefin, a few times on this forum. It’s now ready for me to announce it more formally.

Bluefin’s API differs from all prior effect systems in that it implements a “well typed Handle/Services pattern”. That is, all effects are accessed through value-level handles, which makes it trivial to mix a wide variety of effects, including:

If you’re interested then read the Introduction to Bluefin. I’d love to know what you all think.

36 Likes
#2

From the linked Introduction:

countPositivesNegatives :: [Int] -> String
countPositivesNegatives is = runPureEff $
  evalState (0 :: Int) $ \positives -> do
      r <- try $ \ex ->
          evalState (0 :: Int) $ \negatives -> do
              for_ is $ \i -> do
                  case compare i 0 of
                      GT -> modify positives (+ 1)
                      EQ -> throw ex ()
                      LT -> modify negatives (+ 1)

              p <- get positives
              n <- get negatives

              pure $
                "Positives: "
                  ++ show p
                  ++ ", negatives "
                  ++ show n

      case r of
          Right r' -> pure r'
          Left () -> do
              p <- get positives
              pure $
                "We saw a zero, but before that there were "
                  ++ show p
                  ++ " positives"

Wow, this is great work, especially seeing how seemless and idiomatically it integrates with typical Haskell code!

Have you considered combining the explicit handle- or capability-passing style with implicit parameters? I imagine that often there’s just a single effect of a given kind to consider. I imagine that it’s a bit like labels in Java, where you only want to give an outer: label to break out of an outer loop.

Although arguably, when there are multiple effects involved, the naming helps. It is a shame that implicit arguments are non-standard and cumbersome to use. By contrast, the explicit naming isn’t all that annoying in the single effect case.

I imagine that GHC 15 would allow us to write \@positives -> ... modify @positives (+ 1) ... and leave out the implicit value argument when it can be inferred, but I’m not holding my breath yet.

2 Likes
#3

Thanks!

Yes, it was suggested by @prophet, but I couldn’t get it to work. I don’t know if there’s some technical reason that it is hopeless or whether it just needs someone clever enough to work out the recipe. Someone might like to look at my progress so far.

Yes, I also tried that but type abstractions don’t seem good enough yet. Perhaps by GHC 15 they will be!

3 Likes
#4

This is really cool! For a long time I’ve been wondering if we could have an effect system that’s as nice to work with as effectful or cleff, but with first class effects that we pass around, rather than shuffling everything around implicitly. I was particualy motivated to explore this when I opened “When is something an effect, and when is something a handle?” on the effectful discussion board - and I still don’t know what the answer to that question is. It makes me err more on the side of preferring handles, but I’m not quite sure why. I started exploring something a bit like Bluefin myself, hoping to not need any type classes at all, but I do ultimately think you need something like your :> class - it basically ends up needing something like Oleg’s “Lightweight monadic regions” to scope the effect. At this point I lost interest, but kudos for pushing on - your solution is a lot cleaner than I thought would be possible!

Now the inevitable unfortunately is work has already made one massive shift to effectful, and probably can’t afford another anytime soon. I do wonder if there’s a way to “reify” implicit effects in effectful into an explicit handler. That would be very cool, but your comments here don’t fill me with hope

Anyway, a bit of a rambly reply - but great work! I look forward to seeing where this goes next, when it gets exercised a bit more.

(And sorry I never replied to your original email!)

3 Likes
#5

Thanks! I think there’s a good chance there’s an ergonomic way of converting between effectful and Bluefin, but I haven’t found it yet. One major impediment is that effectful (and all other effect libraries, I think) track effects in a type level list. Bluefin tracks them in a type level binary tree. I think the latter is much more ergonomic because it allows you to do compound effects really trivially.

#6

Yes, I noticed that when initially wondering why you had :& instead of just reusing : - only to realize what you’re doing. That’s quite nifty!

2 Likes
#7

Yes, there is. I have a work-in-progress implementation of that at GitHub - tomjaguarpaw/bluefin-style-effectful: Bluefin-style effectful. Specifically, the applyHandle and withHandle functions convert between implicit type class style and explicit handle style. Native effectful effects are wrapped in Handle to become value-level handles. So, for example, you can convert between effectful and Bluefin-style State operations and handlers. N.B. This doesn’t allow interoperation between effectful and bluefin. Rather, it’s a value-level (Bluefin-style) API for effectful.

It’s going to take a bit of thinking to work out how to get the interop to be seamless, because effectful uses OverlappingInstaces to manage its type level effects whereas Bluefin needs IncoherentInstances. I had to define my own :>.

Is this project something you’d be interested in collaborating on, by any chance?

What is an effect and an effect system?
#8

I’m pretty surprised to that. Why does it need more than just overlapping instances?

#9

Because handlers are of the form

handler :: (forall e. Handle e -> Eff (e :& es) r) -> ...

so if you have an effectful operation that uses two effects, say of type

op :: (e1 :> effs, e2 :> effs) => Handle e1 -> Handle2 e2 -> Eff effs r

and you call it using handler like

handle $ \h -> op h h2

where h2 is bound in an outer scope, then e1 gets instantiated to (the rigid, skolem?) e and effs gets instantiated to e :& es. That means we end up with the constraint e2 :> (e :& es), and we need it to resolve to e2 :> es. That happens according to the instance (e2 :> es) => e2 :> (e :& es). Apparently that really does need INCOHERENT on the other instance e :> (e :& es) because it is a potential match for the head of the first, e2 :> (e :& es) (if e ~ e2). Now, it can’t actually match, because e is universally quantified, but it seems that INCOHERENT is still needed to let GHC apply the first instance without flagging an overlap.

1 Like