¿Cómo puedo simplificar este tipo?

Question

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

¿Hay algún truco para reducir este tipo?tengo un redundante x ahí.

Monad es una clase de tipos: (Set -> Set) -> Type

Answer 1

Esto es más corto pero no mucho más útil...

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

Sin embargo, no entiendo por qué quieres o necesitas esto más corto de lo que es.Cada cosa tiene su importancia y los pocos nombres que aparecen ayudan a leerlo también.

Este liftM2 parece lo más ligero posible.

Sin embargo, si está definiendo muchas funciones que comparten algunos parámetros, puede definirlas dentro de una sección, dentro de la cual puede tener Parámetros.Por ejemplo, vea cómo se define liftM2 aquí:

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

El mon : Monad m se define dentro de la sección y se pasará a todas las funciones que realmente lo usan.Una vez cerrada la sección, podrás comprobar la firma para comprobar que realmente está aprobada.

Answer 2

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

o

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

El segundo cambia el orden de los argumentos implícitos, pero creo que es razonable.

Para obtener una explicación de la `{} sintaxis, consulte aquí .La principal diferencia es que el nombre, en lugar del tipo, es opcional.Además, el comportamiento implícito de los argumentos es extraño dentro de `{} a menos que comienza el tipo con!.