"有"在idris教程,第11页,第3.4.4节中如何工作？

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

Here 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在整个证明中而是在列表中发生变化.