How can i simplify this type?

Question

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

Answer 1

This is shorter but not much more useful...

liftM2 {A B R} {m} : Monad m -> (A -> B -> R) -> m A -> m B -> m R.

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 m is 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.

Answer 2

liftM2 {A B R : Set} `{Monad m} (f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

or

liftM2 `{Monad m} `(f : A -> B -> R) (ma : m A) (mb : m B) : (m R)

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 !.