Version 18 (modified by diatchki, 10 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
    scheme   -> 'forall' tvar_1 .. tyvar_n '.' opt_ctxt type    (n > 0)
              | type
    ascheme  -> '(' scheme ')'
              | atype
    bscheme  -> '(' scheme ')'
              | btype
    opt_ctxt -> context '=>'
  3. Syntax for algebraic datatype (Section 4.2.1)

Change type,atype,btype to scheme, ascheme, bscheme' respectively.

constr   -> con [!] ascheme_1 ... [!] ascheme_k 	 (arity con = k, k>=0)
	  | (bscheme | ! ascheme) conop (bscheme | ! ascheme) 	(infix conop)
	  | con { fielddecl1 , ... , fielddecln } 	(n>=0)
fielddecl-> vars :: (scheme | ! ascheme)
  1. 4.2.1 - syntax in "Algebreic Datatype Declarations", add forall to various bits.
  2. 4.2.3 - syntax in "Datatype Renaming" newtype declarations
  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