Version 15 (modified by diatchki, 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


Open Issues

  1. allow empty foralls?
    data T a = Mk (forall . Show a => a)
  2. hugs vs. ghc treatment as keyword (see below)
  3. design choice: only wildcard & variables are allowed when pattern matching on polymorphic components (ghc allows as-patterns, hugs doesn't)


add polymorphic components


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


  • more complex denotational semantics

Report TODO List

List of items that need to change in the draft report.

  1. Introduce a new special identifier forall. This identifier has a special interpretation in types and type schemes (i.e., it is not a type variable). However, forall can still be used as an ordinary variable in expressions.
  2. syntax
    1. change "atype" or modify specific sections?
    2. 4.2.1 - syntax in "Algebreic Datatype Declarations", add forall to various bits.
    3. 4.2.3 - syntax in "Datatype Renaming" newtype declarations
  3. lots of english text in algebreic datatype declartions
  4. english text in Labelled fields - give an example of fields with polymorphic types, or do this in section 3?
  5. anything in "kind inference"?
  6. note for: for field labels, when you have the same label in different constructors, it's permitted as long as the type is the same; anything here to describe the syntactic checking that occurs to determine whether these types are the same? "Syntactic up-to alpha-renaming." Might be unintuative as this is rejected by GHC and Hugs:
    data T  = C1 { x :: forall a. (Show a,Eq a) => a -> a }
            | C2 { x :: forall a. (Eq a,Show a) => a -> a } 
  7. note you can name polymorphic components (see design choice above)
    1. when you match on x it instantiates the forall to a monomorphic type as below:
      data S    = C (forall a. [a])
      f (C x)   = (show (x::[Int]), show (x::String))
      -- f (C []) = ("[]","\"\"")
    2. this is not allowed: (see open issue above, iavor thinks GHC tried this and it was really tricky)
      f (C []) = True
    3. desugaring…
      f (C []) = e1 -- illegal
    would desugar to
    f x = case x of
           C [] -> e 1 -- illegal
           _ -> error ...
    would desugar to
    case x of
     C y -> case y of -- NOT illegal
             [] -> e1
             _ -> error...
     _ -> error...
    which is a little funny.
  8. where is explanation of type checking…
  9. where to put the bangs in strict polymorphic fields, hugs and GHC differ - can't figure it out in Hugs