Как я могу упростить этот тип?

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)

Второй изменяет порядок неявных аргументов, но я думаю, что это разумно.

Объяснение синтаксиса `{} смотрите в разделе здесь .Основное отличие заключается в том, что имя, а не тип является необязательным.Кроме того, неявное поведение аргументов странно внутри `{}, если вы не начинаете тип с!.

Answer 2

Это короче, но не намного полезнее ...

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

Я не понимаю, почему вы хотите или нуждаетесь в этом короче, чем сейчас. Каждая вещь имеет свою важность, и немногие имена помогают ее читать.

Этот лифтM2 выглядит настолько легким, насколько это возможно.

Однако, если вы определяете множество функций, которые имеют общие параметры, вы можете определить его внутри раздела, внутри которого вы можете иметь параметры. Например, посмотрите, как здесь определяется liftM2:

http://mattam.org/repos/coq/oldprelude/Monad.v

mon : Monad m определен внутри раздела и будет передан всем функциям, которые фактически его используют. После закрытия раздела вы можете проверить подпись, чтобы убедиться, что она действительно пропущена.