Matthew Doty (Sep 19 2021 at 13:02): 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?
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.
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.
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...
Gaëtan Gilbert (Sep 19 2021 at 18:58):the curly brackets {} mean the arguments between them are implicit
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.
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.
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).
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.
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.
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:
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}.
@Paolo Giarrusso This is great! Thank you very much!
John Wiegley (Sep 21 2021 at 16:57):I like this, @Paolo Giarrusso, I'll look into changing the code over to this style.
Paolo Giarrusso (Sep 21 2021 at 19:10):happy you like it… (BTW just fixed a silly typo)
Notification Bot (Sep 24 2021 at 02:29):Matthew Doty has marked this topic as resolved.
Last updated: Oct 13 2024 at 01:02 UTC