Difference between revisions of "Impredicative types"
Benmachine (talk  contribs) (→See also) 
(Fix a broken link) 

(7 intermediate revisions by one other user not shown)  
Line 1:  Line 1:  
−  Impredicative types are to be contrasted with [[rankN types]]. 
+  Impredicative types are an advanced form of polymorphism, to be contrasted with [[rankN types]]. 
−  A standard Haskell type is universally quantified by default, and quantifiers can only appear at the top level of a type or to the right of function arrows. 

+  Standard Haskell allows polymorphic types via the use of type variables, which are understood to be ''universally quantified'': <tt>id :: a > a</tt> means "''for all'' types <tt>a</tt>, <tt>id</tt> 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. 

−  A higherrank polymorphic type allows universal quantifiers to appear to the left of function arrows as well, so that function arguments can be functions that are themselves polymorphic. 

+  Higherrank polymorphism (e.g. [[rankN 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: <tt>Int > forall a. a > [a]</tt> is actually the same as <tt>forall a. Int > a > [a]</tt>. However, higherrank polymorphism allows quantifiers to the ''left'' of function arrows, too, and <tt>(forall a. [a] > Int) > Int</tt> really ''is'' different from <tt>forall a. ([a] > Int) > Int</tt>. 

−  +  Impredicative types take this idea to its natural conclusion: universal quantifiers are allowed ''anywhere'' in a type, even inside normal datatypes like lists or <tt>Maybe</tt>. The GHC User's Guide gives the following example: 

<haskell> 
<haskell> 

Line 13:  Line 13:  
</haskell> 
</haskell> 

−  Impredicative types are enabled in GHC with the <hask>{# LANGUAGE ImpredicativeTypes #}</hask> pragma. They are among the less wellused and welltested language extensions, and so some caution is advised in their use. They are rarely needed in practice. 

+  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> 

+  ghci> f ((Just :: (forall a. [a] > [a]) > Maybe (forall a. [a] > [a])) reverse) 

+  Just ([3],"olleh") 

+  </haskell> 

+  
+  Other examples are more successful: see below. 

=== See also === 
=== See also === 

−  * [ 
+  * [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#impredicativepolymorphism The GHC User's Guide on impredicative polymorphism]. 
+  * [http://augustss.blogspot.co.uk/2011/07/impredicativepolymorphismusecasein.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] 

+  
+  [[Category:Glossary]] 
Latest revision as of 12:29, 30 December 2016
Impredicative types are an advanced form of polymorphism, to be contrasted with rankN 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.
Higherrank polymorphism (e.g. rankN 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, higherrank 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.