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

# 5.3. Quantified types

## 5.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 case 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)

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

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