Version 28 (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

- 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

- allow empty foralls?
data T a = Mk (forall . Show a => a)

- hugs vs. ghc treatment as keyword (see below)
- 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
`newtype`s. - 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.

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

- 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. - Labeled fields.
- Type of the selector functions:
data T a = C { x :: forall b. ctxt => type } x :: ctxt => T a -> type

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

- Type of the selector functions:

TODO:

- lots of english text in algebreic datatype declartions
- english text in Labelled fields - give an example of fields with polymorphic types, or do this in section 3?
- anything in "kind inference"?
*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 }

*note*you can name polymorphic components (see design choice above)- 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 []) = ("[]","\"\"")

- this is not allowed: (see open issue above, iavor thinks GHC tried this and it was really tricky)
f (C []) = True

- desugaring...
f (C []) = e1 -- illegal

f x = case x of C [] -> e 1 -- illegal _ -> error ...

would desugar tocase x of C y -> case y of -- NOT illegal [] -> e1 _ -> error... _ -> error...

which is a little funny.- when you match on
- where is explanation of type checking...
- where to put the bangs in strict polymorphic fields, hugs and GHC differ - can't figure it out in Hugs