Idris样张中的案例分析

Question

所以我编写了以下类型来证明Integers的一些属性：

data Number : Type where
    PosN : Nat -> Number
    Zero : Number
    NegN : Nat -> Number

plusPosNeg : Nat -> Nat -> Number
plusPosNeg n m with (cmp n m)
    plusPosNeg (k + S d) k  | CmpGT d = PosN d
    plusPosNeg k k          | CmpEQ = Zero
    plusPosNeg k (k + S d)  | CmpLT d = NegN d

plus : Number -> Number -> Number
plus Zero y = y
plus x Zero = x
plus (PosN k) (PosN j) = PosN (k + j)
plus (NegN k) (NegN j) = NegN (k + j)
plus (PosN k) (NegN j) = plusPosNeg k j
plus (NegN k) (PosN j) = plusPosNeg j k

现在我想证明Zero是加法的中性元素，这在plus的定义中非常明显。事实上，伊德里斯接受以下证据：

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l = Zero} = Refl
plusRZeroNeutral {l = PosN _} = Refl
plusRZeroNeutral {l = NegN _} = Refl

但拒绝我首先提出的更短版本：

plusRZeroNeutral : {l : Number} -> plus l Zero = l
plusRZeroNeutral {l} = Refl

我的问题是为什么会这样？看看plus的定义，似乎编译器应该知道只要左参数是plus（反之亦然），构造函数作为正确参数传递给Zero无关紧要。也许这是一个错误，或者我错过了什么？

Answer 1

如果你所知道的关于l的是它，那么，l（即一些任意参数），那么你不能再进一步减少plus l Zero，因为你被卡在plus的哪个分支上。

在例如模式匹配时l = Zero，右手边的类型现在被改进为plus Zero Zero = Zero，可以减少（通过plus的定义）到Zero = Zero。构造函数Refl的类型很容易与这个精炼的结果类型统一，因此条款plusRZeroNeutral {l = Zero} = Refl typechecks。

其他分支的处理类似于您对plusRZeroNeutral的第一个定义的其他条款。