wiki:PolymorphicComponents

Version 10 (modified by ross@…, 8 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

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