idris - idris 教程第 11 页第 3.4.4 节中的 "There"是如何工作的？

Question

这里是教程中的示例，为简单起见稍作修改:

data Vect : Nat -> (b:Type) -> Type where
  Nil : Vect Z a
  (::) : a -> Vect k a -> Vect (S k) a

data Elem : a -> Vect n a -> Type where
  Here : {x:a} -> {xs:Vect n a} -> Elem x (x :: xs)
  There : {x,y:a} -> {xs:Vect n a} -> Elem x xs -> Elem x (y :: xs)

testVec : Vect 4 Int
testVec = 3 :: 4 :: 5 :: 6 :: Nil
inVect : Elem 4 testVec
inVect = There Here

我无法理解 There 如何验证该值是否正确。据我了解，There 就像一个函数，所以它需要Here类型的元素，填空时对应Elem 3 testVec，然后设置testVec的第一个值为 y，其余为 xs。但是由于 y 没有在任何地方使用，所以我希望除此之外不会造成任何限制。

然而，当我尝试

inVectBroken : Elem 2 testVec
inVectBroken = There Here

我得到一个错误:

When checking an application of constructor There:
Type mismatch between
        Elem x (x :: xs) (Type of Here)
and
        Elem 2 [4, 5, 6] (Expected type)

Specifically:
        Type mismatch between
                2
        and
                4

谁能给我解释一下上面的代码是如何(神奇地？)将 There 限制在 Vect 的尾部的？

Answer 1

这里4(x::xs)证明4在(x::xs)的头部，所以x = 4。 There 需要一个证明 Elem 4 xs 证明 4 在 xs 中，所以证明 Elem 4 (y::xs)，那个 4 仍然在扩展列表的某个地方。这就是 y 的去向。 y 实际上是什么并不重要，它只是允许将证明扩展到更大的列表。例如:

in1 : Elem 4 (4 :: Nil)
in1 = Here

in2 : Elem 4 (3 :: 4 :: Nil)
in2 = There in1

in3 : Elem 4 (8 :: 4 :: Nil)
in3 = There in1

根据类型，您可以看到在整个证明中变化的不是元素 4，而是列表。