imap requires that f.andThen(g) == identity

[armanbilge]

One possible fix for #4199. It seems that at least some of our implementations of Invariant have been relying on this precondition anyway, so this is a way forward without retracting those instances.

[johnynek]

Actually, can we also be explicit: we require that f.andThen(g) == identity.

[armanbilge]

Hmm, that's a good point. IIUC requiring f.andThen(g) == identity is weaker than requiring an isomorphism. @s5bug's proof in #4199 actually doesn't require an isomorphism, at least for Semigroup.

[s5bug]

imap generally doesn't require an isomorphism one way (see the general proof in the Discord logs).

I would keep in mind that there are more lenient cases where imap on Semigroup will still behave nicely:

Specifically on Semigroup, I believe it will behave nicely whenever g is a Semigroup Homomorphism (more pseudo-Agda. This time it hasn't actually been checked by the type-checker, so I could be wrong):

imap-on-semigroup-hom : {A B : Type} (x : Semigroup A) (f : A → B) (g : B → A)
                      → (fSemigroupHom : ∀ {a b : A} → (imap f g x).combine (f a) (f b) ≡ f (x.combine a b))
                      → (gSemigroupHom : ∀ {a b : B} → x.combine (g a) (g b) ≡ g ((imap f g x).combine a b))
                      → ∀ {a b c : B} (imap f g x).combine ((imap f g x).combine a b) c ≡ (imap f g x).combine a ((imap f g x).combine b c)
imap-on-semigroup-hom =
  f (x.combine (g (f (x.combine (g a) (g b)))) (g c)) ≡⟨ ap (λ l → f (x.combine l (g c))) (sym gSemigroupHom) ⟩
  f (x.combine (x.combine (g a) (g b)) (g c))         ≡⟨ ap f x.combine-assoc ⟩
  f (x.combine (g a) (x.combine (g b) (g c)))         ≡⟨ ap (λ r → f (x.combine (g a) r)) gSemigroupHom ⟩
  f (x.combine (g a) (g (f (x.combine (g b) (g c))))) ∎

[armanbilge]

Cats also has Invariant instances for Monoid and Group and lots of stuff.

cats/core/src/main/scala/cats/Invariant.scala

Line 125 in 5a3e175

object Invariant extends ScalaVersionSpecificInvariantInstances with InvariantInstances0 {

I'm not sure what the minimum requirement on imap is for those instances to be lawful.

[s5bug]

I would expect Monoid and Group Homomorphisms likewise.

[s5bug]

Actually, * 2 isn't even a semigroup homomorphism on the product semigroup.

It is not true that (a * 2) * (b * 2) = (a * b) * 2, and yet imap(identity)(_ * 2) works anyways. So it's even more lenient than that.

[armanbilge]

Right, it's sort of a balancing act :) the question here is for Invariant in general, what should the API contract be to permit interesting instances without being too restrictive? Basically, we're trying to make a safe abstraction.

Of course, if you know you are imapping a Semigroup or whatever specifically, then you can take advantage of whatever leniencies apply to that specific situation.

[armanbilge]

@jmgimeno informs me that the category-theoretic term here is "retraction".
https://en.wikipedia.org/wiki/Section_(category_theory)

[armanbilge]

Any more thoughts on this one? :)

[johnynek]

The comment isn't correct as it is now.

I bet there are some instances that require the f.andThen(g) == identity some that require some kind of homomorphism and some uses of imap that don't require anything other than the types lining up.

I actually don't know if we know very much.

I would like to see some tests that fail to help us learn more. E.g. we know we can make some of the tests fail with semigroup + poor choices. Are there are implementations of Invariant other than the algebra cases?

[s5bug]

Personally, my vote is for imap itself to not explicitly have a hard requirement, but explain that

1. f >>> g ≡ identity implies imap(f)(g) >>> imap(g)(f) ≡ identity (and likewise for <<<)
2. When used on other law-having things, incorrect usage will produce something invalid

Although, with (2), isn't the standard to put instances like that in alleycats?

[armanbilge]

some uses of imap that don't require anything other than the types lining up.

Absolutely, any Functor or ContravariantFunctor should fall into this category.

---

Are there are implementations of Invariant other than the algebra cases?

If we look at the instances of Invariant{,Semigroupal,Monoidal} in its companion object, then I believe they are all Semigroups: Semigroup, CommutativeSemigroup, Monoid, CommutativeMonoid, Numeric, Integral, Fractional, Band, Semilattice, BoundedSemilattice, Group, CommutativeGroup.

I stumbled on this question because I wanted to implement an InvariantMonoidal instance for a discrete probability measure, although actually I think this requires a bijection be passed to imap 🤔

---

Personally, my vote is for imap itself to not explicitly have a hard requirement

Do we have any lawful instances then, that don't also implement Functor or ContravariantFunctor?

[armanbilge]

Relevant Twitter thread, h/t @s5bug
https://twitter.com/Fish_CTO/status/1530938960549031942

[s5bug]

(Archive)