How do you represent nested types using the Scott Encoding?

3
votes

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?

2
haskellfunctional-programminglambda-calculusalgebraic-data-typesscott-encoding
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. – chi

2 Answers

4
votes

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.

4
votes

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.