多态编码的递归代数数据类型的值是什么？

Question

以下问题涉及Haskell中通过多态的递归代数数据类型.

递归代数数据类型可以使用通用参数多态在具有System F功能的任何语言中实现.例如,可以引入自然数的类型(在Haskell中)

newtype Nat = Nat { runNat :: forall t. (t -> (t -> t) -> t) }

将"通常"的自然数表n实现为

\ x0 f -> f(f(...(f x0)...))

使用n迭代f.

同样,布尔的类型也可以作为

newtype Bool = Bool { runBool :: forall t. t -> t -> t }

预期值'true'和'false'被实现为

true = \ t f -> t
false = \ t f -> f

问:上述形式的所有类型Bool或Nat任何其他可能的递归代数数据类型(以这种方式编码)是否都达到了操作语义的一些约简规则？

示例1(自然数):forall t. t -> (t -> t) -> t在某种意义上,任何类型的术语是否与形式的术语相同\ x0 f -> f (f ( ... (f x0) ... ))？

例2(布尔):forall t. t -> t -> t在某种意义上,任何类型的"等价"都是\ t f -> t或者\ t f -> f？

附录(内部版本):如果所考虑的语言甚至能够表达命题平等,这个元数学问题可以内化如下,如果有人想出一个解决方案,我会很高兴:

对于任何仿函数,m我们可以在其上定义通用模块和一些解码编码功能,如下所示:

type ModStr m t = m t -> t
UnivMod m = UnivMod { univProp :: forall t. (ModStr m t) -> t }

classifyingMap :: forall m. forall t. (ModStr m t) -> (UnivMod m -> t)
classifyingMap f = \ x -> (univProp x) f

univModStr :: (Functor m) => ModStr m (UnivMod m)
univModStr = \ f -> UnivMod $ \ g -> g (fmap (classifyingMap g) f)

dec_enc :: (Functor m) => UnivMod m -> UnivMod m
dec_enc x = (univProp x) univModStr

问:如果语言能够表达这种情况:是否存在平等类型dec_enc = id？

Answer 1

在系统 F（又称为 \xce\xbb2）中， 的所有居民\xe2\x88\x80\xce\xb1.\xce\xb1\xe2\x86\x92\xce\xb1\xe2\x86\x92\xce\xb1实际上都等于K或K*。

\n\n

首先，如果M : \xe2\x88\x80\xce\xb1.\xce\xb1\xe2\x86\x92\xce\xb1\xe2\x86\x92\xce\xb1那么它具有范式N（因为系统 F 正在标准化）并且通过主题归约定理（参见Barendregt：具有类型 的 Lambda 演算）N : \xe2\x88\x80\xce\xb1.\xce\xb1\xe2\x86\x92\xce\xb1\xe2\x86\x92\xce\xb1。

\n\n

让我们看看这些范式是什么样子的。（我们将使用 \xce\xbb2 的生成引理，有关正式详细信息，请参阅 Barendregt\ 的书。）

\n\n

如果N是范式，则 that N（或其任何子表达式）必须采用头范式，即 形式的表达式\xce\xbbx1 ... xn. y P1 ... Pk，其中n和/或k也可以为 0。

\n\n

对于 的情况N，必须至少有一个 \xce\xbb，因为最初我们在打字上下文中没有绑定任何可以代替 的变量y。所以N = \xce\xbbx.U和x:\xce\xb1 |- U:\xce\xb1\xe2\x86\x92\xce\xb1.

\n\n

现在，在 的情况下，必须至少有一个 \xce\xbb U，因为 if Uwere 则将y P1 ... Pk具有y函数类型（即使对于 k=0 我们也需要y:\xce\xb1\xe2\x86\x92\xce\xb1），但我们只是x:\xce\xb1在上下文中。所以N = \xce\xbbxy.V和x:\xce\xb1, y:\xce\xb1 |- V:\xce\xb1.

\n\n

但V不可能是\xce\xbb..，因为那样它就会有函数类型\xcf\x84\xe2\x86\x92\xcf\x83。所以V必须是 的形式z P1 ... Pk，但由于我们在上下文中没有任何函数类型的变量，所以k必须是 0，因此V只能是x或y。

\n\n

\xe2\x88\x80\xce\xb1.\xce\xb1\xe2\x86\x92\xce\xb1\xe2\x86\x92\xce\xb1因此，类型: and的正常形式中只有两个项，\xce\xbbxy.x并且\xce\xbbxy.y该类型的所有其他项都 \xce\xb2 - 等于其中之一。

\n\n\n\n

使用类似的推理，我们可以证明\xe2\x88\x80\xce\xb1.\xce\xb1\xe2\x86\x92(\xce\xb1\xe2\x86\x92\xce\xb1)\xe2\x86\x92\xce\xb1\xce\xb2 的所有居民都等于 Church 数字。（而且我认为对于 type 来说，\xe2\x88\x80\xce\xb1.(\xce\xb1\xe2\x86\x92\xce\xb1)\xe2\x86\x92\xce\xb1\xe2\x86\x92\xce\xb1情况稍微糟糕一些；我们还需要 \xce\xb7-equality，因为\xce\xbbf.f和\xce\xbbfx.fx对应于1，但不是 \xce\xb2-equal，只是 \xce\xb2\xce\xb7-平等的。）

\n