wiki:PolymorphicComponents

Version 13 (modified by ijones, 7 years ago) (diff)

notes about semantics of binding

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 required in patterns (ghc allows as-patterns, hugs doesn't) allowed for polymorphic fields

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. is forall a keyword? in what cases? (In types? In identifiers?)
    f forall = forall
    
    1. Hugs treats forall as a reserved keyword, whereas GHC only treats it specially in types.
  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 when you pattern-match on a field w/ a polymorphic type, the bound variables also have a polymorphic type
    1. but case is different; 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