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

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

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

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`

).

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;
```

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`

.

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

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.

The classical definition using `leftAdjunct`

/`rightAdjunct`

makes no mention of `unit`

/`counit`

.

You can derive all the laws involving `unit`

and `counit`

from that definition.

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

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`

?

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 = id`

and 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`

...?

An adjunction `F -| G`

is given by a natural isomorphism `leftAdjunct`

/`rightAdjunct`

between the functors `Hom(F _, _)`

and `Hom(_, G _)`

. In other words:

- those are two natural transformations, and
- they are inverses of each other.

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:

`fmap g . leftAdjunct f . h = leftAdjunct (g . f . fmap h)`

(naturality of`leftAdjunct`

)`g . rightAdjunct f . fmap h = rightAdjunct (fmap g . f . h)`

(naturality of`rightAdjunct`

)`leftAdjunct . rightAdjunct = id`

(semiinverse)`rightAdjunct . leftAdjunct = id`

(the other half)

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

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

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

I see there is `paramcoq`

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

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.

@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: Jan 29 2023 at 05:03 UTC