(New page: Impredicative types are to be contrasted with rank-N types. A standard Haskell type is universally quantified by default, and quantifiers can only appear at the top level of a type or...)
(Rewrite most of the article)
|(6 intermediate revisions by one user not shown)|
Revision as of 16:43, 4 January 2013
Impredicative types are an advanced form of polymorphism, to be contrasted with rank-N types.
Standard Haskell allows polymorphic types via the use of type variables, which are understood to be universally quantified: id :: a -> a means "for all types a, id can take an argument and return a result of that type". All universal quantifiers ("for all"s) must appear at the beginning of a type.
Higher-rank polymorphism (e.g. rank-N types) allows universal quantifiers to appear inside function types as well. It turns out that appearing to the right of function arrows is not interesting: Int -> forall a. a -> [a] is actually the same as forall a. Int -> a -> [a]. However, higher-rank polymorphism allows quantifiers to the left of function arrows, too, and (forall a. [a] -> Int) -> Int really is different from forall a. ([a] -> Int) -> Int.
Impredicative types take this idea to its natural conclusion: universal quantifiers are allowed anywhere in a type, even inside normal datatypes like lists or Maybe. The GHC User's Guide gives the following example:
f :: Maybe (forall a. [a] -> [a]) -> Maybe ([Int], [Char]) f (Just g) = Just (g , g "hello") f Nothing = Nothing
However, impredicative types do not mix very well with Haskell's type inference, so to actually use the above function with latest GHC you need to specify the full (unpleasant) type signature for the Just constructor:
ghci> f ((Just :: (forall a. [a] -> [a]) -> Maybe (forall a. [a] -> [a])) reverse) Just (,"olleh")
Other examples are more successful: see below.