Version 28 (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 for writing type schemes: (TODO check for ambiguities with happy.)
    poly     -> 'forall' tvar_1 ... tyvar_n '.' opt_ctxt type    (n > 0)
    opt_ctxt -> context '=>'
    scheme   -> '(' poly ')' | type
    ascheme  -> '(' poly ')' | atype
    bscheme  -> '(' poly ')' | btype
    NOTE: Schemes should not contain quantified variables that are not mentioned

in the scheme body because this probably indicates a programmer error.

  1. Syntax for data and newtype declarations
    -- Section 4.2.1
    constr   -> con acon_filed_1 ... acon_field_k       (arity con = k, k>=0)
    	  | bcon_field conop bcon_field             (infix conop)
    	  | con { fielddecl1 , ... , fielddecln }   (n>=0)
    fielddecl-> vars :: con_field 
    con_field  -> ! ascheme | scheme    -- or scheme instead of ascheme?
    acon_filed -> ! ascheme | ascheme
    bcon_filed -> ! ascheme | bscheme   -- or bscheme instead of ascheme?
    -- Section 4.2.3
    newconstr -> con ascheme
              | con { var :: scheme }
    NOTE: The grammar in the Haskell 98 report contains a minor bug that seems to allow erroneous data declarations like the following:
    data T = C !
    For this reason I introduced the con_field productions.
  2. Labeled fields.
    1. Type of the selector functions:
      data T a = C { x :: forall b. ctxt  => type }
      x :: ctxt => T a -> type
    2. If different constructors of the same datatype contain the same label, then the corresponding schemes should be equal up to renaming of the quantified variables.


  1. lots of english text in algebreic datatype declartions
  2. english text in Labelled fields - give an example of fields with polymorphic types, or do this in section 3?
  3. anything in "kind inference"?
  4. 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 } 
  5. 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.
  6. where is explanation of type checking…
  7. where to put the bangs in strict polymorphic fields, hugs and GHC differ - can't figure it out in Hugs