Personal tools

Rank-N types

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
(a real description of rank n types)
m (→See also)
(4 intermediate revisions not shown.)
Line 1: Line 1:
[[Category:Language extensions]]
[[Category:Language extensions]]
-
[[Category:Stub articles]]
 
== About ==
== About ==
Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as
Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as
-
 
+
<haskell>a -> b -> a</haskell>
-
<hask>a -> b -> a</hask>
+
-
 
+
implies that the type variables are universally quantified like so:
implies that the type variables are universally quantified like so:
-
 
+
<haskell>forall a b. a -> b -> a</haskell>
-
<hask>forall a b. a -> b -> a</hask>
+
<hask>forall</hask> can be floated out of the right-hand side of <hask>-></hask> if it appears there, so:
-
 
+
<haskell>forall a. a -> (forall b. b -> a)</haskell>
-
<hask>forall</hask> can be floated out of the right-hand side of <hask>(->)</hask> if it appears there, so:
+
-
 
+
-
<hask>forall a. a -> (forall b. b -> a)</hask>
+
-
 
+
is also a Rank-1 type because it is equivalent to the previous signature.
is also a Rank-1 type because it is equivalent to the previous signature.
Line 29: Line 22:
<hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>.
<hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>.
 +
== Relation to Existentials ==
 +
 +
In order to unpack an existential type, you need a polymorphic function that works on any type that could be stored in the existential. This leads to a natural relation between higher-rank types and existentials; and an encoding of existentials in terms of higher rank types in continuation-passing style.
 +
 +
In general, you can replace
 +
<haskell>data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek</haskell>
 +
(where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>)
 +
 +
<haskell>Constructor exp1 .. expk -- application of the constructor</haskell>
 +
 +
<haskell>case e of (Constructor pat1 .. patk) -> res</haskell>
 +
 +
with
 +
 +
<haskell>data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 -> e2 -> ... -> ek -> b) -> b)</haskell>
 +
 +
<haskell>Constructor' (\f -> f exp1 .. expk)</haskell>
 +
 +
<haskell>case e of (Constructor' f) -> let k pat1 .. patk = res in f k</haskell>
-
== Also see ==
+
== See also ==
-
[http://hackage.haskell.org/trac/haskell-prime/wiki/RankNTypes Rank-N types] on the Haskell' website.
+
* [http://hackage.haskell.org/trac/haskell-prime/wiki/RankNTypes Rank-N types] on the Haskell' website.
 +
* [http://www.haskell.org/ghc/docs/latest/html/users_guide/other-type-extensions.html#universal-quantification The GHC User's Guide on higher-ranked polymorphism].

Revision as of 01:04, 6 September 2012


1 About

Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as 

a -> b -> a

implies that the type variables are universally quantified like so: 

forall a b. a -> b -> a
forall
can be floated out of the right-hand side of
->
if it appears there, so: 
forall a. a -> (forall b. b -> a)

is also a Rank-1 type because it is equivalent to the previous signature.

However, a
forall
appearing within the left-hand side of
(->)
cannot be moved up, and therefore forms another level or rank. The type is labeled "Rank-N" where N is the number of
forall
s which are nested and cannot be merged with a previous one. For example:
(forall a. a -> a) -> (forall b. b -> b)
is a Rank-2 type because the latter
forall
can be moved to the start but the former one cannot. Therefore, there are two levels of universal quantification.

Rank-N type reconstruction is undecidable in general, and some explicit type annotations are required in their presence.

Rank-2 or Rank-N types may be specifically enabled by the language extensions

{-# LANGUAGE Rank2Types #-}
or
{-# LANGUAGE RankNTypes #-}
.

2 Relation to Existentials

In order to unpack an existential type, you need a polymorphic function that works on any type that could be stored in the existential. This leads to a natural relation between higher-rank types and existentials; and an encoding of existentials in terms of higher rank types in continuation-passing style.

In general, you can replace 

data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek
(where
e1..ek
are types in terms of
a1..ai
and
t1..tj
) 
Constructor exp1 .. expk -- application of the constructor
case e of (Constructor pat1 .. patk) -> res

with 

data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 -> e2 -> ... -> ek -> b) -> b)
Constructor' (\f -> f exp1 .. expk)
case e of (Constructor' f) -> let k pat1 .. patk = res in f k

3 See also

Retrieved from "http://www.haskell.org/haskellwiki/Rank-N_types"

Category: Language extensions