Comment puis-je simplifier ce type?

Question

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

Y a-t-il des astuces pour réduire ce type? J'ai un redondant x là-dedans.

Monad est une typlasse: (Set -> Set) -> Type

Answer 1

C'est plus court mais pas beaucoup plus utile ...

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

Je ne comprends pas pourquoi vous voulez ou avez besoin de cela plus court qu'il ne l'est. Tout a son importance, et les quelques noms qui aident également à le lire.

Ce liftm2 semble aussi léger que possible.

Cependant, si vous définissez de nombreuses fonctions qui partagent tous certains paramètres, vous pouvez le définir à l'intérieur d'une section, à l'intérieur de laquelle vous pouvez avoir des paramètres. Par exemple, voyez comment LiftM2 est défini ici:

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

La mon : Monad m est défini à l'intérieur de la section et sera transmis à toutes les fonctions qui l'utilisent réellement. Une fois la section fermée, vous pouvez vérifier la signature pour voir qu'elle est réellement adoptée.

Answer 2

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

ou

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

Le second modifie l'ordre des arguments implicites, mais je pense que c'est raisonnable.

Pour une explication de la syntaxe `{}, voir ici. La principale différence est que le nom, plutôt que le type est facultatif. De plus, le comportement implicite des arguments est étrange à l'intérieur de `{} à moins que vous ne démarriez le type avec !.