如何解决Vec:过滤器:我不确定构造函数是否应该使用这种情况[]
我正在尝试为Vec定义过滤功能:
vecFilter : ∀ {P : Pred A p} → Decidable P → ∀ {n m : ℕ} → Vec A (m + n) → Vec A n
vecFilter P? [] = []
vecFilter P? (x ∷ xs) with does (P? x)
... | false = vecFilter P? xs
... | true = x ∷ vecFilter P? xs
我基于Data.List
filter
,也基于Data.Vec
count
。
我收到以下错误消息:
I'm not sure if there should be a case for the constructor [],because I get stuck when trying to solve the following unification
problems (inferred index ≟ expected index):
ℕ.zero ≟ n + m
when checking that the pattern [] has type Vec A (n + m)
我想知道这是否与我使用Vec A (n + m)
有关。
解决方法
我刚刚注意到filter
Data.Vec已经实现了Vec
。我在Data.Vec.Base
您建议的filter
类型非常大:
vecFilter : ∀ {P : Pred A p} → Decidable P → ∀ {n m : ℕ} → Vec A (m + n) → Vec A n
它声称对于任何可判定的谓词P
以及任何一对自然数n
和m
,您都可以转换{{1 }}元素转换成m + n
元素的向量。
但是,这显然是不正确的;例如,如果我选择n
为P
,选择const ⊤
为0,选择n
为1,则需要使用过滤器函数才能从单元素向量生成空向量,即使该谓词必然适用于该元素。
那我们该怎么办?必须由您的函数来选择要删除多少个元素(m
)。换句话说,它必须以某种方式进行定量存在。实际的做法是说m
可以处理任何长度的任何向量,然后返回一对相关的删除元素数,以及其余元素:
vecFilter
当然,标准库中的实际实现要好一些,它使用唯一的表示形式来表示长度上的差异(而vecFilter : ∀ {P : Pred A p} → Decidable P → ∀ {n : ℕ} → Vec A n → Σ ℕ λ m → Vec A (n ∸ m)
允许n ∸ m
之类的内容表示空结果)。
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。