這個函數爲什麼會掛起REPL？

Question

Test-Driven Development with Idris的第9章介紹了以下數據類型和removeElem函數。

import Data.Vect 

data MyElem : a -> Vect k a -> Type where 
    MyHere : MyElem x (x :: xs) 
    MyThere : (later : MyElem x xs) -> MyElem x (y :: xs) 

-- I slightly modified the definition of this function from the text. 
removeElem : (value : a) -> (xs : Vect (S n) a) -> (prf : MyElem value xs) -> Vect n a 
removeElem value (value :: ys) MyHere   = ys 
removeElem value (y :: ys) (MyThere later) = removeElem value (y :: ys) (MyThere later) 

以下工作：

*lecture> removeElem 1 [1,2,3] MyHere 
[2, 3] : Vect 2 Integer 

但是，下面的調用仍然在幾分鐘後運行：

*lecture> removeElem 2 [1,2,3] (MyThere MyHere) 

這是爲什麼，我假設，編譯這麼慢？

Answer 1

您removeElem的第二種情況下讀取

removeElem value (y :: ys) (MyThere later) = removeElem value (y :: ys) (MyThere later) 

的右手邊是完全一樣的左側;所以你的遞歸分歧。這就是評估掛起的原因。

請注意，如果你宣佈removeElem應占總伊德里斯會抓住了這個錯誤：

total removeElem : (value : a) -> (xs : Vect (S n) a) -> (prf : MyElem value xs) -> Vect n a 
removeElem value (value :: ys) MyHere   = ys 
removeElem value (y :: ys) (MyThere later) = removeElem value (y :: ys) (MyThere later) 

這會導致編譯時錯誤

RemoveElem.idr線9山坳0：

Main.removeElem由於遞歸路徑可能不是全部Main.removeElem