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

Posted 2023-02-24

【中文标题】多态编码的递归代数数据类型的值是多少？

【英文标题】：What are the values of a polymorphically encoded recursive algebraic data type?

【发布时间】：2014-08-15 17:35:14

【问题描述】：

以下问题与Recursive algebraic data types via polymorphism in 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

Q: 是否所有类型的项都是Bool 或Nat 或上述形式的任何其他潜在递归代数数据类型（以这种方式编码），直至操作语义的一些简化规则?

示例 1（自然数）： forall t. t -> (t -> t) -> t 类型的任何术语在某种意义上是否与 \ x0 f -> f (f ( ... (f x0) ... )) 形式的术语“等效”？ p>

示例 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？

【参考方案1】：

在系统 F (AKA λ2) 中，∀α.α→α→α 的所有居民确实 λ 等于 K 或 K*。

首先，如果M : ∀α.α→α→α，那么它有范式N（因为系统F正在归一化）并且通过主题归约定理（参见Barendregt: Lambda calculi with types）还有N : ∀α.α→α→α。

让我们来看看这些正常形式的外观。 （我们将使用 λ2 的生成引理，有关正式细节，请参阅 Barendregt 的书。）

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

对于N 的情况，必须至少有一个 λ，因为最初我们在键入上下文中没有任何变量绑定来代替y。所以N = λx.U 和x:α |- U:α→α。

现在在U 的情况下必须至少有一个λ，因为如果U 只是y P1 ... Pk 那么y 将有一个函数类型（即使对于k=0，我们也需要@ 987654343@)，但上下文中只有x:α。所以N = λxy.V 和x:α, y:α |- V:α。

但是V 不能是λ..，因为那样它就会有函数类型τ→σ。所以V 必须是z P1 ... Pk 的形式，但是由于我们在上下文中没有任何函数类型的变量，k 必须为0，因此V 只能是x 或@987654355 @。

因此，∀α.α→α→α 类型的正常形式中只有两个术语：λxy.x 和 λxy.y，并且此类型的所有其他术语都 β 等于其中之一。

---

使用类似的推理，我们可以证明∀α.α→(α→α)→α 的所有居民都β-等于教堂数字。 （而且我认为对于∀α.(α→α)→α→α 类型，情况稍差；我们还需要η-相等，因为λf.f 和λfx.fx 对应于1，但不是β-相等，只是βη-相等。 )

【讨论】：

亲爱的彼得 - 谢谢你的回答，很抱歉我花了很长时间才回复！您是否从您的术语中省略了多态抽象和应用程序？在我看来，人们必须考虑范式形式，其主要抽象可能在术语和类型抽象之间交替，以及这些抽象中的(y P1 ... Pk) [T] 等应用术语。但是，这似乎不会在您的论点中引起任何严重的并发症。

@Hanno 我的答案是针对没有任何类型注释或 Λ 的 System-F 的 Curry 风格版本。但我相信同样的论点也可以用于教会风格。我还推荐this answer，它给出了完全不同的证明——它没有表​​明只有两个正常形式的术语，但它表明布尔类型的所有术语都是extensionally equal到K和@987654366 @.

好的，谢谢！然而，我偶然发现 CoQ'Art 书中的一句话（前言中的 p.XII）让我感到困惑：关于递归类型的多态编码，它说“......，她 [Christine Mohring] 意识到'她使用的“禁止性”编码不尊重归纳类型的术语仅限于类型构造函数的组合的传统。多态 lambda 演算中的编码引入了寄生术语，使得无法表达适当的归纳原则。你知道这与你的答案有什么关系吗？

即（为什么）如果我们使用更具表现力的构造微积分，事情会崩溃吗？

@Hanno 这超出了我的知识范围。如果您发现了，请添加评论。

【参考方案2】：

如果我们忽略底部和unsafe 的东西，那么你唯一可以用函数a -> a 做的事情就是组合它们。然而，这并不能完全阻止我们使用有限的 f (f ( ... (f x0) ... )) 表达式：我们还有无限的组合 infty x f = f $ infty x f。

同样，唯一的非递归布尔值确实是\t _ -> t 和\_ f -> f，但你也可以在这里打结，比如

blarg t f = blarg (blarg t f) (blarg f t)

【讨论】：

感谢您的回答！我应该更准确一点，因为我希望这些术语存在于 System F 中，这样就消除了递归的可能性。