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).

Tickets

#57

add polymorphic components

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 newtypes.
• useful for polymorphic continuation types, like the  ReadP type used in a proposed replacement for the Read class.

Cons

• more complex denotational semantics