Idris 确定结果向量长度

Question

在Idris中，如果我想根据谓词删除一个元素，有filter、dropWhile、takeWhile。但是，所有这些函数 return 依赖对 (n : Nat ** Vect n elem).

是否有任何函数 return 返回 Vect 类型？

我能想到的：

将依赖对转换为Vect
实现一个表示转换后长度向量的类型（以为我不知道怎么做），比如Here、There

以上思路，1（对每一个结果进行转换）或者2（对每一个类型都设计一个表示结果向量长度），似乎比较繁琐

有没有更好的方法来实现这种行为？

dropElem : String -> Vect n String -> Vect ?resultLen String

Answer 1

也许这就是您要搜索的内容？

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

Idris 确定结果向量长度

Idris determining result vector length

dependent-type

idris