Version 14 (modified by 11 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.

- is
*forall*a keyword? in what cases? (In types? In identifiers?)f forall = forall

- Hugs treats forall as a reserved keyword, whereas GHC only treats it specially in types.

- syntax
- change "atype" or modify specific sections?
- 4.2.1 - syntax in "Algebreic Datatype Declarations", add
*forall*to various bits. - 4.2.3 - syntax in "Datatype Renaming"
*newtype*declarations

- 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