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 ()
= do
handleLength m <- runExceptT m
e 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 ()
= do
handleLengthMTL m <- runExceptT m
e 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

```
fooTML ::
handleLengthMTLMonadError 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.

So far we have seen types

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

The Bluefin equivalent is

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

and the Bluefin equivalent of the handler is

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

When we use it to handle `fooBf`

we get

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

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 ::
:> es', e2 :> es') =>
(e1 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 s ::
(fooBfforall e2.
:> (e2 :& es), e2 :> (e2 :& es)) =>
(e1 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)`

.