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

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 迭代。

类似地， bool 类型可以引入为

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

预期值“true”和“false”被实现为

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

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

示例 1(自然数):对于所有 t 来说，都是 类型的任何项。 t -> (t -> t) -> t 在某种意义上“等同于”\x0 f -> f (f ( ... (f x0) ... ))？

示例 2( bool 值): 是否为所有 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(又名 λ2)中，∀α.α→α→α 的所有居民确实 λ-等于 K或K* .

首先，如果 M : ∀α.α→α→α那么它的范式为 N (因为系统 F 正在标准化)并且通过主体归约定理(参见 Barendregt: Lambda calculi with types )也 N : ∀α.α→α→α .

让我们看看这些范式是什么样子的。 (我们将使用生成引理来表示 λ2，请参阅 Barendregt 的书了解正式细节。)

如果N是一个范式，即 N (或其任何子表达式)必须采用 head 范式，即 λx1 ... xn. y P1 ... Pk 形式的表达式，其中n和/或 k也可以是0。

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

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

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

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

<小时/>

使用类似的推理，我们可以证明 ∀α.α→(α→α)→α 的所有居民β-等于丘奇数。 (我认为对于 ∀α.(α→α)→α→α 类型，情况稍微糟糕一些；我们还需要 η-相等，因为 λf.f 和 λfx.fx 对应于 1 ，但不是 β 相等，只是 βη 相等。 )