Personal tools

Rank-N types

From HaskellWiki

(Difference between revisions)
Jump to: navigation, search
m (See also)
 
(4 intermediate revisions by 3 users not shown)
Line 1: Line 1:
 
[[Category:Language extensions]]
 
[[Category:Language extensions]]
 +
 +
{{GHCUsersGuide|glasgow_exts|arbitrary-rank-polymorphism|an Arbitrary Rank Polymorphism section}}
  
 
== About ==
 
== About ==
Line 21: Line 23:
 
Rank-2 or Rank-N types may be specifically enabled by the language extensions
 
Rank-2 or Rank-N types may be specifically enabled by the language extensions
 
<hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>.
 
<hask>{-# LANGUAGE Rank2Types #-}</hask> or <hask>{-# LANGUAGE RankNTypes #-}</hask>.
 +
 +
== Church-encoded Lists ==
 +
Church-encoded lists use RankNTypes too, as seen in [http://stackoverflow.com/a/15593349/849891 a StackOverflow answer by sacundim]:
 +
<haskell>
 +
-- | Laws:
 +
--
 +
-- > runList xs cons nil == xs
 +
-- > runList (fromList xs) f z == foldr f z xs
 +
-- > foldr f z (toList xs) == runList xs f z
 +
newtype ChurchList a =
 +
    ChurchList { runList :: forall r. (a -> r -> r) -> r -> r }
 +
 +
-- | Make a 'ChurchList' out of a regular list.
 +
fromList :: [a] -> ChurchList a
 +
fromList xs = ChurchList $ \k z -> foldr k z xs
 +
 +
-- | Turn a 'ChurchList' into a regular list.
 +
toList :: ChurchList a -> [a]
 +
toList xs = runList xs (:) []
 +
 +
-- | The 'ChurchList' counterpart to '(:)'.  Unlike 'DList', whose
 +
-- implementation uses the regular list type, 'ChurchList' abstracts
 +
-- over it as well.
 +
cons :: a -> ChurchList a -> ChurchList a
 +
cons x xs = ChurchList $ \k z -> k x (runList xs k z)
 +
 +
-- | Append two 'ChurchList's.  This runs in O(1) time.  Note that
 +
-- there is no need to materialize the lists as @[a]@.
 +
append :: ChurchList a -> ChurchList a -> ChurchList a
 +
append xs ys = ChurchList $ \k z -> runList xs k (runList ys k z)
 +
 +
-- i.e.,
 +
 +
nil = {- fromList [] = ChurchList $ \k z -> foldr k z []
 +
                  = -} ChurchList $ \k z -> z
 +
 +
singleton x = {- cons x nil = ChurchList $ \k z -> k x (runList nil k z)
 +
            = -} ChurchList $ \k z -> k x z
 +
 +
snoc xs x = {- append xs $ singleton x
 +
          = ChurchList $ \k z -> runList xs k (runList (singleton x) k z)
 +
          = -} ChurchList $ \k z -> runList xs k (k x z)
 +
</haskell>
  
 
== Relation to Existentials ==
 
== Relation to Existentials ==
Line 45: Line 90:
  
 
* [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].
+
* [https://downloads.haskell.org/~ghc/latest/docs/html/users_guide/glasgow_exts.html#arbitrary-rank-polymorphism The GHC User's Guide on higher-ranked polymorphism].

Latest revision as of 23:02, 13 November 2016


The GHC Users Guide has an Arbitrary Rank Polymorphism section.

Contents

[edit] 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 #-}
.

[edit] 2 Church-encoded Lists

Church-encoded lists use RankNTypes too, as seen in a StackOverflow answer by sacundim:

 
-- | Laws:
--
-- > runList xs cons nil == xs
-- > runList (fromList xs) f z == foldr f z xs
-- > foldr f z (toList xs) == runList xs f z
newtype ChurchList a = 
    ChurchList { runList :: forall r. (a -> r -> r) -> r -> r }
 
-- | Make a 'ChurchList' out of a regular list.
fromList :: [a] -> ChurchList a
fromList xs = ChurchList $ \k z -> foldr k z xs
 
-- | Turn a 'ChurchList' into a regular list.
toList :: ChurchList a -> [a]
toList xs = runList xs (:) []
 
-- | The 'ChurchList' counterpart to '(:)'.  Unlike 'DList', whose
-- implementation uses the regular list type, 'ChurchList' abstracts
-- over it as well.
cons :: a -> ChurchList a -> ChurchList a
cons x xs = ChurchList $ \k z -> k x (runList xs k z)
 
-- | Append two 'ChurchList's.  This runs in O(1) time.  Note that
-- there is no need to materialize the lists as @[a]@.
append :: ChurchList a -> ChurchList a -> ChurchList a
append xs ys = ChurchList $ \k z -> runList xs k (runList ys k z)
 
-- i.e.,
 
nil = {- fromList [] = ChurchList $ \k z -> foldr k z []
                  = -} ChurchList $ \k z -> z
 
singleton x = {- cons x nil = ChurchList $ \k z -> k x (runList nil k z) 
            = -} ChurchList $ \k z -> k x z
 
snoc xs x = {- append xs $ singleton x
          = ChurchList $ \k z -> runList xs k (runList (singleton x) k z) 
          = -} ChurchList $ \k z -> runList xs k (k x z)

[edit] 3 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

[edit] 4 See also