GHC's type system supports explicit universal quantification in constructor fields and function arguments. This is useful for things like defining runST from the state-thread world. GHC's syntax for this now agrees with Hugs's, namely:
forall a b. (Ord a, Eq b) => a -> b -> a |
The context is, of course, optional. You can't use forall as a type variable any more!
Haskell type signatures are implicitly quantified. The forall allows us to say exactly what this means. For example:
g :: b -> b |
means this:
g :: forall b. (b -> b) |
The two are treated identically.
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) |
data T a = MkT (forall b. Either a b) (forall b. b -> b) |
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.)
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 } |
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.
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... |
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] |
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 |
type Discard a = forall b. a -> b -> a g :: Int -> Discard Int g x y z = x+y |
g :: Int -> (forall b. Int -> b -> Int) |
g :: forall b. Int -> Int -> b -> Int |
type1 -> forall a. type2 ==> forall a. type1 -> type2 |
g :: Int -> Int -> forall b. b -> Int |