如何使用依赖对的结果？

Question

我正在 idris 中学习依赖对，但不明白如何使用它。例如，如果我过滤一个

Data.List

，我会得到一个

Data.List

，我可以对其进行

sum

或其他计算。

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

但是如果我过滤

Data.Vect

，我会得到一个依赖对：

:t filter (< 3) (fromList [1,2,3,4])
filter (\arg => arg < 3) (fromList [1, 2, 3, 4]) : (p : Nat ** Vect p Integer)

显然，filter的结果不再是普通的Vect。相反，它是

(p : Nat ** Vect p Integer)

。我读到这可以解释为某些

Vect p Integer

的

p

。但我不确定如何用它进行计算。列表方式的幼稚尝试是类型错误：

sum $ filter (< 3) (fromList [1,2,3,4])
Error: Sorry, I can't find any elaboration which works. All errors:
...

因此问题

如何计算从

sum

返回的依赖对中的项目

map

、

filter

（甚至

Vect.filter

本身）？

（这是idris2 0.6.0）

Answer 1

依赖对具有构造函数

fst

和

snd

来提取值：

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