我该如何简化这种类型？

Question

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

Answer 1

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)

第二个改变隐式参数的顺序,但我认为这是合理的.

有关`{}语法的说明,请参见此处.主要区别在于名称,而不是类型是可选的.另外,参数的隐式行为在`{}内部是奇怪的,除非你用!开始这个类型.