使用 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)
为什么这个,我假设,编译这么慢?
你removeElem
阅读的第二种情况
removeElem value (y :: ys) (MyThere later) = removeElem value (y :: ys) (MyThere later)
右侧与左侧完全相同;所以你的递归发散了。这就是评估挂起的原因。
请注意,如果您声明removeElem
应该为全部,则 Idris 会发现此错误:
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
本文收集自互联网,转载请注明来源。
如有侵权,请联系[email protected] 删除。
我来说两句