Stream: Coq users

Topic: Extending `coq-haskell` to cover `Data.Functor.Adjunction`

view this post on Zulip Matthew Doty (Sep 24 2021 at 01:43):

@John Wiegley I alluded in another topic that I am trying to extend coq-haskell to cover Ed Kmett's adjunctions package.

While I have an axiomatization I'm confident in, it's pretty divergent from what's written in Data.Functor.Adjunction :half_frown: .

view this post on Zulip Matthew Doty (Sep 24 2021 at 01:48):

The documentation in Data.Functor.Adjunction states:

Minimal definition: both unit and counit or both leftAdjunct and rightAdjunct, subject to the constraints imposed by the default definitions that the following laws should hold.

unit = leftAdjunct id
counit = rightAdjunct id
leftAdjunct f = fmap f . unit
rightAdjunct f = counit . fmap f

Any implementation is required to ensure that leftAdjunct and rightAdjunct witness an isomorphism from Nat (f a, b) to Nat (a, g b)

rightAdjunct unit = id
leftAdjunct counit = id

view this post on Zulip Matthew Doty (Sep 24 2021 at 02:03):

Early on in my efforts, I had trouble proving fmap g x = rightAdjunct (unit ∘ g) x and fmap g x = leftAdjunct (g ∘ counit) x. I ended up adding these as laws.

This feels a little like how you ended up adding the law fmap g x = pure g <*> x to your ApplicativeLaws. I know the Control.Applicative documentation claims this is derivable, but I am not sure about that. However, I haven't found a counter-example...

view this post on Zulip Matthew Doty (Sep 24 2021 at 02:05):

Along with FunctorLaws, the laws fmap g x = rightAdjunct (unit ∘ g) x and its dual are strong enough to prove rightAdjunct unit = id and its dual (follows from fmap id = id).

view this post on Zulip Matthew Doty (Sep 24 2021 at 02:15):

But I found I needed yet another pair of laws to prove (rightAdjunct ∘ leftAdjunct) g = g and its dual... namely, I needed the following triangle identities:

  counit_univ : forall {a b} (g : f a -> b) (x : f a),
    g x = (counit ∘ fmap (leftAdjunct g)) x;
  unit_univ : forall {a b} (g : a -> u b) (x : a),
    g x = (fmap (rightAdjunct g) ∘ unit) x;

view this post on Zulip Matthew Doty (Sep 24 2021 at 02:23):

So here's my WIP. 

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.

Definition unit `{Adjunction f u} {a} (x : a) :=
  leftAdjunct id x.

Definition counit `{Adjunction f u} {a} (x : f (u a)) :=
  rightAdjunct id x.

Class AdjunctionLaws {f u} `{Adjunction f u} := {
  f_has_functor_laws :> FunctorLaws f;
  u_has_functor_laws :> FunctorLaws u;

  left_adjunct_to_unit : forall {a b} (g : f a -> b) (x : a),
    leftAdjunct g x = (fmap g ∘ unit) x;
  right_adjunct_to_counit : forall {a b} (g : a -> u b) (x: f a),
    rightAdjunct g x = (counit ∘ fmap g) x;

  f_fmap : forall {a b} (g : a -> b) (x : f a),
    fmap g x = rightAdjunct (unit ∘ g) x;
  u_fmap : forall {a b} (g : a -> b) (x : u a),
    fmap g x = leftAdjunct (g ∘ counit) x;

  counit_univ : forall {a b} (g : f a -> b) (x : f a),
    g x = (counit ∘ fmap (leftAdjunct g)) x;
  unit_univ : forall {a b} (g : a -> u b) (x : a),
    g x = (fmap (rightAdjunct g) ∘ unit) x;
}.

If you find this satisfactory, I'll try to prepare a PR. My proofs use CoqHammer, so they'll need some rework to make them fit in coq-haskell.

view this post on Zulip Matthew Doty (Sep 24 2021 at 02:35):

Looking at this again, I see (rightAdjunct ∘ leftAdjunct) g = g and its dual are equivalent to counit_univ and unit_univ, so maybe it's better to go with those as laws...

view this post on Zulip Li-yao (Sep 24 2021 at 18:08):

The first four laws are consequences of the naturality of leftAdjunct and rightAdjunct (together with those relating to counit/unit), which seems like a better law to encode.

view this post on Zulip Li-yao (Sep 24 2021 at 18:12):

The classical definition using leftAdjunct/rightAdjunct makes no mention of unit/counit.

view this post on Zulip Li-yao (Sep 24 2021 at 18:12):

You can derive all the laws involving unit and counit from that definition.

view this post on Zulip Paolo Giarrusso (Sep 24 2021 at 21:07):

On naturality and laws that are "provable in Haskell" but not in Coq: Haskell-side, are they making a parametricity argument? Because those aren't directly formalizable @Matthew Doty

view this post on Zulip Matthew Doty (Sep 25 2021 at 02:54):

The first four laws are consequences of the naturality of leftAdjunct and rightAdjunct (together with those relating to counit/unit), which seems like a better law to encode.

@Li-yao I'm a little confused... maybe you could show me what you have in mind for encoding AdjunctionLaws?

view this post on Zulip Matthew Doty (Sep 25 2021 at 03:14):

On naturality and laws that are "provable in Haskell" but not in Coq: Haskell-side, are they making a parametricity argument? Because those aren't directly formalizable

@Paolo Giarrusso So digging around I see that there is a parametricity argument for fmap g x = rightAdjunct (unit ∘ g) x from rightAdjunct unit = idand its dual (Ed Kmett has a remark about this)

A similar argument for applicatives means fmap f x = pure f <*> x follows from pure id <*> x = x (which sheds a little light on this statement from the documentation). @John Wiegley maybe worth mentioning the parametricity argument for fmap f x = pure f <*> x as a comment in coq-haskell...?

view this post on Zulip Li-yao (Sep 25 2021 at 15:50):

An adjunction F -| G is given by a natural isomorphism leftAdjunct/rightAdjunct between the functors Hom(F _, _) and Hom(_, G _). In other words:

The "inverse" part is straightforward. The "natural transformation" part is more daunting if you're new to this but it really is still just unfolding the definition of a natural transformation to this setting, which boils down to a commutative diagram (in Set, i.e., where arrows are functions):

                      leftAdjunct
           Hom(F a, b)   -> Hom(a, G b)
g . _ . fmap h  |               |  fmap g . _ . h
                v               v
           Hom(F a', b') -> Hom(a', G b')
                      leftAdjunct

In summary, unfolding that definition of adjunctions, we end up with four equations:

view this post on Zulip Li-yao (Sep 25 2021 at 16:36):

unit/counit is a different definition of adjunction, and it might be worthwhile to define it as it own class as well. One benefit is that then you can try to prove the equivalence between the definitions, which gives you some amount of confidence that you haven't missed an essential axiom.

view this post on Zulip Matthew Doty (Sep 25 2021 at 21:19):

@Li-yao I see, naturality of leftAdjunct and rightAdjunct are enough to prove what I've labeled f_fmap, u_fmap, left_adjunct_to_unit and right_adjunct_to_unit.

As I mentioned above, fmap g x = rightAdjunct (unit ∘ g) x follows from parametricity and rightAdjunct . leftAdjunct = id (and the dual). I wonder if the full naturality laws follow from parametricity?

I agree that a unit/counit formulation of adjunction is valuable as a check.

view this post on Zulip Li-yao (Sep 25 2021 at 23:36):

I think they do follow from parametricity but you can't really make use of that in Coq.

view this post on Zulip Matthew Doty (Sep 26 2021 at 00:37):

I see there is paramcoq. Looks like @Karl Palmskog is a contributor... maybe he can speak to whether it is ready for prime time?

view this post on Zulip Karl Palmskog (Sep 26 2021 at 00:41):

I mostly help out with compatibility and CI. Paramcoq is described by the authors as experimental still, but it's used in many large projects, such as CoqEAL and Hydra battles, and it's part of Coq's CI, so is continually updated as Coq evolves.

view this post on Zulip Paolo Giarrusso (Sep 26 2021 at 05:24):

@Matthew Doty FWIW, paramcoq won't let you drop the law from the class, but it should prove the law on at least all monomorphic instances.

Last updated: Sep 30 2023 at 05:01 UTC