你如何使用Scott Encoding表示嵌套类型？ [英] How do you represent nested types using the Scott Encoding?

问题描述

ADT可以使用Scott编码通过用元组替换产品和匹配器产生的和来表示。例如：

An ADT can be represented using the Scott Encoding by replacing products by tuples and sums by matchers. For example:

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

可以使用Scott编码进行编码：

Can be encoded using the Scott Encoding as:

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

但我无法找到如何使用SE编码嵌套类型：

But I couldn't find how nested types can be encoded using SE:

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

如何做？

How can it be done?

推荐答案

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

If the Wikipedia article is correct, then

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

有Scott编码

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

看起来斯科特编码对于（嵌套）类型是无差别的。它所关心的是向构造函数提供正确数量的参数。

It looks like the Scott encoding is indifferent to (nested) types. All it's concerned with is delivering the correct number of parameters to the constructors.

这篇关于你如何使用Scott Encoding表示嵌套类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！