Rank-N types

From HaskellWiki

Revision as of 12:40, 9 July 2007 (edit) MathematicalOrchid (Talk | contribs) m (+category) ← Previous diff		Revision as of 12:48, 26 August 2007 (edit) (undo) Mrd (Talk | contribs) (a real description of rank n types) Next diff →
Line 4:		Line 4:
	== About ==		== About ==
-	As best as I can tell, rank-N types are exactly like [[existential type]]s - except that they're completely different.	+	Normal Haskell '98 types are considered Rank-1 types. A Haskell '98 type signature such as
		+
		+	<hask>a -> b -> a</hask>
		+
		+	implies that the type variables are universally quantified like so:
		+
		+	<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:
		+
		+	<hask>forall a. a -> (forall b. b -> a)</hask>
		+
		+	is also a Rank-1 type because it is equivalent to the previous signature.
		+
		+	However, a <hask>forall</hask> appearing within the left-hand side of <hask>(->)</hask> cannot be moved up, and therefore forms another level or rank. The type is labeled "Rank-N" where N is the number of <hask>forall</hask>s which are nested and cannot be merged with a previous one. For example:
		+
		+	<hask>(forall a. a -> a) -> (forall b. b -> b)</hask>
		+
		+	is a Rank-2 type because the latter <hask>forall</hask> 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
		+	<hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>.
-	Rank-2 types are a special case of rank-N types, and normal Haskell 98 types are all rank-1 types.
	== 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 12:48, 26 August 2007

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 Also see

Rank-N types on the Haskell' website.

Categories: Language extensions | Stub articles