Why does this function hang the REPL?

Question

Chapter 9 of Test-Driven Development with Idris presents the following data type and removeElem function.

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)

The following works:

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

But, the following call is still running after a few minutes:

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

Why is this, I'm assuming, compilation so slow?

Cactus Cactus · Accepted Answer · 2017-06-21T01:54:11

The second case of your removeElem reads

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

The right-hand side is exactly the same as the left-hand side; so your recursion diverges. This is why evaluation hangs.

Note that Idris would have caught this error if you declared that removeElem should be total:

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)

which results in the compile-time error

RemoveElem.idr line 9 col 0:

Main.removeElem is possibly not total due to recursive path Main.removeElem

Why does this function hang the REPL?

1 Answers