您如何使用 Scott 编码表示嵌套类型？

Question

ADT 可以使用 Scott 编码表示，方法是用元组替换乘积，用匹配器替换求和。例如：

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

可以使用 Scott 编码编码为：

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

但我找不到如何使用 SE 对嵌套类型进行编码：

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

如何做到？

Answer 1

如果Wikipedia article正确，则

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

有 Scott 编码

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

看起来 Scott 编码与（嵌套）类型无关。它所关心的只是将正确数量的参数传递给构造函数。

Answer 2

Scott 编码基本上是通过其 case 表达式的类型来表示 T。所以对于列表，我们会像这样定义一个 case 表达式：

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

这给了我们一个类比：

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

这给出了一个类型

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

构造函数只是选择适当分支的值：

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

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

然后我们可以倒退，从无聊的 case 表达式到 case 函数，再到类型，为您的树：

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

大致应该是这样的

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

所以我们得到

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 编码非常简单，因为它们仅大小写。 Church 编码是折叠，这对于嵌套类型来说是出了名的困难。

您如何使用 Scott 编码表示嵌套类型？

How do you represent nested types using the Scott Encoding?

haskell

functional-programming

lambda-calculus

algebraic-data-types

scott-encoding