“有”在idris教程，第11页，第3.4.4节中如何工作？

下面是本教程中，稍加修改简单的例子：“有”在idris教程，第11页，第3.4.4节中如何工作？

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尾（神奇？）？

来源

2016-01-21 redfish64

'There'的构造函数不会忽略向量的头部，因为您必须提供元素在尾部内的证明，即'Elem x xs'参数。你的错误信息是你不能构建一个'This 2 [4，5，6]'。 – Lee

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改变了整个证据，但该列表。

来源

2016-01-21 12:02:31 xash

“有”在idris教程，第11页，第3.4.4节中如何工作？

回答

相关问题