Hi!

Coq n00b here. I'm trying to add implicit arguments to `leftAdjunct`

and `rightAdjunct`

below.

```
Class Adjunction {f u} := {
f_is_functor :> Functor f;
u_is_functor :> Functor u;
leftAdjunct : forall a b : Type, (f a -> b) -> a -> u b;
rightAdjunct : forall a b : Type, (a -> u b) -> f a -> b;
}.
```

Haven't had much luck with the documentation so far... any pointers?

Can you be more specific about what you want to happen? `f`

, `u`

and the class argument should already be implicit.

Can you be more specific about what you want to happen?

Sure. I have various theorems like this:

```
Lemma left_nat `{AdjunctionLaws f u}:
forall {a} (x : u a), (leftAdjunct _ _ ∘ rightAdjunct _ _) id x = x.
```

I want to omit those arguments where it's just types that can be inferred.

I'm studying @John Wiegley (Gitter import)'s `coq-haskell`

. I'm hoping to extend it to cover Ed Kmett's `Data.Functor.Adjunction`

among other things in the `adjunctions`

package.

John has some clever implicit argument declarations I don't understand. For instance, he writes:

```
Class Functor (f : Type -> Type) : Type := {
fmap : forall {a b : Type}, (a -> b) -> f a -> f b
}.
Arguments fmap {f _ a b} g x.
```

I'm curious what's going on there...

the curly brackets `{}`

mean the arguments between them are implicit

What I would write is:

```
Class Adjunction {f u} := {
f_is_functor :> Functor f;
u_is_functor :> Functor u;
leftAdjunct {a b : Type} : (f a -> b) -> a -> u b;
rightAdjunct {a b : Type} : (a -> u b) -> f a -> b;
}.
Arguments Adjunction : clear implicits.
```

you can write `leftAdjunct : forall {a b : Type}, (f a -> b) -> a -> u b;`

instead of `leftAdjunct {a b : Type} : (f a -> b) -> a -> u b;`

, they're equivalent and it's a matter of taste.

In all cases, after the `Class`

declaration, arguments between curly braces are implicits — in particular, `f`

and `u`

become implicit arguments for `Adjunction`

and to all the class projections (`f_is_functor`

, `u_is_functor`

, `leftAdjunct`

and `rightAdjunct`

).

But since in practice one wants `Adjunction`

to take `f`

and `u`

as _explicit_ arguments, `Arguments Adjunction : clear implicits.`

corrects the declaration.

instead, @John Wiegley's `Functor`

snippet is declaring `f`

as an explicit parameter (by using `()`

not `{}`

) — and then he's using `Arguments`

to make `f`

implicit for `fmap`

.

both styles work, but since records/classes often have many fields, I prefer using `clear implicits`

over the alternative:

namely,

```
Class Adjunction f u := {
f_is_functor :> Functor f;
u_is_functor :> Functor u;
leftAdjunct {a b : Type} : (f a -> b) -> a -> u b;
rightAdjunct {a b : Type} : (a -> u b) -> f a -> b;
}.
Arguments leftAdjunct {f u a b}.
Arguments rightAdjunct {f u a b}.
(* honestly, you might not care for the next two declarations: *)
Arguments f_is_functor {f u}.
Arguments u_is_functor {f u}.
```

@Paolo Giarrusso This is great! Thank you very much!

I like this, @Paolo Giarrusso, I'll look into changing the code over to this style.

happy you like it… (BTW just fixed a silly typo)

Matthew Doty has marked this topic as resolved.

Last updated: Sep 25 2023 at 12:01 UTC