Search code examples
haskelltypescategory-theoryisomorphismhigher-rank-types

Why is this type annotation wrong?

I tried to follow the article by Gabriel Gonzalez and I ran into a type mismatch. Consider the following short module:

{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE Rank2Types #-}

module Yoneda where

newtype F a = F a deriving (Show, Functor)

type G f a = forall a'. (a -> a') -> f a'

fw :: Functor f => G f a -> f a
fw x = x id

bw :: Functor f => f a -> G f a
bw x = \f -> fmap f x

It compiles fine. (With either ghc 8.2.2 and 8.4.3.) But when I poke it in repl, fw and bw do not compose:

λ :t bw . fw

<interactive>:1:6: error:
    • Couldn't match type ‘a’ with ‘G f a1’
      ‘a’ is a rigid type variable bound by
        the inferred type of it :: Functor f => a -> (a1 -> a') -> f a'
        at <interactive>:1:1
      Expected type: a -> f a1
        Actual type: G f a1 -> f a1
    • In the second argument of ‘(.)’, namely ‘fw’
      In the expression: bw . fw

When I look at bw more closely, it appears that the types of the functor it takes and returns are distinct:

λ :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

— Even though I stated in the type signature that they should be the same! And whatever type annotations I pepper fw and bw with, they do not want to unify.

If I remove the type signature from fw, everything works smoothly. In particular, the inferred type signature would then be:

fw :: ((a -> a) -> t) -> t

So, it appears that the forall quantifier spoils things. But I do not understand why. Should not it mean "any type a -> a' will do, including a -> a"? It seems as though the same type synonym G f a acts in different ways in the type signatures of fw and bw!

What's going on here?

Some more experiments:

λ (fw . bw) (F 1)
...error...
λ (fw (bw (F 1)))
F 1
λ :t fw . undefined
...error...
λ :t undefined . fw
...error
λ :t bw . undefined
bw . undefined :: Functor f => a1 -> (a2 -> a') -> f a'
λ :t undefined . bw
undefined . bw :: Functor f => f a -> c

So (as @chi pointed out in an answer) no function may be composed with fw. But not so for bw. Why?

Solution

  • This is a predicativity issue.

    Essentially, if we have a polymorphic value f :: forall a . SomeTypeDependingOn a, and we use it in some larger expression, this can instantiate the type a to any type T needed to fit that context. However, predicativity requires that T does not contain foralls. This restriction is needed to have type inference.

    In your code, bw . fw you use the polymorphic function . (composition). This has a polymorphic type, where one type variable t stands for the domain of the second function to be composed (g in f . g) . For bw . fw to type check we should pick t ~ G f a, but G f a = (forall a' . ...) so it violates predicativity.

    The usual solution is to use a newtype wrapper

    newtype G f a = G { unG :: forall a'. (a -> a') -> f a' }

    which "hides" the forall under a constructor, so that t ~ G f a becomes allowed. To use that, one needs to exploit the isomorphisms G and unG as needed, wrapping and unwrapping as needed. This requires extra work by the programmer, but it is this work that enables the inference algorithm to do its job.

    Alternatively, don't use ., and compose your functions in pointful style

    test :: Functor f => G f a -> G f a
test x = bw (fw x)

    About the type of bw, as reported by GHCi:

    > :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

    This type is the result of "forall hoisting", which essentially "moves" the universal quantifiers in this way:

    a1 -> ... -> forall b. F b   =====>     forall b. a1 -> ... -> F b

    Hoisting is automatically performed so to help type inference.

    More in defail, we have

    bw :: forall f a . Functor f => f a -> G f a
-- by definition of G
bw :: forall f a . Functor f => f a -> (forall a'. (a -> a') -> f a')
-- after hoisting
bw :: forall f a a'. Functor f => f a -> (a -> a') -> f a'

    Since now all the quantifiers are at the top level, when composing bw with another function as in bw . h or h . bw, we can first instantiate f, a, a' to fresh type variables, and then perform unification on such variables so to match the type of h.

    For instance, in bw . undefined we proceed as follows

     -- fresh variables for (.)
 (.) :: (b -> c) -> (a -> b) -> a -> c
 -- fresh variables for bw
 bw :: Functor f . f a1 -> (a1 -> a') -> f a'
 -- fresh variables for undefined
 undefined :: a2

 So we get:
 b = f a1
 c = (a1 -> a') -> f a'
 a2 = a -> b

 Hence the type of (bw . undefined) is
 a -> c
 = a -> (a1 -> a') -> f a'
 (assuming Functor f)

    GHCi agrees, except that it chooses different names for the type variables. This choice is immaterial, of course.

    (bw . undefined) :: Functor f => a1 -> (a2 -> a') -> f a'

    Ah-ha! There seems to be some issue with GHCi-8.2.2 which is not present in GHC 8.4.3.

    -- GHCi 8.2.2
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f1 => f2 a1 -> (a2 -> a') -> f1 a'

-- GHCi 8.4.3
> :set -XRankNTypes
> type G f a = forall a'. (a -> a') -> f a'
> bw :: Functor f => f a -> G f a ; bw x = \f -> fmap f x
> :t bw
bw :: Functor f => f a -> (a -> a') -> f a'