如何解决Applicative 请求意外类型
我很难为我的类型实现 Applicative
。这是Functor
data Connection : repr -> out -> Type where
MkConnection : (repr -> ty) -> (ty -> out) -> Connection repr out
Functor (Connection repr) where
map f (MkConnection get g) = MkConnection get $ f . g
如果我写Applicative
有一个洞
Applicative (Connection repr) where
pure x = ?rhs
我可以输入 check 来获取
"src/Foo.idr" 94L,4210C written
0 a : Type
0 repr : repr
x : a
------------------------------
rhs : Connection repr a
搜索没有结果。确实,如果我添加更多细节
Applicative (Connection repr) where
pure x = MkConnection ?get ?g
我明白
"src/Foo.idr" 94L,4223C written
Error: While processing right hand side of pure. When unifying Connection repr a and Connection repr a.
Mismatch between: Type and repr (implicitly bound at .../src/Foo.idr:94:5--94:34).
.../src/Foo.idr:94:14--94:34
|
94 | pure x = MkConnection ?get ?g
|
我以为我可以用
pure x = MkConnection (\r => ()) (\_ => x)
但我得到了
"src/Foo.idr" 94L,4235C written
Error: While processing right hand side of pure. When unifying Connection repr a and Connection repr a.
Mismatch between: Type and repr (implicitly bound at .../src/Foo.idr:94:5--94:47).
.../src/Foo.idr:94:14--94:47
|
94 | pure x = MkConnection (\r => ()) (\_ => x)
| ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
它似乎将 \r => ()
解释为 Type -> something
版权声明:本文内容由互联网用户自发贡献,该文观点与技术仅代表作者本人。本站仅提供信息存储空间服务,不拥有所有权,不承担相关法律责任。如发现本站有涉嫌侵权/违法违规的内容, 请发送邮件至 dio@foxmail.com 举报,一经查实,本站将立刻删除。