types - このタイプを単純化するにはどうすればよいですか？

Question

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

このタイプを減らすためのトリックはありますか？そこに冗長性xがあります。

モナドは型クラスです：(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)

2つ目は暗黙の引数の順序を変更しますが、それは合理的だと思います。

`{}構文の説明については、ここを参照してください。主な違いは、タイプではなく名前がオプションであるということです。さらに、！で型を開始しない限り、引数の暗黙の動作は`{}内では奇妙です。

Answer 2

これは短いですが、それほど便利ではありません...

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セクション内で定義され、実際にそれを使用するすべての関数に渡されます。セクションが閉じられたら、署名をチェックして、実際に渡されていることを確認できます。