How do you represent nested types using the Scott Encoding?

Question

An ADT can be represented using the Scott Encoding by replacing products by tuples and sums by matchers. For example:

data List a = Cons a (List a) | Nil

Can be encoded using the Scott Encoding as:

cons = (λ h t c n . c h t)
nil  = (λ c n . n)

But I couldn't find how nested types can be encoded using SE:

data Tree a = Node (List (Tree a)) | Leaf a

How can it be done?

Mckeon

I am not sure, but I think it's encoded in the same way you would encode data Tree a = Node a | Leaf a, i.e. node = (λ x n l. n x), etc. After all, the list encoding didn't care about the recursive reference -- the encoding is the same as for data List a = Cons a a | Nil. Still, I am not familiar enough with SE to write an actual answer. – Plating

Answer 1

If the Wikipedia article is correct, then

data Tree a = Node (List (Tree a)) | Leaf a

has Scott encoding

node = λ a . λ node leaf . node a
leaf = λ a . λ node leaf . leaf a

It looks like the Scott encoding is indifferent to (nested) types. All it's concerned with is delivering the correct number of parameters to the constructors.

Envelope

Answer 2

Scott encodings are basically representing a T by the type of its case expression. So for lists, we would define a case expression like so:

listCase :: List a -> r -> (a -> List a -> r) -> r
listCase []     n c = n
listCase (x:xs) n c = c x xs

this gives us an analogy like so:

case xs of { [] -> n ; (x:xs) -> c }
=
listCase xs n (\x xs -> c)

This gives a type

newtype List a = List { listCase :: r -> (a -> List a -> r) -> r }

The constructors are just the values that pick the appropriate branches:

nil :: List a
nil = List $ \n c -> n

cons :: a -> List a -> List a
cons x xs = List $ \n c -> c x xs

We can work backwards then, from a boring case expression, to the case function, to the type, for your trees:

case t of { Leaf x -> l ; Node xs -> n }

which should be roughly like

treeCase t (\x -> l) (\xs -> n)

So we get

treeCase :: Tree a -> (a -> r) -> (List (Tree a) -> r) -> r
treeCase (Leaf x)  l n = l x
treeCase (Node xs) l n = n xs

newtype Tree a = Tree { treeCase :: (a -> r) -> (List (Tree a) -> r) -> r }

leaf :: a -> Tree a
leaf x = Tree $ \l n -> l x

node :: List (Tree a) -> Tree a
node xs = Tree $ \l n -> n xs

Scott encodings are very easy tho, because they're only case. Church encodings are folds, which are notoriously hard for nested types.

Adair