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

我正在尝试使用类似于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减少时，只是d!由于我尚未准备好eta-reducer，因此我执行了以下“无用识别”功能:

λ n: Nat ->

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

(n Nat Succ Zero)

现在，通过将这个无用的id应用于n的每一次出现，我将其“取消eta”设置，从而验证了证明。我想对这里发生的事情有任何了解。这个“无用的id”功能是书写证明上已知/使用的模式吗？为什么在没有这么多帮助的情况下，构造演算无法对这种证明进行类型检查？在这种现象背后是否有任何深层的推理，或者仅仅是事物在没有特殊原因的情况下发生了？

最佳答案

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

按Ulf Norell's thesis第22页中的说明进行类型导向，并在Agda中使用

未定型，如Coq AFAIK中使用的

在我们的案例中，无类型eta转换对于函数来说是完整的，并且比带类型的版本更简单，更快(在中性应用程序中无需重新计算或缓存类型)。该算法是这样的:

我们首先检查两个值都照常为lambda的情况。但是，此后，当只有一侧为lambda时，我们还要检查另外两种情况。在这些情况下，我们将lambda主体应用于新的泛型变量(照常)，还将另一个项应用于相同的变量，并检查结果值的相等性。

仅此而已!它实际上非常简单，并且没有太多的性能成本。请注意，我们不需要实现eta缩减或强eta标准化，因为eta转换检查很容易在运行时对弱磁头正常值进行。

关于haskell - 通常将变量包装在无用的 `id`调用中，以避免证明中的eta转换问题？，我们在Stack Overflow上找到一个类似的问题：https://stackoverflow.com/questions/41905759/