[Haskell-cafe] Mysterious fact

[wren ng thornton]

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