如何使用 Scott Encoding 表示嵌套类型？答案

【问题标题】：How do you represent nested types using the Scott Encoding?如何使用 Scott Encoding 表示嵌套类型？
【发布时间】：2015-06-04 23:04:44
【问题描述】：

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

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

可以使用 Scott Encoding 编码为：

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

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

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

怎么做？

【问题讨论】：

我不确定，但我认为它的编码方式与您对data Tree a = Node a | Leaf a 的编码方式相同，即node = (λ x n l. n x) 等。毕竟，列表编码并不关心递归引用-- 编码与data List a = Cons a a | Nil 相同。不过，我对 SE 还不够熟悉，无法写出实际的答案。

标签： haskell functional-programming lambda-calculus algebraic-data-types scott-encoding

【解决方案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 编码与（嵌套）类型无关。它所关心的只是向构造函数传递正确数量的参数。

【讨论】：

【解决方案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 编码是折叠，这对于嵌套类型来说是出了名的难。

【讨论】：