Added implementation of Eq[Free] #3949
Conversation
|
@LukaJCB I'm going to add a couple other instances actually. Can also test with something other than |
djspiewak
force-pushed
the
feature/free-eq
branch
from
9e79eec to
157efa0
Compare
|
@LukaJCB I think this is ready for a final look |
|
|
||
| // TODO HashLaws#sameAsUniversalHash is really dodgy | ||
| // checkAll("Free[Option, Int]", HashTests[Free[Option, Int]].hash) | ||
| checkAll("Free[Option, Int]", PartialOrderTests[Free[Option, Int]].partialOrder) |
There was a problem hiding this comment.
is it the case that f1: Free[Option, Int] == f2: Free[Option, Int] <=> f1.runTailRec == f2.runTailRec?
That seems like a nice property to have, but I don't see that if the current code can get it.
If it can't get it, what does this notion of equality mean?
There was a problem hiding this comment.
I guess if I read the docs I might learn something...
So, I guess the property I mention is not true, but one way: if we are "free-equal" then we are option-equal.
That might be a nice test to add to strengthen the tests here (e.g. I think returning that all items are equivalent always passes the laws, but isn't what we really want, adding a law I suggest here rules out many bad implementations since happening to get equal Option[Int] is unlikely.
There was a problem hiding this comment.
So, I guess the property I mention is not true, but one way: if we are "free-equal" then we are option-equal.
I believe this is the case. Caffeine is still working its way into my brain, but at first glance, I think this property holds at least because Either is monotone with respect to Eq (meaning that a1 === a2 implies Right(a1) === Right(a2) and Left(a1) === Left(a2) and the converse), which means that this would reduce to an inductive argument over that monotonicity. But, as I'll argue in a minute, this restriction on the pattern functor is probably not needed.
The stronger bidirectional implication definitely doesn't hold, since Free.pure(42).runTailRec === Free.suspend(Some(42)).runTailRec, but they would not be considered equal by the structural definition of Eq. You can build versions of this which don't rely on coyoneda as well. Interpreting a Free into a monad is a stronger process than simply inspecting its defining structure, which is what this Eq does. In a sense, this is the reification of the intuition that, for almost any value, there are many different programs which can produce that outcome. The structural Eq inspects the program, while runTailRec inspects the outcome.
What you're saying is that, for any programs that are structurally equal, the outcomes they produce when run must also be equal. I believe this holds for all suspension functors which are deterministic monads (e.g. race makes IO a nondeterministic monad, which is why it is generally ignored as a combinator). Of course, this property is only defined for suspension functors which also form monads, which will not be true in general for most of the functors with which this kind of technique is useful, so I'm not sure we need to formalize this intuition.
| // TODO HashLaws#sameAsUniversalHash is really dodgy | ||
| // checkAll("Free[Option, Int]", HashTests[Free[Option, Int]].hash) | ||
| checkAll("Free[Option, Int]", PartialOrderTests[Free[Option, Int]].partialOrder) | ||
| checkAll("Free[ExprF, String]", EqTests[Free[ExprF, String]].eqv) |
| } | ||
| } | ||
|
|
||
| Show[Free[Option, Int]] |
There was a problem hiding this comment.
Is this just for checking that you can summon the show instance?
Look ma, no documentation! Okay that's not entirely true, but it's close to true. Documentation coming.
So this probably looks a little odd if you're unfamiliar with recursion schemes.
Freeis a fixed point (similar toFixorMu), but we don't normally think of it that way. IMOFreeis a lot more useful in this role thanFixis, and thisEqinstance is one of the first steps in being able to unlock this power on top of vanilla Cats (rather than requiring something like Droste for even trivial cases).Anyway, examples to come. There are some nice ones of how this can be leveraged in practice, I just haven't written them down yet.
Poke @Baccata since I promised you this a while back.