Add Decidable
#2607
Add Decidable
#2607
Conversation
| def chosen[B, C](fb: F[B], fc: F[C]): F[Either[B, C]] = | ||
| decide(fb, fc)(identity[Either[B, C]]) | ||
|
|
||
| def zero: F[Nothing] = trivial[Nothing] |
There was a problem hiding this comment.
Are these two always the same? I feel like it's a bit weird that both the additive and multiplicative identities are the same, but it might very well be that my intuition for these sorts of things are off 🤔
There was a problem hiding this comment.
I am a bit suspicious of it as well... For example, the case of maps into Semirings that doesn't quite feel like the right choice... It might bear more thinking on.
There was a problem hiding this comment.
Yeah, I think we might need to change this. I think for any [A, B: Semiring]: A => B you'll want unit to be A => 1 and zero to be A => 0. With this default, zero would be the same as unit, which we don't want.
I think we can already see this in this PR, where you explicitly override zero in the Predicate instance (which can be seen as a specialization of [A, B: Semiring]: A => B) in order for it to be const(false) instead of const(true) :)
There was a problem hiding this comment.
Yeah, that was sort of my intuition as well. I'm a bit puzzled at the original's choice to use Void but, there's probably some reason. Regardless, will change.
There was a problem hiding this comment.
See my comment in #2620 (comment)
| trait DecideableLaws[F[_]] extends ContravariantMonoidalLaws[F] { | ||
| implicit override def F: Decideable[F] | ||
|
|
||
| def decideableDecideRightAbsorption[A](fa: F[A]): IsEq[F[A]] = |
There was a problem hiding this comment.
This one tests right identity, not absorption, right?
Absorption would be product(fa, zero) == zero
There was a problem hiding this comment.
Good call, that' definitely the right name. Morally, I think then we're trading an identity for the traditional absorption on Alternative which makes sense. It's hard to imagine an absorption law for sum or decide that would make sense.
There was a problem hiding this comment.
Hmm, I'm not sure I agree, in Alternative we have both identity and absorption, I think we could have both for Decidable as well. :)
There was a problem hiding this comment.
For ContravariantMonoidal we already have left and right multiplicative identity as well as associativity.
So for Decidable I think we need :
sumandzeroLeft IdentitysumandzeroRight IdentitysumAssociativityproductandzeroRight absorptionsumandcontramapRight DistributivitysumandproductRight Distributivity
And then we should be good IMO :)
There was a problem hiding this comment.
Ah I see how you'd write absorption I think now, yeah, sounds good.
There was a problem hiding this comment.
Interestingly, having both left and right identities seems to rule out OptionT because you have to make a choice for None (either a Left or a Right, which contradicts one or the other identity law, at least if I've written them in a reasonable way), and similarly the sum and product distribution rules out Order and Ordering instances as you end up reversing orderings in the course of that, though I'm working to see if I can fix those instances to respect it.
There was a problem hiding this comment.
Massive thanks @stephen-lazaro! Really great work on this PR. I've added a bunch of comments, but none are really major I think :)
|
|
||
| In other words, if we have two contexts `F[A]` and `F[B]` and we have a procedure `C => Either[A, B]` that could produce either an A or a B depending on the input, we have a way to produce a context `F[C]`. | ||
|
|
||
| The classic example of a `Decideable` is that of predicates `A => Boolean`, leaning on the fact that both `&&` and `^` are valid monoids on `Boolean`. |
There was a problem hiding this comment.
Another note on this one, the default Rig for Boolean uses || instead of ^, should we use || here as well? https://github.com/typelevel/algebra/blob/master/core/src/main/scala/algebra/instances/boolean.scala
|
Thanks for the feedback @LukaJCB ! It may take me a day or two to incorporate, but good points all. |
| package cats | ||
| package laws | ||
|
|
||
| trait DecidableLaws[F[_]] extends ContravariantMonoidalLaws[F] { |
There was a problem hiding this comment.
So a couple concerns about the laws (and again, apologies in advance for any hare-brained comments :)
- they don't seem to invoke
zeroorloseanywhere, so their implementations are not actually checked. - usually when providing default implementations for methods (
decideandlosehere) we add a simple law to check the actual implementation matches the default. This would fix (1) and also makes me wonder if strictly speaking we need thedecideidentity laws, although I guess they don't hurt :)
There was a problem hiding this comment.
I can add some on those certainly, I think keeping the identity laws is a good idea though because they nicely capture some of the vaguely monoid-like character of this stuff.
|
I see there's some discussion on laws in: |
|
Yeah, I'd read that Kmett thread back when opening this - it's true that it's a bit difficult to say what exactly the right choices are. I think we vaguely our choices here largely on the principle of lifting |
|
It gets pretty difficult to actually run some of the laws even once they are expressed, because generating things with |
They're kinda dumb but it's something I guess
stephen-lazaro
force-pushed
the
slazaro/decideable
branch
from
ba64533 to
00a6cd9
Compare
|
@armanbilge This is probably as complete as it's going to get at this stage - let me know if there are thoughts on it. |
|
Ah, great, thanks for the bump and all your work! I will try to take a look this weekend. |
There was a problem hiding this comment.
Sorry that it took me forever to cycle back, had to work up the courage to face this PR again 😅
Just a couple comments for now, but will slowly be combing through this. Really want to land this in the next Cats release.
Also can we add a Nopeee 😂 ignore my inane comment.Decidable[Show] instance?
| def sum[A, B](fa: Eq[A], fb: Eq[B]): Eq[Either[A, B]] = | ||
| Eq.instance { | ||
| case (Left(a1), Left(a2)) => fa.eqv(a1, a2) | ||
| case (Right(b1), Right(b2)) => fb.eqv(b1, b2) | ||
| case _ => false | ||
| } |
There was a problem hiding this comment.
This is equivalent to the usual Eq[Either[A, B]] right? We can probably just delegate to that instances.
There was a problem hiding this comment.
Good call! Thank you.
| trait Decidable[F[_]] extends ContravariantMonoidal[F] { | ||
| def sum[A, B](fa: F[A], fb: F[B]): F[Either[A, B]] | ||
| def zero: F[Nothing] | ||
|
|
||
| def decide[A, B, C](fa: F[A], fb: F[B])(f: C => Either[A, B]): F[C] = | ||
| contramap(sum(fa, fb))(f) | ||
|
|
||
| def lose[A](f: A => Nothing): F[A] = contramap[Nothing, A](zero)(f) | ||
| } |
There was a problem hiding this comment.
Ok I realize this is a bit late in the day, but wouldn't it make more sense to define it like this? Basically trade two abstract defs (contramap+sum) for one (decide).
// abstract
def decide[A, B, C](fa: F[A], fb: F[B])(f: C => Either[A, B]): F[C]
// concrete
def contramap[A, B](fa: F[A])(f: B => A): F[B] =
decide(fa, zero)(b => Left(f(b)))
def sum[A, B](fa: F[A], fb: F[B]): F[Either[A, B]] =
decide(fa, fb)(identity)There was a problem hiding this comment.
Based on principle of power, I suspect that this similar adjustment should also be made.
// abstract
def lose[A](f: A => Nothing): F[A]
// concrete
def zero: F[Nothing] = lose(identity)There was a problem hiding this comment.
I'm fine with this! I think this actually better fits our current modeling with a monoidal / semigroupal hierarchy. This encoding I think predates some of the rest of that work and was originally part of that push.
EDIT: Remembering now, I think actually we went back and forth on this and at that time sentiment went otherwise, I am flexible on this - I think either makes sense but perhaps this is more coherent with the traditional modeling of say implementing Apply. At one point, I think interest went more towards having the monoidal, comonoidal, or unit items be the fundamentals, and everything else be derived (i.e. not principle of power, but principle of algebraic composition, as it were).
|
Does anyone else have thoughts on my latest comments? Specifically #2607 (comment). I am happy to try and push this across the finish line if Stephen is busy atm. This is phenomenal work, and I'd really like to land it before another 4 years pass 😄 |
|
Apologies! I have been preoccupied with my wedding. Seeing that there are comments here, I will endeavor to resolve them this weekend. If there is other feedback, I would appreciate having that up front so I can do them all in a few iterations, that said if it takes a few over that I understand - we all have constraints. |
Resolves #1935 and #2604.
Seeing an issue with binary compatibility I'm not sure how to resolve correctly.
Maybe someone can help me out? I'm probably misunderstanding the intended function of the BinCompat traits.
Included a very barebones doc page.
Since the laws are not formalized in ekmett's original, I've done a bit of guesswork / intiuitioneering on what the right laws look like. Open to discussion.