「有」在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節中如何工作？

回答

相關問題