平等模式匹配

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 就会调用一个定理证明器，它将为我们传播该等式。这是 "pleasure" 部分。

"pain" 部分在于没有完整的依赖类型。我们在 Haskell 中并没有真正的 f : (x : T) -> ...。如果x是全称量化，那么它一定是Haskell中的一个类型，而且会在运行时被擦除，所以我们不能直接对它进行模式匹配。我们必须使用单例和其他技术。另外，在 Haskell 中我们不能写 g : (h : *->*) (x : *) -> h x -> ... 并传递前两个参数来生成 h x = Int。为此，h 需要是类型级函数，例如g (\t:* -> t) Int 42，但我们没有。但是，缺少此功能大大简化了 "pleasure" 部分，并且类型擦除使语言更高效（即使我们应该可以选择避免擦除，使用 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。要玩这个 "trick" 我们需要两个不同的变量。

原始代码的问题在于 m 和 n 中同一变量 n 多次出现。这使得依赖匹配将 both 替换为 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
.

平等模式匹配

Pattern Match on Equality

haskell

dependent-type

idris