|Version 4 (modified by ross@…, 10 years ago) (diff)|
Types of data constructor arguments are allowed local universal quantification (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
- From Hindley-Milner Types to First-Class Structures by Mark P. Jones, Haskell Workshop, 1995.
- type inference seems to be a simple extension of Hindley-Milner.
- large increment in expressiveness: types become impredicative, albeit with an intervening data constructor, enabling Church encodings and similar System F tricks.
- used by the ReadP type.
- more complex denotational semantics