Version 9 (modified by ross@…, 9 years ago) (diff) |
---|

# Polymorphic Components

## Brief Explanation

Arguments of data constructors may have polymorphic types (marked with `forall`)
and contexts constraining universally quantified type variables, e.g.

newtype Swizzle = MkSwizzle (forall a. Ord a => [a] -> [a])

The constructor then has a rank-2 type:

MkSwizzle :: (forall a. Ord a => [a] -> [a]) -> Swizzle

If RankNTypes are not supported, these data constructors are subject to similar restrictions to functions with rank-2 types:

- polymorphic arguments can only be matched by a variable or wildcard (
`_`) pattern - when the costructor is used, it must be applied to the polymorphic arguments

This feature also makes it possible to create explicit dictionaries, e.g.

data MyMonad m = MkMonad { unit :: forall a. a -> m a, bind :: forall a b. m a -> (a -> m b) -> m b }

The field selectors here have ordinary polymorphic types:

unit :: MyMonad m -> a -> m a bind :: MyMonad m -> m a -> (a -> m b) -> m b

## References

- From Hindley-Milner Types to First-Class Structures by Mark P. Jones, Haskell Workshop, 1995.
- distinguish from ExistentialQuantification (currently also marked with
`forall`, but before the data constructor).

## Pros

- type inference is a simple extension of Hindley-Milner.
- offered by GHC and Hugs for years
- large increment in expressiveness: types become impredicative, albeit with an intervening data constructor, enabling Church encodings and similar System F tricks.
Functions with rank-2 types may be trivially encoded.
Functions with rank-n types may also be encoded, at the cost of packing and unpacking
`newtype`s. - useful for polymorphic continuation types, like the ReadP type used in a proposed replacement for the Read class.

## Cons

- more complex denotational semantics