Idris中如何使用Vect.filter返回的依赖对进行计算？

Vect的filter返回(p : Nat ** Vect p Integer)这种依赖对，本质是因为过滤后的向量长度无法在编译期确定，所以用依赖对把动态长度和对应长度的向量绑定起来，保证类型安全。要对其中的元素执行sum、map、filter等操作，核心是先提取出内部的Vect实例，再用普通的Vect操作函数处理，具体方法如下：

1. 计算sum：提取向量后直接调用sum #

方式一：模式匹配拆分依赖对 #

用let绑定把依赖对拆分成长度和向量，再对向量调用sum：

let (len ** vec) = filter (< 3) (fromList [1,2,3,4])
in sum vec

执行后会得到结果3，和List的操作逻辑一致。

方式二：用snd直接投影向量 #

依赖对的第二个元素就是目标Vect，直接用snd提取后调用sum：

sum $ snd $ filter (< 3) (fromList [1,2,3,4])

Idris会自动推导类型，识别出snd返回的是符合sum参数要求的Vect类型。

2. 执行map操作：处理向量后可重新构造依赖对 #

如果需要保留长度和向量的绑定关系，处理后可以重新组装成依赖对：

-- 模式匹配后map，再构造新的依赖对
let (len ** vec) = filter (< 3) (fromList [1,2,3,4])
in (len ** map (*2) vec)

如果不需要保留依赖对结构，直接操作向量即可：

map (*2) $ snd $ filter (< 3) (fromList [1,2,3,4])

3. 再次执行filter：嵌套处理依赖对 #

第二次filter依然会返回新的依赖对（因为长度可能再次变化），可以嵌套模式匹配或者链式投影：

嵌套模式匹配（保留长度信息） #

let (len1 ** vec1) = filter (< 3) (fromList [1,2,3,4])
    (len2 ** vec2) = filter (> 0) vec1
in sum vec2

链式投影（直接取最终向量） #

sum $ snd $ filter (> 0) $ snd $ filter (< 3) (fromList [1,2,3,4])

简单来说，依赖对只是把“长度”和“向量”打包在一起了，操作时先拆包取出向量，剩下的就和处理普通Vect完全一样，必要时再把新的长度和向量重新打包即可。

内容的提问来源于stack exchange，提问作者thor