armanbilge [23:35]
question: is this a bijection?

def f[A](some: Some[A]): Option[A] = some

seems so, but you can't write the inverse g: Option[A] => Some[A] 🤔

Adam [23:50]
On the value level, yes. But not on the type-level.
(it's not surjective on the type level)

armanbilge [23:57]
thanks. I have a GADT that semantically should only be transformed via bijections. invariant seemed good, until I realized I lose .widen which makes it less flexible
I guess the burden is now on consuming APIs to be sufficiently generic to handle Foo[Some[A]] when they really only need Foo[Option[A]], since it's impossible to widen your way there

armanbilge [00:13]
hmm, but InvariantMonoidal#point is defined like:

def point[A](a: A): F[A] = imap(unit)(_ => a)(_ => ())

maybe imap isn't really about bijections
or maybe that signature should return F[a.type]

Adam [00:17]
Hmm I think I've handled that once before, but I really should get some sleep. Does your GADT have a specific form that may make it easier to work with? What does it represent?

armanbilge [00:18]
https://github.com/armanbilge/schrodinger/blob/e97397da4c7cb4fedcce5a4035310b5210da7246/monte-carlo/src/main/scala/schrodinger/montecarlo/Weighted.scala#L51
a weighted sample from a probability distribution

Adam [00:18]
Sometimes it's easier to define a StructTransformer than a Struct that admits to all the right ways to handle it

armanbilge [00:19]
right, not sure if that's the case here

Adam [00:23]
That's a pretty cool piece of code.
One last thought is to "simply" require that all functions acting on it are tagged with a bijective trait (though you'd probably want even stricter guarantees since you're working with probabilities and there's not that many meaningful operations you can do on that class).

armanbilge [00:24]
yeah, that's an option too. but then no cats interop 🙂
I guess if you have a trait Bijection[A, B] or something it would be isomorphic to the imap signature
I think my current feeling is that point in cats is defined "wrong"

Aly [01:29] (⮎ replying to "question: is this a bijection?...")
It would be a bijection if i.e. the output type was (x: Option[A], x.type <:< Some[A]). However, with imap, you need a bijection between the _type_s you're given, and Option and Some lack that

armanbilge [01:30]
right, so would you agree that point has the wrong signature then?

Aly [01:30]
I would not

armanbilge [01:31]
why not?

Aly [01:32]
Ok sorry yes you're right it should be a.type
I'm a bit slow

armanbilge [01:35]
that can be fixed bincompat 🙂 but I guess it would wreak havoc 🙃

Aly [01:35]
I'm wondering actually whether that should be true of invariant functors

armanbilge [01:35]
what should be true, specifically?

Aly [01:35]
.imap(f)(g).imap(g)(f) = identity

armanbilge [01:36]
oh interesting 🤔

armanbilge [01:39]
is that implied by this law

  def invariantComposition[A, B, C](fa: F[A], f1: A => B, f2: B => A, g1: B => C, g2: C => B): IsEq[F[C]] =
    fa.imap(f1)(f2).imap(g1)(g2) <-> fa.imap(g1.compose(f1))(f2.compose(g2))

Aly [01:39]
No, that's actually looser

armanbilge [01:40]
ah right

armanbilge [01:41]
actually
that law checking violates the assumption that its bijection-based
since scalacheck wouldn't generate f1 and f2 that are inverses

Aly [01:46]
So if .imap(f)(g).imap(g)(f) ≡ identity is not true, then point is technically correct (and probably the most helpful definition)

armanbilge [01:50]
right, exactly
and it also means that I shouldn't rely on imap if I only want my ADT to be transformed by bijections

armanbilge [01:55]
@Aly what about this law

Aly [01:57]
That's some sort of associativity. Doesn't seem to involve imap
A property of imap itself at least

armanbilge [01:57]
so there is an InvariantSemigroupal that doesn't satisfy .imap(f)(g).imap(g)(f) ≡ identity but does satisfy that law

Aly [01:58]
If .imap(f)(g).imap(g)(f) ≡ identity were a law it would moreso mean that the user should pass isomorphisms into imap
Well
That's not true
Hmmmmm

armanbilge [02:01]
right, imap f g ∘ imap g f = identity has a prereq that f ∘ g = identity right

Aly [02:01]
as well as g ∘ f

armanbilge [02:03]
right, so then it seems like it might come from that composition law

Aly [02:09]
The composition law...
It does
Yep
The combination of the two laws says that imap by an isomorphism creates an isomorphism

armanbilge [02:10]
so the scaladoc example is a bijection

Aly [02:10]
When I'm done eating this chicken I'll prove it in AgdaPad

armanbilge [02:16]
https://github.com/scalaz/scalaz/blob/master/core/src/main/scala/scalaz/InvariantFunctor.scala
scalaz actually uses the word bijection
hm, but only on a special overload

armanbilge [03:34]
the plot thickens zio/zio-prelude#548

Aly [04:00]
@armanbilge

If:

• f is a morphism X => Y
• g is a morphism Y => X
• f andThen g ≡ identity

Then:

• (_.imap(f)(g)) andThen (_.imap(g)(f)) ≡ identity

Proof: https://gist.github.com/s5bug/05610879f1b13fff5c9893071d2b77f1#file-invariant-imap-iso-is-iso-agda
prelude ends at record Precategory

armanbilge [04:02]
Does it not require g and then f is id?

Aly [04:02]
it does to show that the other direction of imap is identity as well

armanbilge [04:02]
Ahh gotcha

Aly [04:03]
I think I would express this as "invariant functors preserve isomorphisms, but don't require them"
But I am not a mathematician so

armanbilge [04:04]
Yeah
The thing I'm confused about is whether invariant functors make sense without it
For example is it valid to imap a semi group without an isomorphism
Do you get a lawful semigroup out?

Aly [04:05]
Well, in the point case, you get a constant semigroup

armanbilge [04:06]
And if not, should it have an instance of invariant

Aly [04:06]
i mean I guess I could try to prove this

armanbilge [04:06]
The proof just needs an example 🙂
Well, maybe more than that 🤔
I guess the proof is that a semi group created via imap is lawful iff made by an isomorphism
Something like that
*the proof = the thing to be proven

Aly [04:09]
Well of course a semigroup created via an imap on an isomorphism is lawful
but we want to prove that it's lawful even without the iso

armanbilge [04:09]
So then, maybe all we need is an example of a semi group made by imap that is unlawful

Aly [04:11]
or, a proof that all semigroups made by imap are lawful

armanbilge [04:12]
Yes. Or that 🙂

Aly [05:06]
hmm... I can prove that mySemigroup.imap(f)(g) is lawful if g ∘ f ≡ id... Any two functions I think of that don't hold that property seem to work out in my head, but idk

Aly [05:12]
if f is identity and g is _ + 2 then

(2 * 3) * 5 → ((2 + (4 * 5)) * 7) = 154
2 * (3 * 5) → 4 * (2 + (5 * 7)) = 148
@armanbilge check my math?

Aly [05:17]
Yeah, without an iso the semigroup is not lawful

armanbilge [05:18]
You did it!
Want to open an issue in cats? Or a PR to update the docs to state this precondition

Aly [05:20]
I'll open an issue, I don't feel like writing docs today