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
怎么做到呢?
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
怎么做到呢?
如果维基百科的文章是正确的,那么
data Tree a = Node (List (Tree a)) | Leaf a
有斯科特编码
node = λ a . λ node leaf . node a
leaf = λ a . λ node leaf . leaf a
看起来 Scott 编码与(嵌套)类型无关。它所关心的只是向构造函数提供正确数量的参数。
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 编码是折叠,这对于嵌套类型来说是出了名的难。