Warum hängt diese Funktion die REPL?

Question

Kapitel 9 von Test-Driven Development with Idris präsentiert den folgenden Datentyp und removeElem Funktion.

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) 

Die folgenden Werke:

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

Aber wird folgender Aufruf noch nach ein paar Minuten laufen:

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

Warum dies, ich gehe davon aus, Kompilation so langsam ?

Answer 1

Der zweite Fall Ihrer removeElem liest

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

Die rechte Seite ist genau der gleiche wie der linken Seite; also divergiert Ihre Rekursion. Aus diesem Grund hängt die Bewertung ab.

Beachten Sie, dass Idris diesen Fehler gefangen haben würde, wenn Sie erklärt, dass removeElem insgesamt sein soll:

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) 

, die in der Kompilierung-

RemoveElem.idr Linie 9 col Fehler führt 0:

Main.removeElem ist möglicherweise nicht insgesamt aufgrund rekursiver Pfad