[WIP] #1234 - Leibniz & Liskov #1314

hobwekiva · 2017-01-16T05:48:32Z

I have ported some of the original Leibniz / Liskov functionality over to scalaz8 branch.

I am still not clear on whether the upper and lower bounds on Leibniz are needed. I understand that without them subst[F] on F[_ <: X] won't work, but is it really ever used in such a context?
I changed some of the names, but I am happy to stick with scalaz7 naming if that's an issue.
It is possible to generalize Leibniz to higher-kinded types (e.g. equality between type constructors).
There are no lower functions yet since there is no Injective typeclass.
A lot of Liskov companion object functions are still missing.
Should I keep all companion object functions in a ...Functions trait?
=:= and <:< might have most of the required functionality (most importantly substitute) in 2.13.
I have adapted some ideas from a similar PR to cats by @tel. The top comment in Leibniz is from the article.

TomasMikula · 2017-01-16T13:24:35Z

I am still not clear on whether the upper and lower bounds on Leibniz are needed. I understand that without them subst[F] on F[_ <: X] won't work, but is it really ever used in such a context?

I have used it in such context before.

hobwekiva · 2017-01-16T21:34:27Z

@TomasMikula My concern is that it adds a lot of noise to an otherwise simple idea, makes type-inference harder, and makes some of the user-facing methods harder to use because you have to supply them with additional type parameters (e.g. lift functions) :( Furthermore, you can make a Groupoid/Category instance only for some specific choice of L and H (since there is no GeneralizedGroupoid right now). And AFAIK scalaz is moving away from subtyping / variance.

Overall it feels like it's a marginal improvement with a non-trivial cost. The same constraints >: L <: H can always be supplied using a typeclass during construction (it doesn't have to be <~<, whatever is enough/necessary), e.g:

class X[A <: B](a: A)
// can be replaced by:
class X[A](a: A, ev: A <~< B)
// or if the evidence is not required after construction:
class X[A] private[X] (a: A)
object X {
  def apply[A](a: A)(implicit ev: A <~< B): X[A] = ???
}

<: bounds are basically poor man's typeclasses and can always be replaced by them. But that might require modifying an existing class.

What if we had BoundedLeibniz[L, H, A, B] / GeneralizedLeibniz[L, H, A, B] and Leibniz[A, B] wrapping it instead? That would solve all problems with some minor code duplication.

Another option is Leibniz[L, H, A, B] and ===[A, B] extends Leibniz[Nothing, Any, A, B] (or type ... =) and all methods on syntax traits.

Technically, Liskov can also be generalized along the same direction.

TomasMikula · 2017-01-16T22:49:30Z

The same constraints >: L <: H can always be supplied using a typeclass

The problem is when the type constructor with type bounds is not under your control, so you can't change it. Do we say "f*** you" to all such use cases?

Aside: I think Scala's bounds checking is unnecessarily strict. If you have

class Foo[A <: Bar]

I believe you should be allowed to talk about Foo[Int] (it just might be uninhabited). This would make things simpler.

hobwekiva · 2017-01-16T23:27:03Z

What do you think of the solutions I outlined at the end of my previous post? I am mostly concerned with type-inference on methods and combinators and I'd like to optimize for the most common case of Leibniz[Nothing, Any, A, B].

P.S.

Do we say "f*** you" to all such use cases?

Well, it is not like every single data type taking kind * -> * type parameters in Scalaz provides you a way to bound them with >: L <: H. Such constraints are unlikely to come up when you live in the Scalazzi world. Scalaz says "f*** you" to many other things like null, non-parametric equals, hashCode, exceptions, unconstrained side-effects, some of scala collections, (ought to say that to with intersection types) etc.

I believe you should be allowed to talk about Foo[Int] (it just might be uninhabited).

That would raise some interesting questions like:

trait Bar { type Out = String }
trait Baz { type Out = Boolean }
class Foo [A <: Bar] { type Out = A#Out }
type X = Foo[Baz]#Out // what is X?

TomasMikula · 2017-01-17T01:49:22Z

What do you think of the solutions I outlined at the end of my previous post?

I like the one with wrapping.

Not sure how "all methods on syntax traits" helps if === is just a type alias (unless the methods are named differently anyway).

That would raise some interesting questions like:

trait Bar { type Out = String }
trait Baz { type Out = Boolean }
class Foo [A <: Bar] { type Out = A#Out }
type X = Foo[Baz]#Out // what is X?

Good point. For that the constraint would have to be checked.

hobwekiva · 2017-01-17T04:59:06Z

This is roughly what I had in mind. Turns out there is quite a bit of duplication needed to completely avoid allocations (calling methods on BoundedLeibniz would require unwrapping and then wrapping Leibniz again). I also implemented LeibnizK there (useful for type-aligned sequences of natural transformations).

TomasMikula · 2017-01-18T04:47:29Z

If Leibniz extended AnyVal, wrapping would be without allocation, right?

S11001001 · 2017-03-03T00:52:19Z

@TomasMikula Not quite.

TomasMikula

For the sake of moving forward, I propose to merge this and add type bounds if/when needed.

hobwekiva · 2017-06-04T10:04:40Z

Sorry for neglecting this PR, I've been experimenting with Leibniz, Liskov, and a number of other related ideas in a separate project. I understand why you want bounded version of Leibniz now.

hobwekiva · 2017-06-04T10:13:37Z

Some of the new "inventions" and old goodies:

Is - unbounded Leibniz.
As - unbounded Liskov.
Leibniz - bounded Leibniz.
Liskov - bounded Liskov.
As1 - unbounded Liskov that uses existential types for its encoding, which allows you to call methods like def f[X <: B](x: X): F[X] given a: A and As1[A, B] and get F[A] back.
Liskov1 - ditto, but bounded.
IsK - higher-order Leibniz. I have tried poly-kinded Leibniz and Liskov (Ξ = AnyKind) and they are a lot of fun to play with, you can implicitly summon things like Some <~< Option and Monad <~< Functor.
IsF - equality of F-Bounded polymorphism types (use case gist).
Eq - experiments showed that you can make === even more powerful if you have an ability to lift term equality a === b to singleton type equality a.type === b.type (e.g. this gist, this one, and this one; the last gist also shows how to "prove" stuff in Scala, Idris-style). But you need an equality that satisfies forall (a: A) (b: A) (f: A -> Bool) . f(a) == f(b) <===> a === b assuming f follows Scalazzi rules.
Bounded - witnesses that L <: A <: H. Haven't really found the use so far.

I also found a way to emulate union types on Scala2 and I think it can be made safe but it is extremely mmm hacky in its appearance. Useful if you want to turn A <~< B into Liskov[L, H, A, B] given that you know that L <: A <: H and L <: B <: H.

TomasMikula · 2017-06-04T22:04:30Z

If you want to replace this PR with your new Is, As, Leibniz, Liskov, IsK, I would give it a 👍.

experiments showed that you can make === even more powerful if you have an ability to lift term equality a === b to singleton type equality a.type === b.type (e.g. this gist, this one, and this one

In the last two gists there doesn't seem to be any guarantee that the types you are asserting to be equal are singleton types.

the last gist also shows how to "prove" stuff in Scala, Idris-style

This is nice. Could it be used to prove something about types that are not fully known at compile time? E.g. how would you prove that M + N = N + M when all you know at compile time is M <: Nat, N <: Nat?

But you need an equality that satisfies forall (a: A) (b: A) (f: A -> Bool) . f(a) == f(b) <===> a === b

I suppose you meant forall (a: A) (b: A) . (forall (f: A -> Bool) . f(a) == f(b)) <===> a === b.

hobwekiva · 2017-06-05T16:26:34Z

If you want to replace this PR with your new Is, As, Leibniz, Liskov, IsK, I would give it a 👍.

Okay, awesome. I'll get it done this week.

In the last two gists there doesn't seem to be any guarantee that the types you are asserting to be equal are singleton types.

Right, those are early prototypes before I got into singleton types 😉

This is nice. Could it be used to prove something about types that are not fully known at compile time? E.g. how would you prove that M + N = N + M when all you know at compile time is M <: Nat, N <: Nat?

Well, ideally you would have the compiler (or a compiler plugin) figure out that since the proof is total and equality is a singleton (as in there is only one implementation according to free theorems), you can just "force" it for arbitrary M <: Nat and N <: Nat. I guess you could have some kind of

def assertTotal[P[_ <: Nat, _<: Nat]: Proof]
(proof: [M <: Nat, N <: Nat] (M, N) => P[N, M]): P[N, M]

I suppose you meant forall (a: A) (b: A) . (forall (f: A -> Bool) . f(a) == f(b)) <===> a === b).

Yep.

Conflicts: base/src/main/scala/scalaz/typeclass/Liskov.scala base/src/main/scala/scalaz/typeclass/LiskovFunctions.scala base/src/main/scala/scalaz/typeclass/LiskovInstances.scala base/src/main/scala/scalaz/typeclass/LiskovTypes.scala

TomasMikula

Overall, great stuff!

TomasMikula · 2017-06-20T17:38:49Z

base/src/main/scala/scalaz/data/Leibniz.scala

+    * explicitly coerce types. It is unsafe, but needed where Leibnizian
+    * equality isn't sufficient.
+    */
+  def unsafeForce[A, B]: A === B =


Why does this unsafeForce not need @SuppressWarnings(Array("org.wartremover.warts.AsInstanceOf")), while all of the others do?

Scalaz doesn't use WartRemover as far as I can tell, I will simply remove this annotation. All asInstanceOf require it, I was just being lazy with warnings in leibniz 😉

TomasMikula · 2017-06-20T17:39:22Z

base/src/main/scala/scalaz/data/Liskov.scala

+  //  final def liftCt[F[-_]]: F[B] <~< F[A] = {
+  //    type f[+α] = F[α] <~< F[A]
+  //    substCo[f](refl)
+  //  }


👎 for commented-out code.

hobwekiva · 2017-06-20T20:19:04Z

It looks like CI checks failed because it couldn't download SBT.
EDIT: nvm all green now

TomasMikula · 2017-08-11T09:20:24Z

Sorry for waiting so long, I just wanted to give others the chance to review. If you find time to resolve the conflicts, I will merge this. If not, I will try to resolve them myself. Thanks!

hobwekiva · 2017-11-22T03:05:19Z

#1524

beer-avalanche added 5 commits January 14, 2017 22:15

Moved liskov to data, added more methods on Liskov and Leibniz.

a1d3aaa

final all methods, isa -> reify.

ce2b027

More comments.

4641883

More comments in Liskov.

53e58ae

More comments.

09c4dbd

xuwei-k added the scalaz8 label Jan 16, 2017

beer-avalanche added 2 commits January 16, 2017 00:58

bracket is technically unsafe.

2686e79

Renamed isa back.

6656f47

Added bounds to Leibniz.

afadebd

Minor fixes in the comments.

88e4137

TomasMikula approved these changes Jun 4, 2017

View reviewed changes

beer-avalanche added 3 commits June 20, 2017 03:23

As, Is, IsK, Liskov.

7b27745

Merge branch 'series/8.0.x' into leibniz-liskov

fa23a55

Conflicts: base/src/main/scala/scalaz/typeclass/Liskov.scala base/src/main/scala/scalaz/typeclass/LiskovFunctions.scala base/src/main/scala/scalaz/typeclass/LiskovInstances.scala base/src/main/scala/scalaz/typeclass/LiskovTypes.scala

New As from leibniz.

bd08372

TomasMikula reviewed Jun 20, 2017

View reviewed changes

Consistency.

a01f328

TomasMikula approved these changes Jun 20, 2017

View reviewed changes

hobwekiva mentioned this pull request Nov 22, 2017

Leibniz & Liskov : Part 1 #1524

Merged

hobwekiva closed this Nov 22, 2017

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

[WIP] #1234 - Leibniz & Liskov #1314

[WIP] #1234 - Leibniz & Liskov #1314

hobwekiva commented Jan 16, 2017 •

edited

Loading

TomasMikula commented Jan 16, 2017

hobwekiva commented Jan 16, 2017 •

edited

Loading

TomasMikula commented Jan 16, 2017

hobwekiva commented Jan 16, 2017

TomasMikula commented Jan 17, 2017

hobwekiva commented Jan 17, 2017

TomasMikula commented Jan 18, 2017

S11001001 commented Mar 3, 2017

TomasMikula left a comment

hobwekiva commented Jun 4, 2017

hobwekiva commented Jun 4, 2017 •

edited

Loading

TomasMikula commented Jun 4, 2017

hobwekiva commented Jun 5, 2017 •

edited

Loading

TomasMikula left a comment

TomasMikula Jun 20, 2017

hobwekiva Jun 20, 2017

TomasMikula Jun 20, 2017

hobwekiva commented Jun 20, 2017 •

edited

Loading

TomasMikula commented Aug 11, 2017

hobwekiva commented Nov 22, 2017

[WIP] #1234 - Leibniz & Liskov #1314

[WIP] #1234 - Leibniz & Liskov #1314

Conversation

hobwekiva commented Jan 16, 2017 • edited Loading

TomasMikula commented Jan 16, 2017

hobwekiva commented Jan 16, 2017 • edited Loading

TomasMikula commented Jan 16, 2017

hobwekiva commented Jan 16, 2017

TomasMikula commented Jan 17, 2017

hobwekiva commented Jan 17, 2017

TomasMikula commented Jan 18, 2017

S11001001 commented Mar 3, 2017

TomasMikula left a comment

Choose a reason for hiding this comment

hobwekiva commented Jun 4, 2017

hobwekiva commented Jun 4, 2017 • edited Loading

TomasMikula commented Jun 4, 2017

hobwekiva commented Jun 5, 2017 • edited Loading

TomasMikula left a comment

Choose a reason for hiding this comment

TomasMikula Jun 20, 2017

Choose a reason for hiding this comment

hobwekiva Jun 20, 2017

Choose a reason for hiding this comment

TomasMikula Jun 20, 2017

Choose a reason for hiding this comment

hobwekiva commented Jun 20, 2017 • edited Loading

TomasMikula commented Aug 11, 2017

hobwekiva commented Nov 22, 2017

hobwekiva commented Jan 16, 2017 •

edited

Loading

hobwekiva commented Jan 16, 2017 •

edited

Loading

hobwekiva commented Jun 4, 2017 •

edited

Loading

hobwekiva commented Jun 5, 2017 •

edited

Loading

hobwekiva commented Jun 20, 2017 •

edited

Loading