haskellfunctional-programminglambda-calculusalgebraic-data-typesscott-encoding

How do you represent nested types using the Scott Encoding?


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?


Solution

  • 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.