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

Question

以下问题与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？

Answer 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，但不是β-相等，只是βη-相等。 )

Answer 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)