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.

40 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.

3 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!)

4 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
#10

Haha. Would that it were so.

I had almost exactly the same class in my own project, with the same instances justified by the same reasoning:

class                                    x <:    xs  where index :: Index x xs
instance {-# INCOHERENT   #-}            x <: (x:xs) where index = Z
instance {-# OVERLAPPABLE #-} x <: xs => x <: (y:xs) where index = S index

I used this class to infer from types in context which element to pull from a heterogeneous list of skolem-tagged types. The result was a frightening heisenbug that violated the guarantees of my carefully crafted types and stole days of my life.

The core issue is (in my opinion) a GHC bug, or more charitably (and I can see the argument) an unfortunate deficiency in GHC’s treatment of our unrestricted types. We use polymorphic continuations like (forall x. ...) -> ... to introduce new, unique types into a limited scope, but from GHC’s perspective we’ve simply accepted a polymorphic argument and neglected to supply it with a concrete type.

To follow the principle of least surprise, GHC should instantiate each such case at a unique type—if it must instantiate them at all. But it does the exact opposite: they’re all defaulted to Any. Now instead of e1 :> [e1, e2] and e2 :> [e1, e2], you have two dictionaries for Any :> [Any, Any] and a specialiser that considers them interchangeable. Disaster.

One workaround is to NOINLINE everything that introduces a type you want to be treated as unique—this apparently prevents the specialiser from witnessing e1 ~ Any ~ e2. It also obstructs optimisation and could seriously degrade performance.

Another is to manually generate and supply the unique types yourself. There’s apparently a runExists primitive in the wings for just this purpose (GHC#19675), but it’s not implemented yet. I’ve also had a go at it myself. See GHC#24924 for details.

6 Likes
#11

Now instead of e1 :> [e1, e2] and e2 :> [e1, e2], you have two dictionaries for Any :> [Any, Any] and a specialiser that considers them interchangeable. Disaster.

I think bluefin avoids any such issues because its <: class is empty, so the behavior of a program cannot be affected from getting a different dictionary than expected.

1 Like
#12

That’s interesting. Thanks for sharing. In what circumstances does this arise? It would be really bad for Bluefin if the constraint e2 :> (e :& es) became satisfied, rather than “decaying” to e2 :> es!

On the other hand I don’t think it would be bad for Bluefin if the dictionary for e1 :> (e1 :& e2) were considered equal to the dictionary for e2 :> (e1 :& e2), because both are empty in any case.

#13

For bluefin itself where the class has no methods, I imagine you’re fine. But in bluefin-style-effectful you take the effectful version as a superclass—that makes it vulnerable.

I’m not sure what you mean by this, but to my (probably flawed) understanding, the issue doesn’t affect instance resolution itself, only the dictionaries you get after the fact.

1 Like
#14

Ah yes, I see. And also an experimental library I wrote that puts a Bluefin-style API on top of MTL/transformers.