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 (将#修改为@）