6.3. Quantified types

6.3.1. Rank 2 types

In Haskell 98, all type signatures are implicitly universally quantified at the outer level, for example

id :: a -> a

Variables bound with a let or where may be polymorphic, as in

let f x = x in (f True, f 'a')

but function arguments may not be: Haskell 98 rejects

g f = (f True, f 'a')

However, with the -98, the function g may be given the signature

g :: (forall a. a -> a) -> (Bool, Char)

This is called a rank 2 type, because a function argument is polymorphic, as indicated by the forall quantifier.

Now the function g may be applied to expression whose generalized type is at least as general as that declared. In this particular example the choice is limited: we can write

g id
g undefined
g (const undefined)

or various equivalent forms

g (\x -> x)
g (id . id . id)
g (id id id)

There are a number of restrictions on such functions:

• Functions that take polymorphic arguments must be given an explicit type signature.

• In the definition of the function, polymorphic arguments must be matched, and can only be matched by a variable or wildcard (_) pattern.

• When such functions are used, the polymorphic arguments must be supplied: you can't just use g on its own.

GHC, which supports arbitrary rank polymorphism, is able to relax some of these restrictions.

Hugs reports an error if a type variable in a forall is unused in the enclosed type.

An important application of rank 2 types is the primitive

runST :: (forall s. ST s a) -> a

in the module Control.Monad.ST. Here the type signature ensures that objects created by the state monad, whose types all refer to the parameter s, are unused outside the application of runST. Thus to use this module you need the -98 option. Also, from the restrictions above, it follows that runST must always be applied to its polymorphic argument. Hugs does not permit either of

myRunST :: (forall s. ST s a) -> a
myRunST = runST

f x = runST $ do
      ...
      return y

(though GHC does). Instead, you can write

myRunST :: (forall s. ST s a) -> a
myRunST x = runST x

f x = runST (do
      ...
      return y)

6.3.2. Polymorphic components

Similarly, components of a constructor may be polymorphic:

newtype List a = MkList (forall r. r -> (a -> r -> r) -> r)
newtype NatTrans f g = MkNT (forall a. f a -> g a)
data MonadT m = MkMonad {
                my_return :: forall a. a -> m a,
                my_bind :: forall a b. m a -> (a -> m b) -> m b
              }

So that the constructors have rank 2 types:

MkList :: (forall r. r -> (a -> r -> r) -> r) -> List a
MkNT :: (forall a. f a -> g a) -> NatTrans f g
MkMonad :: (forall a. a -> m a) ->
           (forall a b. m a -> (a -> m b) -> m b) -> MonadT m

As with functions having rank 2 types, such a constructor must be supplied with any polymorphic arguments when it is used in an expression.

The record update syntax cannot be used with records containing polymorphic components.

6.3.3. Existential quantification

It is also possible to have existentially quantified constructors, somewhat confusingly also specified with forall, but before the constructor, as in

data Accum a = forall s. MkAccum s (a -> s -> s) (s -> a)

This type describes objects with a state of an abstract type s, together with functions to update and query the state. The forall is somewhat motivated by the polymorphic type of the constructor MkAccum, which is

s -> (a -> s -> s) -> (s -> a) -> Accum a

because it must be able to operate on any state.

Some sample values of the Accum type are:

adder = MkAccum 0 (+) id
averager = MkAccum (0,0)
                   (\x (t,n) -> (t+x,n+1))
                   (uncurry (/))

Unfortunately, existentially quantified constructors may not contain named fields. You also can't use deriving with existentially quantified types.

When we match against an existentially quantified constructor, as in

runAccum (MkAccum s add get) [] = ??

we do not know the type of s, only that add and get take arguments of the same type as s. So our options are limited. One possibility is

runAccum (MkAccum s add get) [] = get s

Similarly we can also write

runAccum (MkAccum s add get) (x:xs) =
    runAccum (MkAccum (add x v) add get) xs

This particular application of existentials – modelling objects – may also be done with a Haskell 98 recursive type:

data Accum a = MkAccum { add_value :: a -> Accum a, get_value :: a}

but other applications do require existentials.