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

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)

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

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
      

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

1. where is explanation of type checking...
2. where to put the bangs in strict polymorphic fields, hugs and GHC differ - can't figure it out in Hugs