wiki:PolymorphicComponents

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

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:

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

TODO:

  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