在Idris中,如果我想根据谓词删除一个元素,有filter
、dropWhile
、takeWhile
。但是,所有这些函数都返回依赖对 (n : Nat ** Vect n elem)
。
是否有任何函数返回为 Vect
类型?
我能想到的:
将依赖对转换为
Vect
实现一个指示转换后长度向量的类型(我想我不知道怎么做),比如
Here
、There
对于上面的思路,1(对每一个结果都进行转换)或者2(对每一个类型都设计一个表示结果向量的长度),似乎比较繁琐。
有没有更好的方法来实现这种行为?
dropElem : String -> Vect n String -> Vect ?resultLen String
最佳答案
也许这就是您要搜索的内容?
import Data.Vect
count: (ty -> Bool) -> Vect n ty -> Nat
count f [] = 0
count f (x::xs) with (f x)
| False = count f xs
| True = 1 + count f xs
%hint
countLemma: {v: Vect n ty} -> count f v `LTE` n
countLemma {v=[]} = LTEZero
countLemma {v=x::xs} {f} with (f x)
| False = lteSuccRight countLemma
| True = LTESucc countLemma
filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty
filter f [] = []
filter f (x::xs) with (f x)
| False = filter f xs
| True = x::filter f xs
然后你可以这样做:
dropElem: (s: String) -> (v: Vect n String) -> Vect (count ((/=) s) v) String
dropElem s = filter ((/=) s)
您甚至可以重用现有的filter
实现:
count: (ty -> Bool) -> Vect n ty -> Nat
count f v = fst $ filter f v
filter: (f: ty -> Bool) -> (v: Vect n ty) -> Vect (count f v) ty
filter f v = snd $ filter f v
关于dependent-type - Idris 确定结果向量长度,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/46526503/