6.7. Explicit universal quantification

6.7.1. Universally-quantified data type fields

In a data or newtype declaration one can quantify the types of the constructor arguments. Here are several examples:

data T a = T1 (forall b. b -> b -> b) a data MonadT m = MkMonad { return :: forall a. a -> m a, bind :: forall a b. m a -> (a -> m b) -> m b } newtype Swizzle = MkSwizzle (Ord a => [a] -> [a])

The constructors now have so-called rank 2 polymorphic types, in which there is a for-all in the argument types.:

T1 :: forall a. (forall b. b -> b -> b) -> a -> T a MkMonad :: forall m. (forall a. a -> m a) -> (forall a b. m a -> (a -> m b) -> m b) -> MonadT m MkSwizzle :: (Ord a => [a] -> [a]) -> Swizzle

Notice that you don't need to use a forall if there's an explicit context. For example in the first argument of the constructor MkSwizzle, an implicit "forall a." is prefixed to the argument type. The implicit forall quantifies all type variables that are not already in scope, and are mentioned in the type quantified over.

As for type signatures, implicit quantification happens for non-overloaded types too. So if you write this:

data T a = MkT (Either a b) (b -> b)

it's just as if you had written this:

data T a = MkT (forall b. Either a b) (forall b. b -> b)

That is, since the type variable b isn't in scope, it's implicitly universally quantified. (Arguably, it would be better to require explicit quantification on constructor arguments where that is what is wanted. Feedback welcomed.)

6.7.2. Construction

You construct values of types T1, MonadT, Swizzle by applying the constructor to suitable values, just as usual. For example,

(T1 (\xy->x) 3) :: T Int (MkSwizzle sort) :: Swizzle (MkSwizzle reverse) :: Swizzle (let r x = Just x b m k = case m of Just y -> k y Nothing -> Nothing in MkMonad r b) :: MonadT Maybe

The type of the argument can, as usual, be more general than the type required, as (MkSwizzle reverse) shows. (reverse does not need the Ord constraint.)

6.7.3. Pattern matching

When you use pattern matching, the bound variables may now have polymorphic types. For example:

f :: T a -> a -> (a, Char) f (T1 f k) x = (f k x, f 'c' 'd') g :: (Ord a, Ord b) => Swizzle -> [a] -> (a -> b) -> [b] g (MkSwizzle s) xs f = s (map f (s xs)) h :: MonadT m -> [m a] -> m [a] h m [] = return m [] h m (x:xs) = bind m x $ \y -> bind m (h m xs) $ \ys -> return m (y:ys)

In the function h we use the record selectors return and bind to extract the polymorphic bind and return functions from the MonadT data structure, rather than using pattern matching.

You cannot pattern-match against an argument that is polymorphic. For example:

newtype TIM s a = TIM (ST s (Maybe a)) runTIM :: (forall s. TIM s a) -> Maybe a runTIM (TIM m) = runST m

Here the pattern-match fails, because you can't pattern-match against an argument of type (forall s. TIM s a). Instead you must bind the variable and pattern match in the right hand side:

runTIM :: (forall s. TIM s a) -> Maybe a runTIM tm = case tm of { TIM m -> runST m }

The tm on the right hand side is (invisibly) instantiated, like any polymorphic value at its occurrence site, and now you can pattern-match against it.

6.7.4. The partial-application restriction

There is really only one way in which data structures with polymorphic components might surprise you: you must not partially apply them. For example, this is illegal:

map MkSwizzle [sort, reverse]

The restriction is this: every subexpression of the program must have a type that has no for-alls, except that in a function application (f e1…en) the partial applications are not subject to this rule. The restriction makes type inference feasible.

In the illegal example, the sub-expression MkSwizzle has the polymorphic type (Ord b => [b] -> [b]) -> Swizzle and is not a sub-expression of an enclosing application. On the other hand, this expression is OK:

map (T1 (\a b -> a)) [1,2,3]

even though it involves a partial application of T1, because the sub-expression T1 (\a b -> a) has type Int -> T Int.

6.7.5. Type signatures

Once you have data constructors with universally-quantified fields, or constants such as runST that have rank-2 types, it isn't long before you discover that you need more! Consider:

mkTs f x y = [T1 f x, T1 f y]

mkTs is a fuction that constructs some values of type T, using some pieces passed to it. The trouble is that since f is a function argument, Haskell assumes that it is monomorphic, so we'll get a type error when applying T1 to it. This is a rather silly example, but the problem really bites in practice. Lots of people trip over the fact that you can't make "wrappers functions" for runST for exactly the same reason. In short, it is impossible to build abstractions around functions with rank-2 types.

The solution is fairly clear. We provide the ability to give a rank-2 type signature for ordinary functions (not only data constructors), thus:

mkTs :: (forall b. b -> b -> b) -> a -> [T a] mkTs f x y = [T1 f x, T1 f y]

This type signature tells the compiler to attribute f with the polymorphic type (forall b. b -> b -> b) when type checking the body of mkTs, so now the application of T1 is fine.

There are two restrictions:

• You can only define a rank 2 type, specified by the following grammar:

  rank2type ::= [forall tyvars .] [context =>] funty funty ::= ([forall tyvars .] [context =>] ty) -> funty | ty ty ::= ...current Haskell monotype syntax...

  Informally, the universal quantification must all be right at the beginning, or at the top level of a function argument.

• There is a restriction on the definition of a function whose type signature is a rank-2 type: the polymorphic arguments must be matched on the left hand side of the "=" sign. You can't define mkTs like this:

  mkTs :: (forall b. b -> b -> b) -> a -> [T a] mkTs = \ f x y -> [T1 f x, T1 f y]

  The same partial-application rule applies to ordinary functions with rank-2 types as applied to data constructors.

6.7.6. Type synonyms and hoisting

GHC also allows you to write a forall in a type synonym, thus:

type Discard a = forall b. a -> b -> a f :: Discard a f x y = x

However, it is often convenient to use these sort of synonyms at the right hand end of an arrow, thus:

type Discard a = forall b. a -> b -> a g :: Int -> Discard Int g x y z = x+y

Simply expanding the type synonym would give

g :: Int -> (forall b. Int -> b -> Int)

but GHC "hoists" the forall to give the isomorphic type

g :: forall b. Int -> Int -> b -> Int

In general, the rule is this: to determine the type specified by any explicit user-written type (e.g. in a type signature), GHC expands type synonyms and then repeatedly performs the transformation:

type1 -> forall a. type2 ==> forall a. type1 -> type2

(In fact, GHC tries to retain as much synonym information as possible for use in error messages, but that is a usability issue.) This rule applies, of course, whether or not the forall comes from a synonym. For example, here is another valid way to write g's type signature:

g :: Int -> Int -> forall b. b -> Int