You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
If we take the imap defined on Semigroup, associativity can be proven with f andThen g ≡ identity. There may be even more lenient cases, but I'm not aware of them (pseudo-Agda):
Invariant[Semigroup].imap (f : A → B) (g : B → A) (x : Semigroup) =record
{ combine =λ a →λ b → f (x.combine (g a) (g b))
; combine-assoc =
f (x.combine (g (f (x.combine (g a) (g b)))) (g c)) ≡⟨ ? ⟩
-- we must have a proof of `g . f ≡ id` to get to this step
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))) ≡⟨ ? ⟩
-- we reuse that proof here
f (x.combine (g a) (g (f (x.combine (g b) (g c))))) ∎
}
When this is not the case, it is possible to produce an unlawful Semigroup via imap:
Discord conversation in Typelevel #theory channel, 2022-05-03T23:35:28.439Z to 2022-05-04T05:20:19.215Z
armanbilge [23:35]
question: is this a bijection?
deff[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:
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?
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?
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
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 [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: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
So perhaps Invariant could use some documentation upgrades too, regarding extra properties that arise from the laws, as well as being able to imap with non-isomorphisms.
The text was updated successfully, but these errors were encountered:
If we take the
imap
defined onSemigroup
, associativity can be proven withf andThen g
≡identity
. There may be even more lenient cases, but I'm not aware of them (pseudo-Agda):When this is not the case, it is possible to produce an unlawful
Semigroup
viaimap
:Discord conversation in Typelevel #theory channel, 2022-05-03T23:35:28.439Z to 2022-05-04T05:20:19.215Z
armanbilge [23:35]
question: is this a bijection?
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 flexibleI guess the burden is now on consuming APIs to be sufficiently generic to handle
Foo[Some[A]]
when they really only needFoo[Option[A]]
, since it's impossible to widen your way therearmanbilge [00:13]
hmm, but
InvariantMonoidal#point
is defined like:maybe
imap
isn't really about bijectionsor 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 theimap
signatureI 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, withimap
, you need a bijection between the _type_s you're given, andOption
andSome
lack thatarmanbilge [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)
= identityarmanbilge [01:36]
oh interesting 🤔
armanbilge [01:39]
is that implied by this law
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
andf2
that are inversesAly [01:46]
So if
.imap(f)(g).imap(g)(f)
≡identity
is not true, thenpoint
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 bijectionsarmanbilge [01:55]
@Aly
what about this lawcats/laws/src/main/scala/cats/laws/InvariantSemigroupalLaws.scala
Line 33 in 5a3e175
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 lawAly [01:58]
If
.imap(f)(g).imap(g)(f)
≡identity
were a law it would moreso mean that the user should pass isomorphisms intoimap
Well
That's not true
Hmmmmm
armanbilge [02:01]
right,
imap f g ∘ imap g f = identity
has a prereq thatf ∘ g = identity
rightAly [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 isomorphismarmanbilge [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:
Then:
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
isidentity
as wellarmanbilge [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 semigrouparmanbilge [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 ifg ∘ f ≡ id
... Any two functions I think of that don't hold that property seem to work out in my head, but idkAly [05:12]
if
f
isidentity
andg
is_ + 2
thenAly [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
So perhaps
Invariant
could use some documentation upgrades too, regarding extra properties that arise from the laws, as well as being able toimap
with non-isomorphisms.The text was updated successfully, but these errors were encountered: