haskell - 相等的模式匹配

Question

我对 idris 有点陌生。我之前用过一点agda，我在GHC Haskell方面有很深的背景。我试图理解为什么在 GHC Haskell 中有效的东西在 Idris 中无效。以下代码无法编译(idris 版本 0.12.3，nobuiltins，noprelude):

data Nat = S Nat | Z

plus : Nat -> Nat -> Nat
plus Z right        = right
plus (S left) right = S (plus left right)

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = case rightIdentityAlt y of
  Refl => Refl

这失败并出现以下错误:

idris_binary.idr:21:3-7:When checking left hand side of IdrisBinary.case block in rightIdentityAlt at idris_binary.idr:20:31: Unifying y and plus y Z would lead to infinite value

大致等效的 GHC haskell 代码会进行类型检查。如果我改为使用以下命令，我可以获得 Idris 版本来进行类型检查:

cong : (x : Nat) -> (y : Nat) -> (f : Nat -> Nat) -> x = y -> f x = f y
cong _ _ _ Refl = Refl

rightIdentity : (n : Nat) -> n = (plus n Z)
rightIdentity Z = Refl
rightIdentity (S x) = cong x (plus x Z) S (rightIdentity x)

我认为 rightIdentityAlt 的原因在 GHC Haskell 中工作，但在 Idris 中不工作，处理了两种语言中统一工作方式的差异。在 GHC Haskell 中，从 GADT 上的模式匹配中学到的统一只是到处传播，但在 Idris 中，您似乎需要使用 with 优化原始类型条款。这是我这样做的尝试:

rightIdentityAlt : (n : Nat) -> n = (plus n Z) 
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) with (rightIdentityAlt y) 
  rightIdentityAlt (S y) | Refl {A = Nat} {x = y} = Refl

爆破。还是不行。现在我们已经失去了我们最初试图证明的平等性:

idris_binary.idr:26:20:When checking left hand side of with block in IdrisBinary.rightIdentityAlt:
Type mismatch between
    plus y Z (Inferred value)
and
    y (Given value)
Holes: IdrisBinary.rightIdentityAlt

我知道务实的答案只是使用 cong 重写它。或者是涉及战术的东西，但我真的很想了解为什么我要写 rightIdentityAlt不起作用。 = 上的模式匹配没有像我期望的那样将证据纳入范围。有没有办法让它做到这一点，或者 idris 的这种方法有什么根本性的错误？

Answer 1

我认为这可能与 Hasochism 有关.

Lindley 和 McBride 使用 Hasochism 这个词来描述在 Haskell 中使用(伪)依赖类型(如 GADT)的痛苦和乐趣。在 Haskell 中，只要我们匹配 Refl , GHC 调用一个定理证明器，它将为我们传播该等式。这是“快乐”部分。

“痛苦”部分在于没有完全依赖类型。我们真的没有f : (x : T) -> ...在 haskell 。如果 x是普遍量化的，它必须是 Haskell 中的一个类型，并且会在运行时被删除，所以我们不能直接对其进行模式匹配。我们必须使用单例和其他技术。另外，在 Haskell 中我们不能写 g : (h : *->*) (x : *) -> h x -> ...并将前两个参数传递给 h x = Int .为此，h需要是类型级函数，例如g (\t:* -> t) Int 42 ，但我们没有这些。但是，缺少此功能极大地简化了“快乐”部分，并且类型删除使语言更加高效(即使我们应该可以选择避免删除，使用 pi 类型)，所以它还不错。

无论如何，在 Agda/Coq/Idris 中，除非你想使用一些自动魔法的东西(比如战术)，否则你必须编写自己的依赖消除，并将你的等式证明带到你需要它们的地方，例如使用您的 cong .

作为替代方案，这也编译:

rightIdentityAlt : (n : Nat) -> n = (plus n Z)
rightIdentityAlt Z = Refl
rightIdentityAlt (S y) = aux y (rightIdentityAlt y) 
  where
  aux : (m : Nat) -> m = plus n Z -> S m = plus (S n) Z
  aux _ Refl = Refl

注意最里面的函数 aux ，其中涉及两个变量 m和 n .在匹配 Refl 时这样做, 这导致替换 m与 plus n Z不影响 n .要玩这个“技巧”，我们需要两个不同的变量。

原始代码的问题是 m和 n ，有多次出现同一个变量 n .这使得依赖匹配替换为 S y ，并检查结果类型，这会触发错误。

就个人而言，我可以更好地理解 Coq 中的依赖模式匹配，您可以在其中使用 match .. return ...表示每个匹配的结果类型。此外，这是一个可以嵌套的表达式，不需要单独的定义。在这里，注释了一些注释，显示每个匹配项如何影响所需的类型。

Fixpoint rightIdentityAlt (n: nat): n = plus n O :=
   match n return n = plus n O with
   | O => (* required: n = plus n O with n := O
             hence   : O = plus O O *)
      eq_refl
   | S y =>  (* required: n = plus n O with n := S y
                hence   : S y = plus (S y) O *)
      match rightIdentityAlt y in _ = o return S y = S o with
      | eq_refl => (* required: S y = S o with o := y
                      hence   : S y = S y *)
         eq_refl
      end
   end
.