Difference between revisions of "Rank-N types"
(Encoding of existentials in terms of higher rank types) |
|||
(12 intermediate revisions by 6 users not shown) | |||
Line 1: | Line 1: | ||
[[Category:Language extensions]] |
[[Category:Language extensions]] |
||
+ | |||
+ | {{GHCUsersGuide|exts/rank_polymorphism||an Arbitrary Rank Polymorphism section}} |
||
== 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 |
||
⚫ | |||
− | |||
⚫ | |||
− | |||
implies that the type variables are universally quantified like so: |
implies that the type variables are universally quantified like so: |
||
⚫ | |||
− | |||
− | <hask>forall |
+ | <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: |
||
− | |||
⚫ | |||
− | |||
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 27: | 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 (fromList 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 33: | Line 72: | ||
In general, you can replace |
In general, you can replace |
||
⚫ | |||
+ | (where <hask>e1..ek</hask> are types in terms of <hask>a1..ai</hask> and <hask>t1..tj</hask>) |
||
⚫ | |||
⚫ | |||
− | |||
⚫ | |||
− | < |
+ | <haskell>case e of (Constructor pat1 .. patk) -> res</haskell> |
with |
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> |
− | == |
+ | == See also == |
− | [ |
+ | * [https://gitlab.haskell.org/haskell/prime/-/wikis/RankNTypes Rank-N types] on the [[Haskell']] website. |
+ | * {{GHCUsersGuide|exts/rank_polymorphism||a section on Arbitrary Rank Polymorphism}} |
Latest revision as of 13:33, 15 April 2024
The GHC Users Guide has an Arbitrary Rank Polymorphism section.
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 #-}
.
Church-encoded Lists
Church-encoded lists use RankNTypes too, as seen in a StackOverflow answer by sacundim:
-- | Laws:
--
-- > runList (fromList 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)
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
See also
- Rank-N types on the Haskell' website.
- The GHC Users Guide has a section on Arbitrary Rank Polymorphism.