你如何使用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表示嵌套类型？的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持！