Rank-N types

From HaskellWiki

Revision as of 12:49, 26 August 2007 (edit) Mrd (Talk | contribs) m (not a stub) ← Previous diff		Revision as of 06:46, 11 November 2008 (edit) (undo) Ryani (Talk | contribs) (Encoding of existentials in terms of higher rank types) Next diff →
Line 28:		Line 28:
	<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
		+
		+	<hask>data T a1 .. ai = forall t1 .. tj. constraints => Constructor e1 .. ek</hask> (where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>)
		+
		+	<hask>Constructor exp1 .. expk -- application of the constructor</hask>
		+
		+	<hask>case e of (Constructor pat1 .. patk) -> res</hask>
		+
		+	with
		+
		+	<hask>data T' a1 .. ai = Constructor' (forall b. (forall t1..tj. constraints => e1 -> e2 -> ... -> ek -> b) -> b)</hask>
		+
		+	<hask>Constructor' (\f -> f exp1 .. expk)</hask>
		+
		+	<hask>case e of (Constructor' f) -> let k pat1 .. patk = res in f k</hask>
	== Also see ==		== Also see ==
	[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.

---

Revision as of 06:46, 11 November 2008

1 About

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

implies that the type variables are universally quantified like so:

can be floated out of the right-hand side of if it appears there, so:

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

However, a 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 s which are nested and cannot be merged with a previous one. For example: is a Rank-2 type because the latter 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

or .

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

(where are types in terms of and )

with

3 Also see

Rank-N types on the Haskell' website.

Category: Language extensions