haskell - 是否通常将变量包装在无用的 `id` 调用中以避免证明上的 eta 转换问题？

Question

使用类似于 Morte/CoC 的语言，我试图证明简单的陈述 there are lists of arbitrary lengths .为此，我编写了以下类型:

∀ n:Nat ->
(ThereIs (List Nat)
  (Equal Nat 
    (List.length Nat l) 
    n)))

ThereIs是依赖对(Sigma)。一切都是教会编码的。为了证明这一点，我写了以下证明:

λ n:Nat ->
(ThereIs.this (List Nat)
  (λ l:(List Nat) -> (Equal Nat (List.length Nat l) n))
  (List.replicate Nat n Nat.Zero)
  (Equal.refl Nat n))

奇怪的是，我在 d 之间出现类型不匹配错误。 (即 Nat 类型的自由变量)和 λ c:* -> λ b:(c -> c) -> λ a:c -> (d c b a) .但是，当 eta-reduced 时，后期项只是 d !由于我没有准备好 eta-reducer，我改为使用以下“无用识别”功能:

λ n: Nat ->

λ Nat:* ->
λ Succ: (Nat -> Nat) ->
λ Zero: Nat ->

(n Nat Succ Zero)

现在，通过将那个无用的 id 应用于 n 的每一次出现，我“un-eta”它，导致证明检查。我想了解这里发生的事情。这个“无用的 id”函数是编写证明的已知/使用模式吗？为什么没有这个小帮助，构造演算就不能对这个证明进行类型检查？这种现象背后是否有任何深刻的原因，或者只是没有特殊原因，事情就是这样？

Answer 1

您需要将 eta 添加到您的转换检查算法中。这可以通过多种方式完成，最简单的两种是

Ulf Norell's thesis 的第 22 页中的类型导向并用于 Agda

在 Coq AFAIK

中使用的无类型

函数的无类型 eta 转换是完整的，在我们的例子中，它也比有类型的版本更简单和更快(不需要在中性应用程序中重新计算或缓存类型)。算法是这样的:

我们首先像往常一样检查两个值都是 lambda 的情况。然而，在那之后我们检查了另外两种情况，当只有一侧是 lambda 时。在这些情况下，我们将 lambda 主体应用于一个新的泛型变量(像往常一样)，并将另一个术语应用于同一变量，并检查结果值的相等性。

这就是全部!它实际上非常简单，并且没有太多的性能成本。请注意，我们不需要实现 eta 减少或强 eta 归一化，因为 eta 转换检查很容易在运行中对弱头正常值进行。