我怎样才能简化这个类型？
liftM2 {A B R : Set} {m} {x : Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)
有什么技巧可以减少这种类型吗？我那里有一个多余的x。
Monad 是一个类型类： (Set -> Set) ->类型
liftM2 {A B R : Set} {m} {x : Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)
Are there any tricks to reducing this type? I have a redundant x in there.
Monad is a typeclass: (Set -> Set) -> Type
如果你对这篇内容有疑问，欢迎到本站社区发帖提问 参与讨论，获取更多帮助，或者扫码二维码加入 Web 技术交流群。
绑定邮箱获取回复消息
由于您还没有绑定你的真实邮箱，如果其他用户或者作者回复了您的评论，将不能在第一时间通知您！
发布评论
评论（2）
或者
第二个改变了隐式参数的顺序，但我认为这是合理的。
有关 `{} 语法的解释，请参阅此处。主要区别在于名称而不是类型是可选的。此外，参数的隐式行为在 `{} 中很奇怪，除非
你以 ! 开始输入。
or
The second one changes the order of implicit arguments, but I think it is reasonable.
For an explantion of the `{} syntax, see here. The main difference is that the name, rather than the type is optional. In addition, the implicit behavior of arguments is strange inside `{} unless
you start the type with !.
这更短，但并没有更有用......
我不明白为什么你想要或需要比它更短的东西。每件事都有其重要性，周围的几个名字也有助于阅读。
这款 liftM2 看起来很轻。
但是，如果您定义了许多共享某些参数的函数，则可以在一个部分中定义它，在该部分中可以有参数。例如，请参阅此处如何定义 liftM2：
http://mattam.org/repos/coq /oldprelude/Monad.v
mon : Monad m在该部分中定义，并将传递给实际使用它的所有函数。该部分关闭后，您可以检查签名以查看它是否确实已通过。This is shorter but not much more useful...
I don't understand why you want or need this shorter than it is though. Every thing has its importance, and the few names cast around help reading it too.
This liftM2 seems as light as it can be.
However, if you are defining a lot of functions that all share some parameters, you can define it inside a section, inside which you can have Parameters. For instance, see how liftM2 is defined here:
http://mattam.org/repos/coq/oldprelude/Monad.v
The
mon : Monad mis defined inside the section, and will be passed to all the functions that actually use it. Once the section is closed, you can check the signature to see that it is actually passed.