3

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

怎么做到呢?

4

2 回答 2

4

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

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

有斯科特编码

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

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

于 2015-06-05T04:47:00.067 回答
4

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

于 2015-06-05T13:34:59.743 回答