The H2 Wiki

bluefin-plucking-constraints

Plucking constraints in Bluefin

ONe of the promises of strongly-typed, pure functional programming is to “make invalid states unrepresentable”. How does this look in the context of effects in Haskell? Consider an operation foo with type ExceptT String (State Int) (). The valid states of such an operation are those that can throw a String exception, manipulate an Int state (and eventually terminate with a ()). So far so good. But the story gets even better. We can handle effects, making the set of valid states even smaller. For example, if we decide to handle the String exception, and if we catch one, to add its length to the Int state as follows

handleLength :: ExceptT String (State Int) () -> State Int ()
handleLength m = do
  e <- runExceptT m
  case e of
    Left s -> modify (+ length s)
    Right () -> pure ()

Then handleLength foo :: State Int ().

The resulting operation has type State Int (). We have restricted the space of valid states to those operations that manipulate an Int state, despite the fact that the implementation uses an exception.

But we don’t typically want to write concrete monad transformer stacks. Instead we can use MTL-style constraints, for example (MonadError String m, MonadState Int m) => m (). Then exactly the same implementation as handleLength works for this MTL style function too!

Suppose fooMTL :: (MonadError String m, MonadState Int m) => m (). Then defining

handleLengthMTL :: MonadState Int m => ExceptT String m () -> m ()
handleLengthMTL m = do
  e <- runExceptT m
  case e of
    Left s -> modify (+ length s)
    Right () -> pure ()

we have handleLengthMTL fooMTL :: MonadState Int m => m (). How does this work? Well, let’s consider the two types involved, renaming the type variable in fooMTL from m to m' to avoid confusion.

fooMTL :: (MonadError String m', MonadState Int m') => m' ()
handleLengthMTL :: MonadState Int m => ExceptT String m () => m ()

Then we we form handleLengthMTL fooMTL, m' has to be ExceptT String m', so we end up with

handleLengthMTL fooTML ::
  ( MonadError String (ExceptT String m'),
    MonadState Int (ExceptT String m'),
    MonadState Int m,
  ) =>
  ExceptT String m' () ->
  m ' ()

That’s exactly what we expect, except that there are two constraints. Can we discharge them? Let’s see how that proceeds. Firstly, there is an instance

instance Monad m => MonadError e (ExceptT e m)

so the first constraint reduces to Monad m. The third constraint is MonadState Int m, and there’s nothing to be done about that. It’s still a constraint on the result.

The second constraint is more interesting. There is an instance

instance MonadState s m => MonadState s (ExceptT e m)

so the second constraint reduces to MonadState s m. But MonadState s m can only hold when Monad m holds, so the remaining constraint is just MonadState s m.

How did this work? It crucially depended on two elements: firstly, the MonadError instance for ExceptT. That part is straightforward and expected. Less straightforward is the second element: the MonadState instance that “passes” state behaviour through the ExceptT layer to the inner m which is itself an instance of MonadState.

This is why MTL style has the “n squared instances problem”: for every effect “MyEffect” I define, I need a constraint (say MonadMyEffect), I need a transformer MyEffectT, an MonadMyEffect instance for MyEffectT, by then crucially, n more instances, for every other effect constraint, that delegate the effect to the inner monad. For example, I need

instance MonadState s m => MonadState s (MyEffectT m)
instance MonadError e m => MonadError e (MyEffectT m)
...

So far this article has mostly recapitulated what Matt Parsons wrote in his article “Plucking Constraints”. Now let’s see something different: how plucking constraints works in Bluefin.

Bluefin

So far we have seen types

foo :: ExceptT String (State Int)
fooMTL :: (MonadError String m, MonadState Int m) => m ()

The Bluefin equivalent is

fooBf ::
  (e1 :> es, e2 :> es) =>
  State Int e1 ->
  Exception String e2 ->
  Eff es ()

and the Bluefin equivalent of the handler is

handleLengthBf ::
  (e1 :> es) =>
  (forall e2. Exception String e2 -> Eff (e2 :& es) r) ->
  State Int e1 ->
  Eff es ()
handleLengthBf m st =
  e <- try m
  case e of
    Left s -> modify st (+ length s)
    Right () -> pure ()

When we use it to handle fooBf we get

\s -> handleLengthBf (fooBf s) s ::
  (e1 :> es) => State Int e1 -> Eff es ()

Let’s see how this one works. Again, I’m going to rename a type variable to avoid confusion, this time es in fooBf to es'.

fooBf ::
  (e1 :> es', e2 :> es') =>
  State Int e1 ->
  Exception String e2 ->
  Eff es' ()

This means that when we form handleLengthBf (fooBf s) s we need to choose e2 :& es for es', so we get the type

handledBf :: (e1 :> es) => State Int e1 -> Eff es ()
handledBf =
  handleLengthbf
    (fooBf s ::
      forall e2.
      (e1 :> (e2 :& es), e2 :> (e2 :& es)) =>
      Eff (e2 :& es) ())

Se the constraints we have to deal with relate to instances for :> in Bluefin. They are

e1 :> es
e1 :> (e2 :& es)
e2 :> (e2 :& es))

The first, e1 :> es is easiest, because there’s nothing we can do about it. It remains in the final form. This is analogous to the case of MonadState Int m above.

The second, e1 :> (e2 :& es) is dealt with by the following instance for :>:

instance (e :> es) => e :> (x :& es)

It becomes e1 :> es, identical to the constraint we already have. This is analogous to the case above, of

MonadState s m => MonadState s (ExceptT e m)

The third, e2 :> (e2 :& es), is satisfied by

instance e :> (e :> es)

and so is absent from the final form. This is analogous to the constraint MonadError String (ExceptT String m') above.

In this manner, Bluefin avoids the “n squared instances” problem. The only instances needed are those of :>, and they are crafted to deal with all the situations that they need to.

But hold on. Something funny happened here. The third constraint matches both of these instance definitions:

instance e :> (e :> es)
instance (e :> es) => e :> (x :& es)

Above we said that the third constraint was completely satisfied by the former, a desirable outcome. On the other hand, the latter seems to suggest the third constraint should be replaced by e2 :> es. We don’t want that because e2 is not even bound in the type signature for handledBf. It only occurs as a polymorphic type variable in fooBf.

So what’s going on? Well, I omitted something from the instance declarations above. The declaration for e :> (e :& es) is actually incoherent.

instance (e :> es) => e :> (x :& es)
instance {-# INCOHERENT #-} e :> (e :& es)

so we can only use the former instance if we know that e is not the same as x. But in this case we do! Why? Because is this case x is e1, which cannot be the same as e2, because e2 is universally quantified in handleLengthBf, so we can happily apply (e :> es) => e :> (x :& es).

References