dependent-type - Idris 确定结果向量长度

Question

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

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

我能想到的:

1. 将依赖对转换为Vect

2. 实现一个指示转换后长度向量的类型(我想我不知道怎么做)，比如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