如何解决使依赖参数在 Functor 定义中可用
我有 Vect
的以下包装
data Foo : (r : Nat) -> (t: Type) -> Type where
MkFoo : Vect r t -> Foo r t
我想为 Functor
实现 Foo
,并在实现中使用 r
的值,但我无法编译它。
Functor (Foo r) where
map f (MkFoo v) = MkFoo (ff v) where
ff : {r' : Nat} -> Vect r' a -> Vect r' b
给予
Error: While processing right hand side of map. r is not accessible in this
context.
Foo.idr:61:28--61:32
|
61 | map f (MkFoo v) = MkFoo (ff v) where
| ^^^^
这在 Idris 1 中有效,但我不知道如何将其移植到 Idris2。我试过用
不擦除r
Functor ({r : _} -> Foo r) where
map f (MkFoo v) = MkFoo (ff v) where
ff : {r' : Nat} -> Vect r' a -> Vect r' b
但我明白
Error: While processing type
of Functor implementation at Foo.idr:60:1--62:46. When
unifying Type -> Type and Type.
Mismatch between: Type -> Type and Type.
Foo.idr:60:21--60:26
|
60 | Functor ({r : _} -> Foo r) where
| ^^^^^
解决方法
试试:
{r : _} -> Functor (Foo r) where
map f (MkFoo v) = MkFoo (ff v) where
ff : {r' : Nat} -> Vect r' a -> Vect r' b
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。