The Hugs 98 User's Guide
Prev | Chapter 6. Language extensions supported by Hugs and GHC | Next

# 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.

Prev | Home | Next
Type class extensions | Up | Type annotations in patterns