Stream: Coq users

Topic: ✔ Help with Implicit Arguments


view this post on Zulip Matthew Doty (Sep 19 2021 at 13:02):

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?

view this post on Zulip Gaëtan Gilbert (Sep 19 2021 at 13:11):

Can you be more specific about what you want to happen? f, u and the class argument should already be implicit.

view this post on Zulip Matthew Doty (Sep 19 2021 at 18:47):

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.

view this post on Zulip Matthew Doty (Sep 19 2021 at 18:54):

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...

view this post on Zulip Gaëtan Gilbert (Sep 19 2021 at 18:58):

the curly brackets {} mean the arguments between them are implicit

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:43):

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.

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:44):

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.

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:46):

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).

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:46):

But since in practice one wants Adjunction to take f and u as _explicit_ arguments, Arguments Adjunction : clear implicits. corrects the declaration.

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:48):

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.

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:48):

both styles work, but since records/classes often have many fields, I prefer using clear implicits over the alternative:

view this post on Zulip Paolo Giarrusso (Sep 19 2021 at 19:50):

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}.

view this post on Zulip Matthew Doty (Sep 20 2021 at 02:48):

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

view this post on Zulip John Wiegley (Sep 21 2021 at 16:57):

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

view this post on Zulip Paolo Giarrusso (Sep 21 2021 at 19:10):

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

view this post on Zulip Notification Bot (Sep 24 2021 at 02:29):

Matthew Doty has marked this topic as resolved.


Last updated: Feb 08 2023 at 23:03 UTC