この機能が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は合計でなければなりませんと宣言した場合イドリスは、このエラーをキャッチしていることに注意してください：

：コンパイル時にエラーに

RemoveElem.idrライン9 COL 0を結果

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) 

Main.removeElemは、再帰パスのため合計ではない可能性がありますMain.removeElem