|Version 2 (modified by loeh@…, 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])
- 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 step in expressiveness: types become impredicative, albeit with an intervening data constructor, enabling Church encodings and similar System F tricks. The very useful Rank2Types can be viewed as syntactic sugar (and therefore a safe next step).
- used by ReadP type.
- more complex denotational semantics