平等模式匹配

Question

我是伊德里斯的新手.我之前使用过一点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:当在rightIdentityAlt中检查IdrisBinary.case块的左侧时,在idris_binary.idr:20:31:统一y并加上y Z将导致无限值

大致相当的GHC haskell代码做了类型检查.如果我改为使用以下内容,我可以将Idris版本改为typecheck:

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不起作用.模式匹配=并没有像我期望的那样将证据纳入范围.有没有办法让它做到这一点,或者在伊德里斯这种方法是否存在根本性的错误？

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
.