The '~' Instance Pattern

Typeclass instance selection

Haskell typeclass instances have two parts: some constraints, and the instance head:

newtype WrappedFunctor f a = WrappedFunctor (n a)

instance Functor f => Functor (WrappedFunctor f) where
--       ^^^^^^^^^                                      constraints
--                    ^^^^^^^^^^^^^^^^^^^^^^^^^^        head

  fmap f (WrappedFunctor fa) = WrappedFunctor (fmap f fa)

More specifically, the head is of the form C (T a1 ... an), where C is the class, T is a type constructor, and a1 ... an are distinct type variables.1

When the type checker needs to find an instance, it does so purely based on the head, constraints don’t come into it. The instance above means “whenever you use WrappedFunctor f as a functor, regardless of what f is and even if we don’t know what it is yet, then you can use this instance”, and a type error will be thrown if whatever concrete type f is instantiated to doesn’t in fact have a functor instance.

You might think that, if we didn’t define the instance above and instead defined this one:

instance Functor (WrappedFunctor Maybe) where
  fmap f (WrappedFunctor fa) = WrappedFunctor (fmap f fa)

…and then used a WrappedFunctor f as a functor, that the type checker would infer f must be Maybe. This is not so! Typeclass inference happens under an “open world” approach: just because only one instance is known at this time doesn’t mean there won’t be a second instance discovered later. Prematurely selecting the instance for WrappedFunctor Maybe could be unsound.

Type equality constraints

In GHC Haskell, we can express a constraint that two types have to be equal. For example, this is a weird way to check that two values are equal:

-- this requires GADTs or TypeFamilies
funnyEq :: (Eq a, a ~ b) => a -> b -> Bool
funnyEq = (==)

We only have a constraint Eq a, not Eq b, but because of the a ~ b constraint, the type checker knows that they’re the same type:

> funnyEq 'a' 'b'
False
> funnyEq True True
True
> funnyEq True 'b'

<interactive>:22:1: error:
    • Couldn't match type ‘Bool’ with ‘Char’
        arising from a use of ‘funnyEq’
    • In the expression: funnyEq True 'b'
      In an equation for ‘it’: it = funnyEq True 'b'

Type equality constraints in typeclass instances

Let’s put the two together now. Let’s throw away the two instances we defined above, and now look at this one:

instance (f ~ Maybe) => Functor (WrappedFunctor f) where
  fmap f (WrappedFunctor fa) = WrappedFunctor (fmap f fa)

This instance means “whenever you use WrappedFunctor f as a functor, regardless of what f is and even if we don’t know what it is yet, then you can use this instance”, and a type error will be thrown if f cannot be instantiated to Maybe. This is different to the instance Functor (WrappedFunctor Maybe)!

  • If we have instance Functor (WrappedFunctor Maybe):

    > :t fmap (+1) (WrappedFunctor (pure 3))
  :: (Num b, Applicative f, Functor (WrappedFunctor f)) =>
     WrappedFunctor f b

  • If we have instance (f ~ Maybe) => Functor (WrappedFunctor f):

    > :t fmap (+1) (WrappedFunctor (pure 3))
  :: Num b => WrappedFunctor Maybe b

With the latter, we get much better type inference. The downside is that this instance overlaps any more concrete instances, so we couldn’t (for example) define an instance for WrappedFunctor Identity as well.

But if you only need one instance, it’s a neat trick.

Here’s a concrete example from the dejafu-2.0.0.0 branch. I’ve introduced a Program type, to model concurrent programs. There’s one sort of Program, a Program Basic, which can be used as a concurrency monad (a MonadConc) directly. The instances are defined like so:

instance (pty ~ Basic, MonadIO n) => MonadIO (Program pty n) where
  -- ...

instance (pty ~ Basic) => MonadTrans (Program pty) where
  -- ...

instance (pty ~ Basic) =>  MonadCatch (Program pty n) where
  -- ...

instance (pty ~ Basic) => MonadThrow (Program pty n) where
  -- ...

instance (pty ~ Basic) => MonadMask (Program pty n) where
  -- ...

instance (pty ~ Basic, Monad n) => MonadConc (Program pty n) where
  -- ...

If instead the instances has been defined for Program Basic n, then the type checker would have complained that the pty parameter is (in many cases) polymorphic, and not use these instances. This means every single use of a Program pty n, where pty was not otherwise constrained, would need a type annotation. By instead formulating the instances this way, the type checker knows that if you use a Program pty n as a MonadConc, then it must be a Program Basic n.

This has turned a potentially huge breaking change, requiring everyone who uses dejafu to add type annotations to their tests, into something which just works.

  1. The FlexibleInstances extension relaxes this restriction a little, allowing some (or all) of the a1 ... an to be arbitrary types, as well as type variables.↩︎