On 11/1/10 6:28 PM, Andrew Coppin wrote:
The other day, I accidentally came up with this:
|{-# LANGUAGE RankNTypes #-}
type Either x y= forall r. (x -> r) -> (y -> r) -> r
left :: x -> Either x y
left x f g= f x
right :: y -> Either x y
right y f g= g y
|
This is one example; it seems that just about any algebraic type can be
encoded this way. I presume that somebody else has thought of this
before. Does it have a name?
Depending on how you mean for it to interact with recursion there are
different names. Church encoding has already been mentioned, the other
big one is Scott encoding. To illustrate the difference:
-- Note how the recursive site is @r@
newtype ChurchList a =
CL { foldrCL :: forall r. r -> (a -> r -> r) -> r }
churchNil :: forall a. ChurchList a
churchNil = CL $ \n c -> n
churchCons :: forall a. a -> ChurchList a -> ChurchList a
churchCons x xs = CL $ \n c -> c x (foldrCL xs n c)
churchFoldr :: forall a b. b -> (a->b->b) -> ChurchList a -> b
churchFoldr n c xs = foldrCL xs n c
-- Note how the recursive site is @ScottList a@
newtype ScottList a =
SL { caseSL :: forall r. r -> (a -> ScottList a -> r) -> r }
scottNil :: forall a. ScottList a
scottNil = SL $ \n c -> n
scottCons :: forall a. a -> ScottList a -> ScottList a
scottCons x xs = SL $ \n c -> c x xs
scottFoldr :: forall a b. b -> (a->b->b) -> ScottList a -> b
scottFoldr n c xs = caseSL xs n (\x xs' -> c x (scottFoldr n c xs'))
While the Church encodings seem to be more popular in general, Scott
encodings can be seen in /Data Types and Pattern Matching by Function
Application/ [1]. The authors of [1] erroneously claim that the Scott
encodings cannot be typed in Haskell--- though to be fair, the use of
newtypes is requisite for Scott encodings (because the type is infinite)
whereas we can use a type alias for Church encodings if desired. As
Wikipedia says[2], the well-typedness of Scott encodings is not nearly
as straightforward as the well-typedness of Church encodings. Both
require full System F (i.e., -XRankNTypes), but Scott encodings also
require recursive definitions both at the type level (i.e., newtypes to
box off the recursive structure of the infinite type term) and at the
value level (in order to define the catamorphisms).
The Church vs Scott perspectives on recursion can also be seen in the
duality of build/foldr vs unfoldr/destroy list fusion, and has
connections to the iterator/data pull-model vs the iteratee/enumerator
push-model.
Other than the specific encodings, this sort of thing is usually just
called "a CPS transformation". Which isn't very informative.
[1] http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.76.5557
[2] http://en.wikipedia.org/wiki/Mogensen–Scott_encoding
--
Live well,
~wren
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe@haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe
