In Haskell 98, all type signatures are implicitly universally
quantified at the outer level, for example
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
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) |
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.
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.