haskell - 如何使用 Scott Encoding 表示嵌套类型？

Question

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

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

怎么做到呢？

Answer 1

如果维基百科的文章是正确的，那么

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

有斯科特编码

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

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

Answer 2

Scott 编码基本上是T通过其 case 表达式的类型来表示的。因此，对于列表，我们将定义一个 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

斯科特编码非常容易，因为它们只是案例。Church 编码是折叠，这对于嵌套类型来说是出了名的难。