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) -> Type
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) -> Type
liftM2 {A B R : Set} `{Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)
或者
liftM2 `{Monad m} `(f : A -> B -> R) (ma : m A) (mb : m B) : (m R)
第二个改变了隐式参数的顺序,但我认为这是合理的。
有关 `{} 语法的解释,请参见此处。主要区别在于名称,而不是类型是可选的。此外,参数的隐式行为在 `{} 中很奇怪,除非您以 ! 开头类型。
这更短但没有多大用处......
liftM2 {A B R} {m} : Monad m -> (A -> B -> R) -> m A -> m B -> m R.
我不明白为什么你想要或需要这个比它更短。每件事都有其重要性,周围的几个名字也有助于阅读它。
这个 LiftM2 看起来很轻。
但是,如果您要定义许多共享某些参数的函数,则可以在一个部分中定义它,在该部分中可以有参数。例如,看看 liftM2 是如何在这里定义的:
http://mattam.org/repos/coq/oldprelude/Monad.v
是在节内定义的mon : Monad m
,并将传递给实际使用它的所有函数。关闭该部分后,您可以检查签名以查看它是否实际通过。