Personal tools

Impredicative types

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(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...)
 
(See also)
(5 intermediate revisions by one user not shown)
Line 1: Line 1:
Impredicative types are to be contrasted with [[rank-N types]].
+
Impredicative types are an advanced form of polymorphism, 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 to the right of function arrows.
 
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.
Line 13: Line 13:
 
</haskell>
 
</haskell>
   
Impredicative types are enabled in GHC with the <hask>{-# LANGUAGE ImpredicativeTypes #-}</hask> pragma. They are among the less well-used and well-tested language extensions, and so some caution is advised in their use. They are rarely needed in practice.
+
Impredicative types are enabled in GHC with the <hask>{-# LANGUAGE ImpredicativeTypes #-}</hask> pragma. They are among the less well-used and well-tested language extensions, and so some caution is advised in their use.
   
 
=== See also ===
 
=== See also ===
   
* [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#impredicative-polymorphism The GHC User's Guide on impredicative polymorphism].
+
* [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.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://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]]

Revision as of 23:19, 29 December 2012

Impredicative types are an advanced form of polymorphism, 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 to the right of function arrows.

A higher-rank 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.

An impredicative type, on the other hand, allows universal quantifiers anywhere: in particular, may contain ordinary datatypes with polymorphic components. 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
Impredicative types are enabled in GHC with the
{-# LANGUAGE ImpredicativeTypes #-}
pragma. They are among the less well-used and well-tested language extensions, and so some caution is advised in their use.

See also