Add Is constructor for Leibniz equality #1178

tel · 2016-07-05T05:52:36Z

(See #1177 for initial discussion)

This PR adds Leibniz type equality under the name A Is B. Leibniz equality is an improvement over Predef.=:= as it can be substituted into type expressions and as it has more computational meaning. Both of these add power and convenience to Is which makes it appealing for certain kinds of pure functional work. I am, for instance, using a local version of this in a Cats-based lens library I'm working on to implement a generalized Equality[S, T, A, B] optic at the base of the optical hierarchy. It also shows up nicely for making GADTs with more computational integrity.

This is my first Cats contribution so there's probably a lot missing—please let me know how to continue to develop it.

Questions

I've simplified the Scalaz version back to one they used previously which appears to not play as nicely with subtyping. I'm not sure if this is a good idea... but it's undeniable that this version is clearer.
Is Is a good name? Also possible are TEq, Leib, and Leibniz. I like Is since it's very direct.
How can I better document this?
What is the right way to add tests?
What methods or companion object functions are missing? Are there any I have right now that are suspect?

Before we can land

Rename cats.eq to cats.evidence
Decide about design to maximize allocation and inlining
Determine whether or not to include def fromPredef[A, B](eq: A =:= B): A Is B
- Pros greater convenience
- Cons not strictly valid in a constructive sense; may be possible to generate invalid inferences?
Add equality tests at the type level by porting some notion of Shapeless's illtyped macro
Add basic tests showing design of implicits working without imports
Add basic tests to show that methods don't throw
Tests that we aren't reallocating
Decide what to call from ({from, reverse, flip, mirror, symm, inverse})
Determine the appropriate @inline design

Implicits spec

refl is available whenever there is an implicit need for A Is A without extra imports

adelbertc · 2016-07-05T06:30:11Z

core/src/main/scala/cats/eq/Is.scala

+    * implicit conversion to the coercion function.
+    */
+  implicit def witness[A, B](t: A Is B): A => B =
+    t.subst[A => ?](identity)


Hm I don't know about this one as it might bring in implicit conversions that may be undesired.. perhaps turn this into a method on the type class itself?

Sounds good. I'll update this presently.

non · 2016-07-05T15:58:13Z

Minor formatting nit: can you reformat your comments like this?

/**
 * We prefer the Java-style comment syntax.
 */

tel · 2016-07-05T17:25:48Z

Formatting fixed! 👍

tel · 2016-07-05T17:28:58Z

Some more questions:

I placed this in an eq package with expectation that someone will later want to add Liskov—but this might be premature.

codecov-io · 2016-07-05T18:17:41Z

Codecov Report

Merging #1178 into master will decrease coverage by 0.16%.
The diff coverage is 22.22%.

@@            Coverage Diff             @@
##           master    #1178      +/-   ##
==========================================
- Coverage   92.49%   92.33%   -0.17%     
==========================================
  Files         246      247       +1     
  Lines        3891     3900       +9     
  Branches      136      137       +1     
==========================================
+ Hits         3599     3601       +2     
- Misses        292      299       +7

Impacted Files	Coverage Δ
core/src/main/scala/cats/evidence/Is.scala	`22.22% <22.22%> (ø)`

Continue to review full report at Codecov.

Legend - Click here to learn more
Δ = absolute <relative> (impact), ø = not affected, ? = missing data
Powered by Codecov. Last update 94a2e3c...78960e2. Read the comment docs.

kailuowang · 2016-07-07T15:08:21Z

Thanks very much @tel, I had a discussion with @milessabin at gitter IRT testing such code in cats
For your reference
https://gitter.im/typelevel/cats?at=577e6d647aeb0805276ec94e

non · 2016-07-07T15:19:13Z

This looks good to me. Thanks!

One question: how do we feel about a cats.eq package? I have to admit I'm nervous that it's a bit too specialized. Would something like cats.witness or cats.evidence work instead? I can imagine more types living in those packages.

tel · 2016-07-07T16:30:22Z

@kailuowang Great, thanks! I'll take a look and make some plans to investigate this again perhaps this weekend.

@non I immediately agree witness, evidence, proof feels nicer than eq specifically. Of those, I think evidence is perhaps the best: proof feels too heady/academic, witness makes me think of the actual to and fro functions in an isomorphism—it feels specialized. Then, evidence feels both general and already shows up sometimes as the name of implicit arguments. I think that's appropriate. So color my bikeshed red.

tel · 2016-07-07T16:32:18Z

Just to copy some of Miles' comments into this thread:

@kailuowang: looks like we didn’t test the negative cases. I was thinking how do we test those without using shapeless’ illtyped

@milessabin Typically you test by allowing a type to be inferred and then checking it by ascribing.
You could have a test dependency on shapeless for that. Or copy and paste the implementation into the Cats tests.
... it's so small it's probably less effort to have a local copy.

non · 2016-07-07T18:08:13Z

@tel great! thanks for tolerating my bike shed commentary ;)

johnynek · 2016-07-11T14:16:04Z

core/src/main/scala/cats/eq/Is.scala

+ * equalities to be substituted into many more complex type expressions.
+ */
+abstract class Is[A, B] {
+  def subst[F[_]](fa: F[A]): F[B]


bikeshed: could we call this substitute or something? I don't think it is worth saving a few chars personally.

I'm fine with that personally. I defer to Cats House Style whatever that is.

johnynek · 2016-07-11T14:37:24Z

Can we have a simple test just to exercise a few things here:

implicit resolution works as expected without imports
each method doesn't do anything terrible like throw.
if A Is B then subst(x) eq x (check that we are never reallocating).

tel · 2016-07-12T02:44:25Z

@johnynek I think a good spec around what allocations are acceptable (if any) is good. I added some todo items before landing including working with those. That said, I don't understand what you're trying to say with your example test. Could you rephrase?

tel · 2016-07-12T02:45:55Z

@johnynek I also changed the docs on the class—let me know if you feel that's any better and, as necessary, how I can keep improving it.

johnynek · 2016-07-12T16:52:06Z

core/src/main/scala/cats/eq/Is.scala

-    def subst[F[_]](fa: F[A]): F[A] = fa
-  }
+  implicit def refl[A]: A Is A =
+    reflAny.asInstanceOf


I think scala may infer Nothing as the type parameter here and you may need to instead write: reflAny.asInstanceOf[A Is A]

Thanks! Fixed!

On Tue, Jul 12, 2016 at 12:52 PM P. Oscar Boykin [email protected]
wrote:

In core/src/main/scala/cats/eq/Is.scala
#1178 (comment):

*/

implicit def refl[A]: A Is A = new Is[A, A] {

def subst[F[_]](fa: F[A]): F[A] = fa

}

implicit def refl[A]: A Is A =

reflAny.asInstanceOf

I think scala may infer Nothing as the type parameter here and you may
need to instead write: reflAny.asInstanceOf[A Is A]

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/typelevel/cats/pull/1178/files/5558bb1d0d0c37e067f4efdc2a8e8b8debd63690..7a9aa14fa80f0448609b869d228a35d0a6c746b1#r70476249,
or mute the thread
https://github.com/notifications/unsubscribe/AAAEdbdm8tLOyt-yPFKkeYP6Um95z7Lkks5qU8Y9gaJpZM4JEy9z
.

johnynek · 2016-07-12T17:08:27Z

What about adding this method to object:

def fromScala[A, B](implicit ev: A =:= B): A Is B =
  reflAny.asInstanceOf[A Is B]

I can't see how this cast is unsafe, though it is a bit ugly. Can you think of reasons (aside from casting distaste) not to add this? It cannot be unsound, right?

The reason I want this, I do sometimes have A =:= B instances and would like to use this more powerful tool when I only have access to A =:= B.

johnynek · 2016-07-12T21:17:22Z

core/src/main/scala/cats/evidence/Is.scala

+  @inline final def compose[C](prev: C Is A): C Is B =
+    prev andThen this
+
+  @inline final def from: B Is A =


what about calling this reverse?

I'm not a huge fan of from, but I was taking it from some other sources. Calling it reverse feels alright since underlying A Is B is an actual process from A to B, but I sort of want to wipe that notion away. It's incidental instead of important. So, in order of my preference I like:

flip

mirror

reverse

from

But any of the above are acceptable to me.

I like flip.

Just changed it actually!

On Tue, Jul 12, 2016 at 7:06 PM P. Oscar Boykin [email protected]
wrote:

In core/src/main/scala/cats/evidence/Is.scala
#1178 (comment):

* contexts. This can be a more powerful assertion than A =:= B and is more

* easily used in manipulation of types while avoiding (potentially

* erroneous) coercions.

* A Is B is also known as Leibniz equality.

*/
+abstract class Is[A, B] {

def subst[F[_]](fa: F[A]): F[B]

@inline final def andThen[C](next: B Is C): A Is C =

next.substA Is ?

@inline final def compose[C](prev: C Is A): C Is B =

prev andThen this

@inline final def from: B Is A =

I like flip.

—
You are receiving this because you were mentioned.
Reply to this email directly, view it on GitHub
https://github.com/typelevel/cats/pull/1178/files/75d99c44800c0d152e7a093819b87af371f75003#r70538890,
or mute the thread
https://github.com/notifications/unsubscribe/AAAEdWW9A5h087h9IzJYCnKtQC0KWGYEks5qVB4CgaJpZM4JEy9z
.

Just renamed it!

tel · 2016-07-12T23:03:38Z

Another question with respect to performance: I've been recently sort of liberally decorating things with @inline but I have little understanding as to when is a good time to ask for inlining or not. Since ideally most of this code ought to just boil away I think aggressive @inlineing is probably correct, but I'd like the opinion of someone more familiar with JVM/Scala inlining.

johnynek · 2016-07-12T23:08:31Z

What do you think of these:

  // A <: B
  sealed abstract class Sub[A, +B] {
    def co[F[+_]](f: F[A]): F[B]
    def contra[F[-_]](f: F[B]): F[A]
    def andThen[B1 >: B, C](that: Sub[B1, C]): Sub[A, C] =
      that.co[({type G[+T]=Sub[A, T]})#G](this)
  }
  object Sub {
    implicit def reflS[B, A <: B]: Sub[A, B] = new Sub[A, B] {
      def co[F[+_]](f: F[A]): F[B] = f
      def contra[F[-_]](f: F[B]): F[A] = f
    }

    def toSuper[A, B](s: Sub[A, B]): Super[B, A] =
      s.contra[({type G[-T]=Super[B, T]})#G](Super.reflSuper[B, B])
  }
  // A >: B
  sealed abstract class Super[A, -B] {
    def contra[F[-_]](f: F[A]): F[B]
    def co[F[+_]](f: F[B]): F[A]
    def andThen[B1 <: B, C](that: Super[B1, C]): Super[A, C] =
      that.contra[({type G[-T]=Super[A, T]})#G](this)
  }
  object Super {
    implicit def reflSuper[B, A >: B]: Super[A, B] = new Super[A, B] {
      def contra[F[-_]](f: F[A]): F[B] = f
      def co[F[+_]](f: F[B]): F[A] = f
    }
    def toSub[A, B](s: Super[A, B]): Sub[B, A] =
      s.co[({type G[+T]=Sub[B, T]})#G](Sub.reflS[B, B])
  }

which seem like the analogous versions of this for subtyping/supertyping.

tel · 2016-07-13T03:38:22Z

There's Liskov from scalaz that handles both of those ideas at once. Amusingly, it looks like Scala is smart enough to naturally have B >: A lift up to [F]: F[B] => F[A]

Here's a simplified version:

abstract class IsA[-A, +B] {
  def substitute[F[-_]](fb: F[B]): F[A]
}

object Sub {

  // principal basis
  def isa[A, B >: A]: A IsA B = new Isa[A, B] {
    def substitute[F[-_]](fb: F[B]) = F[A]
  }
}

Generally I'm not familiar enough with subtyping in a language like Scala to talk about the value of Liskov/IsA, but I'm sure others would know more. On my experience alone I can't promote including these.

johnynek · 2017-03-15T21:24:28Z

I hear you.

For Monad I can't think of a good description, personally. It is very abstract. For Liebniz I think we all can. We can add in the comments links to where to read more, but I'm not crazy about every deep principle, of which there are many, using a possibly obtuse name to encourage users to learn more. From my experience at large-ish companies, that does not help me sell scala as an appealing method to develop software, and like I said, that is really important to me.

My vote in this case is to keep Is or Same or something like that and we should feel free to link to as many interesting bodies of work for those that need to learn more.

PS: I since opened this PR to scala:
scala/scala#5623

which I hope to have merged in 2.13, so this distinction with =:= and <:< will go away then. Lastly, I can't see any example where =:= is actually weaker than Is[A, B] or Liebniz[A, B] just that it lacks a method to prove that in the type system. Are there legitimate instances of A =:= B where it would have been impossible to construct Is[A, B]? Since we can only make =:= with refl, and it could have had def sub[F[_]](f: F[A]): F[A] = f, it seems to me that implies that in principle it is just as strong, just that the compiler can't see it.

non · 2017-03-15T21:32:23Z

My vote is that we use both, and alias one to the other. I don't think there's a reason to forbid or force people to use either name, and unlike some other types that we have chosen not to do this for, there is literally only one instance with one method so I don't think there is a particularly high documentation burden created by supporting both.

adelbertc · 2017-03-15T23:38:07Z

Wow, re-reading my previous comment, talk about terrible grammar. Guess that's when happens when I attempt to reply to things while amped on coffee.

Are there legitimate instances of A =:= B where it would have been impossible to construct Is[A, B]

That's an interesting question, I'll have to think about that some more. I know S11 has written extensively on related topics:

My vote is that we use both, and alias one to the other.

Not surprisingly my vote would be to use Leibniz for the actual definition and alias Is.

non · 2017-03-16T16:50:50Z

@tel Would you be willing to add a type alias in cats/evidence/package.scala? Something like:

package cats

package object evidence {
  type Leibniz[A, B] = cats.evidence.Is[A, B]
}

tel · 2017-03-16T19:03:49Z

@non Can do. In terms of moving to merger, should I rebase this patch to the mainline as well?

non · 2017-03-16T20:09:41Z

Yes, I think so, thanks. Also, you might want to create a single test that exercises this to make the codecov warnings pass. Something like:

test("Is / Leibniz") {
  def cast1[A, B](as: List[A])(implicit ev: A Is B): List[B] = ev.substitute(as)
  cast1[Int, Int](1 :: 2 :: 3 :: Nil)

  def cast2[A, B](as: List[A])(implicit ev: Leibniz[A, B]): List[B] = ev.substitute(as)
  cast2[Int, Int](1 :: 2 :: 3 :: Nil)
}

(Just compiling successfully is as much of a test as we need, and will ensure those lines are covered.)

Thanks for sticking with this!

non · 2017-03-17T04:35:45Z

LGTM 👍

(We can add more coverage tests at some point but this has been hanging out for awhile and I think it's worth merging soon.)

tel · 2017-03-18T03:22:46Z

🎸

adelbertc reviewed Jul 5, 2016
View reviewed changes

johnynek reviewed Jul 11, 2016
View reviewed changes

johnynek reviewed Jul 12, 2016
View reviewed changes

tel added 15 commits March 16, 2017 15:02

Add Is constructor for Leibniz equality

9481eed

Remove Id witness implicit favoring explicit conversion

705900d

Fix comment formatting

11dacb5

Add newline at end of file to pass style checks

07d1a60

better documentation and inlinability

374d0bb

refactor cats.eq to cats.evidence

27f7df6

explicit type specialization for reflAny cast

c3a66ca

make Is extend Serializable

1a8f2aa

convert implicit def predefEq to a Is method

7dd4f9a

add unsafeFromPredef for consideration

a93db93

rename subst to substitute and add docs

36f58fa

fix to javadoc style comment doc for unsafeToPredef

533cb36

liberally decorate with @inline

673d3cd

add some more documentation of Is methods

7ce238d

fix document formatting to prevent formatting errors

e7b3ea6

tel added 2 commits March 16, 2017 21:45

Add Leibniz alias for cats.evidence.Is

65b8811

Add test for Leibniz / Is; check only

78960e2

tel force-pushed the feat-add-leibniz branch from a7e8feb to 78960e2 Compare March 17, 2017 01:53

kailuowang approved these changes Mar 17, 2017

View reviewed changes

johnynek merged commit f6ef91e into typelevel:master Mar 17, 2017

peterneyens mentioned this pull request Mar 21, 2017

Add Leibniz equality #1177

Closed

kailuowang added this to the 1.0.0-MF milestone Aug 1, 2017

Add Is constructor for Leibniz equality #1178

Add Is constructor for Leibniz equality #1178

Conversation

tel commented Jul 5, 2016 • edited Loading

Questions

Before we can land

Implicits spec

Choose a reason for hiding this comment

Choose a reason for hiding this comment

non commented Jul 5, 2016

tel commented Jul 5, 2016

tel commented Jul 5, 2016

codecov-io commented Jul 5, 2016 • edited Loading

Codecov Report

kailuowang commented Jul 7, 2016

non commented Jul 7, 2016

tel commented Jul 7, 2016

tel commented Jul 7, 2016

non commented Jul 7, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johnynek commented Jul 11, 2016

tel commented Jul 12, 2016

tel commented Jul 12, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

johnynek commented Jul 12, 2016

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

tel commented Jul 12, 2016

johnynek commented Jul 12, 2016

tel commented Jul 13, 2016 • edited Loading

johnynek commented Mar 15, 2017 • edited Loading

non commented Mar 15, 2017

adelbertc commented Mar 15, 2017

non commented Mar 16, 2017 • edited Loading

tel commented Mar 16, 2017

non commented Mar 16, 2017 • edited Loading

non commented Mar 17, 2017

tel commented Mar 18, 2017

tel commented Jul 5, 2016 •

edited

Loading

codecov-io commented Jul 5, 2016 •

edited

Loading

tel commented Jul 13, 2016 •

edited

Loading

johnynek commented Mar 15, 2017 •

edited

Loading

non commented Mar 16, 2017 •

edited

Loading

non commented Mar 16, 2017 •

edited

Loading