我正在 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)
依赖对具有构造函数
fst
和snd
来提取值:
Main> sum $ snd $ filter (< 3) (fromList [1,2,3,4])
3
Main> fst $ filter (< 3) (fromList [1,2,3,4])
2