Come posso semplificare questo tipo?

Question

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

Esistono trucchi per ridurre questo tipo?Ho un x ridondante.

Monad è una classe di tipo: (Set -> Set) -> Type

Answer 1

Questo è più breve ma non molto più utile ...

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

Non capisco perché vuoi o hai bisogno di questo più corto di quanto non sia.Ogni cosa ha la sua importanza e anche i pochi nomi espressi in giro aiutano a leggerlo.

Questo liftM2 sembra il più leggero possibile.

Tuttavia, se stai definendo molte funzioni che condividono tutti alcuni parametri, puoi definirle all'interno di una sezione, all'interno della quale puoi avere Parametri.Ad esempio, guarda come viene definito liftM2 qui:

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

Il mon : Monad m è definito all'interno della sezione, e verrà passato a tutte le funzioni che effettivamente lo utilizzano.Una volta chiusa la sezione, puoi controllare la firma per vedere se è stata effettivamente passata.

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)

Il secondo cambia l'ordine degli argomenti impliciti, ma penso che sia ragionevole.

Per una spiegazione della sintassi di "{}, vedere qui .La differenza principale è che il nome, piuttosto che il tipo, è facoltativo.Inoltre, il comportamento implicito degli argomenti è strano all'interno di `{} a meno che inizi il tipo con!.