# Difference between revisions of "Impredicative types"

Benmachine (talk | contribs) (Rewrite most of the article) |
(Fix a broken link) |
||

(One intermediate revision by one other user not shown) | |||

Line 13: | Line 13: | ||

</haskell> |
</haskell> |
||

− | However, impredicative types do not mix very well with Haskell's type inference, so to actually use the above function with |
+ | However, impredicative types do not mix very well with Haskell's type inference, so to actually use the above function with GHC 7.6.1 you need to specify the full (unpleasant) type signature for the <tt>Just</tt> constructor: |

<haskell> |
<haskell> |
||

Line 24: | Line 24: | ||

=== See also === |
=== See also === |
||

− | * [ |
+ | * [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#impredicative-polymorphism The GHC User's Guide on impredicative polymorphism]. |

* [http://augustss.blogspot.co.uk/2011/07/impredicative-polymorphism-use-case-in.html A Pythonesque EDSL that makes use of impredicative polymorphism] |
* [http://augustss.blogspot.co.uk/2011/07/impredicative-polymorphism-use-case-in.html A Pythonesque EDSL that makes use of impredicative polymorphism] |
||

* [http://stackoverflow.com/a/14065493/812053 A writeup of where ImpredicativePolymorphism is used in a GHC plugin to store a lookup table of strings to polymorphic functions] |
* [http://stackoverflow.com/a/14065493/812053 A writeup of where ImpredicativePolymorphism is used in a GHC plugin to store a lookup table of strings to polymorphic functions] |

## Latest revision as of 12:29, 30 December 2016

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 [3], 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 GHC 7.6.1 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 ([3],"olleh")
```

Other examples are more successful: see below.