SI-2712 Add support for partial unification of type constructors

[milessabin]

An improvement to type inference for type constructors has been added, enabled by the -Ypartial-unification command line option (also enabled in -Xexperimental mode). This fixes SI-2712 in the way suggested by Paul Chiusano in a comment on the issue. This has many benefits for libraries, such as Cats and Scalaz, which make extensive use of higher-kinded types.

With the feature enabled the following compiles,

def foo[F[_], A](fa: F[A]): String = fa.toString
foo { x: Int => x * 2 }

with the type variable F[t] solved as Int => t and the type variable A solved as Int. Previously the compiler would have rejected this programme because,

• The type parameter F of foo is a type constructor with a single type parameter, also known as kind * -> *.
• The provided type, Int => Int, which is a synonym for Function1[Int, Int], has an outer type constructor with two type parameters, or kind * -> * -> *.
• The type inference algorithm required that the kinds of type parameters and their corresponding type arguments must be the same.

Partial unification solves this problem by treating outer type constructors at call sites as partially applied. In the example above, the compiler does the equivalent of creating a local type alias with the correct kind and using that at the call site,

type Partial[t] = Int => t 
foo[Partial, Int] { x: Int => x * 2 }

Partial has the same kind as the type argument F of foo and so this compiles successfully.

The implementation partially applies type constructors from left to right, leaving the rightmost type parameters free. This works well with binary type constructors with a natural right bias, such as Either, Xor in Cats and Scalaz's disjunction. For example a map operation defined with the signature illustrated below will naturally map over the value of the righthand type, corresponding to validity, whilst leaving the value of the lefthand type untouched,

def map[F[_], A, B](fa: F[A])(f: A => B): F[B] = ...
val right: Either[String, Int] = Right(23)
val left: Either[String, Int] = Left("Invalid")
map(right)(_ + 1) // yields Right(24)
map(left)(_ + 1) // yields Left("Invalid")

An article by Daniel Spiewak expands on the consequences of this strategy.

A major benefit of enabling this feature is that existing workarounds for SI-2712, such as shapeless's Unpack and Cats and Scalaz's Unapply and their U suffixed operations are no longer necessary. This both simplifies code from the library implementor and users points of view, and also potentially reduces compile times by virtue of being implemented as a primitive component of type checking rather than being encoded via type level computation using implicits.

Enabling this feature only affects type inference hence code compiled separately with the feature enabled and disabled is fully binary compatible. There is a compiler plugin which makes this feature available for Scala 2.11.x and 2.10.x.

[non]

+1

I think this would be really great to get in for 2.12 -- given that it's off by default and fixes a longstanding known issue. Thanks for your hard work @milessabin!

[djspiewak]

There are no words to describe the kind of impact this would have on my daily use of Scala. I know it's very late in the 2.12 cycle, but I would love to see this make it.

[fommil]

Is there any way to know what impact enabling the flag has on existing code, e.g. running all the tests with the flag enabled? Or, indeed, on the community build.

[djspiewak]

@fommil The only problem I've seen it cause thus far was compiling scalaz (found by @runarorama). Specifically, it ran into some problems with type tags. I'm not sure if @milessabin fixed that particular bug or not, but that's literally the only problem I've seen.

[xuwei-k]

Here is scalaz result. I can remove some Unapply 😃
scalaz/scalaz@scalaz:3a37b10...xuwei-k:03d1fbc

[djspiewak]

If this does make it in for 2.12 (or even if it doesn't), the above should be expanded into a blog post somewhere. We need to be clear that this is very literally adding left-to-right curried type constructor semantics to Scala. I tend to think this is a good thing, and it lines up very very nicely with things the community is already doing by default (e.g. right-biased Xor), but it needs to be made clear.

[Blaisorblade]

it lines up very very nicely with things the community is already doing by default (e.g. right-biased Xor), but it needs to be made clear.

I'm guessing that's an heritage of Haskell's (here, from Either), where type inference works this way since ever. Hence, I conjecture no-Haskell Scalaers might especially need this explained.

[larsrh]

I'm guessing that's an heritage of Haskell's (here, from Either), where type inference works this way since ever.

Yes, but on top of that, in Haskell, left-to-right is the only thing you can do.

[raulraja]

+1 a much awaited fix, this would be great to have in 2.12

[milessabin]

@djspiewak the bug that @runarorama found, and a related one that @xuwei-k found are both fixed in this PR.

[markus1189]

I'm unreasonably excited about this! And if there is a chance to get this for 2.12 - oh my! What a start into the weekend. Awesome work @milessabin

[DavidGregory084]

This causes lots of pain and leads to lots of weird magic tricks in the source code of Scala libraries that are extremely off-putting to new contributors.
I would be very happy to see this fixed in 2.12 so that I don't ever have to understand how these tricks work or try to explain them to anybody else.

[smarter]

So, I personally like this idea (I implemented something similar in a branch of Dotty a while ago, but didn't pursue it further because of a million more urgent things), but there's a bunch of questions that need to be answered to go down that road, for example:

class X1
class X2
class X3

trait One[A]
trait Two[A, B]

class Foo extends Two[X1, X2] with One[X3]
object Test {
  def test[M[_], A](x: M[A]): M[A] = x

  val foo = new Foo
  test(foo) // M = ?, A = ?
}

With -Yhigher-order-unification off we get M=One, A=X3, but with -Yhigher-order-unification on we get M=[X]=>Two[X1,X], A=X2. Is this good or bad? I have no idea.

However, this seems pretty bad:

class X1
class X2
class X3

trait One[A]
trait Two[A, B]

class Foo extends Two[X1, X2] with One[X3]
object Test {
  def test[M[X] <: One[X], A](x: M[A]): M[A] = x

  val foo = new Foo
  test(foo) // M = ?, A = ?
}

With -Yhigher-order-unification off this works fine, but with -Yhigher-order-unification on, it fails with:

inferred type arguments [[Unify$1]Two[X1,Unify$1],X2] do not conform to method test's type parameter bounds [M[X] <: One[X],A]

in other words, M=[X]=>Two[X1,X], A=X2 is inferred and not rejected, even though this does not conform to the declared bounds.

[non]

@smarter Ouch! I'm assuming that it's trying Two[_, _] first because of the order of the mix-ins? If Foo extends One[X3] with Two[X1, X2] do things work as expected?

[smarter]

@non: Yup. You can play with it easily using the sbt project at https://github.com/milessabin/si2712fix-demo

[non]

@smarter It seems like this may just be a generalization of a pre-existing problem in Scala:

class X1
class X3

trait One[A]
trait Three[A]

class Foo31 extends Three[X1] with One[X3]

object Test {
  def test[M[X] <: One[X], A](x: M[A]): M[A] = x

  val foo31 = new Foo31
  test(foo31) // M = ?, A = ?
}

With this I get:

inferred type arguments [si2712.Three,si2712.X1] do not conform to method test's type parameter bounds [M[X] <: si2712.One[X],A]

This doesn't invalidate the point that there are some things that could stop type-checking. But I do think that it's consistent with the kinds of problems these constraints already have.

[runarorama]

Everyone on my team would very much like to see this in 2.12.

[ekmett]

👍 This would greatly simplify a lot of scala code we have

[wheaties]

👍 for this but have to agree with @djspiewak on a post explaining how things will work, espcially in light of what @smarter has put up there.

[larsrh]

With -Yhigher-order-unification off we get M=One, A=X3, but with -Yhigher-order-unification on we get M=[X]=>Two[X1,X], A=X2. Is this good or bad? I have no idea.

@smarter The fact that this yields different results already tells us that we're in ambiguous/unspecified territory here. I think changing behaviour is acceptable under these circumstances.

[etorreborre]

@djspiewak what's the effect on Emm?

[smarter]

@larsrh : changing behaviour is fine, but I don't think this can be done blindly: you need to think carefully about what semantics you want.

[djspiewak]

what's the effect on Emm?

I get to delete about 90% of the boilerplate, with an exponential decrease in compile time due to the dramatically smaller search space. I still need the Permute type classes, but all of the rest can be implemented in a very straightforward manner.

[djspiewak]

I'm sure that @milessabin would explain things far better than I, but here's a quick write-up of how the fix works and what kind of implications it has for type constructor design: https://gist.github.com/7a81a395c461fd3a09a6941d4cd040f2

[tpolecat]

Big 👍 for inclusion in 2.12 ... this would make my life much happier.

[lambdista]

👍 thank you @milessabin

[adriaanm]

Cool! Happy to have this go into M5 under a switch. I'm on vacation this week (hence the fat fingering on phone), but will take a look when I get back.

[adriaanm]

As a final consideration, I'd like to revisit @smarter's comment above (#5102 (comment)). My understanding is that it's about the order of places where we look for a type constructor of the expected arity. Currently, there must be one in the base type sequence (transitive closure of the extends clause -- BTS). After this change, the BTS is not consulted and we synthesize a type constructor of the right arity using the new logic.

Is this the order we want? Should we look at the BTS for existing type constructors of the right arity before we start synthesizing new ones?

PS: maybe it is the order we want, but I do think this change is important enough to double check and highlight in the release notes

[Blaisorblade]

Slight OT: TL; DR. Unlike I thought, pattern unification is by far too weak for the interesting scenarios.

So I figured I should really unsuggest it, and apologize a bit for suggesting it in the first place without doing enough homework, in particular to @milessabin and @mandubian.

If anybody is interested in the evidence, see (and comment) this Agda snippet:
https://gist.github.com/Blaisorblade/5284942a6a7bee22a372afe7d86beb98

[adriaanm]

@milessabin I'll let @retronym do the honors, but I think this is ready to merge.

Since this definitely merits inclusion in the release notes, could you update and expand the PR description to make it suitable for that? My last comment is probably one of the things that should be mentioned as a breaking change.

[milessabin]

@adriaanm will do. I'll flag up @smarter's example as something that warrants further investigation.

[retronym]

Merging now, I'll let @milessabin update the PR description with a small example of what this means to users

[milessabin]

Awesome! Thanks to everyone who contributed, and especially to @retronym and @adriaanm :-)

[TomasMikula]

Somewhat off-topic, but do you think that partial unification in implicit search could also have a similar solution?

Example:

object ImplicitSearchTest {
  import scala.language.higherKinds

  final case class KPair[F[_], G[_], A](_1: F[A], _2: G[A])

  trait Getter[A, B] {
    def get(a: A): B
  }

  implicit def leftProjection[F[_], G[_], A]: Getter[KPair[F, G, A], F[A]] =
    new Getter[KPair[F, G, A], F[A]] {
      def get(p: KPair[F, G, A]): F[A] = p._1
    }

  implicit def rightProjection[F[_], G[_], A]: Getter[KPair[F, G, A], G[A]] =
    new Getter[KPair[F, G, A], G[A]] {
      def get(p: KPair[F, G, A]): G[A] = p._2
    }

  implicit def composedRightProjection[F[_], G[_], A, B](implicit G: Getter[G[A], B]): Getter[KPair[F, G, A], B] =
    new Getter[KPair[F, G, A], B] {
      def get(p: KPair[F, G, A]): B = G.get(p._2)
    }

  trait Foo[A]
  trait Bar[A]
  trait Baz[A]

//type FooBarBaz[A] = KPair[Foo, KPair[Bar, Baz, ?], A]
  type FooBarBaz[A] = KPair[Foo, ({ type Out[X] = KPair[Bar, Baz, X] })#Out, A]

  implicitly[Getter[FooBarBaz[Int], Foo[Int]]] // error: could not find implicit value
  implicitly[Getter[FooBarBaz[Int], Bar[Int]]] // error: could not find implicit value
  implicitly[Getter[FooBarBaz[Int], Baz[Int]]] // error: could not find implicit value

  // if we create an intermediate alias, implicit search works
  type BarBaz[A] = KPair[Bar, Baz, A]
  type FooBarBaz1[A] = KPair[Foo, BarBaz, A]

  implicitly[Getter[FooBarBaz1[Int], Foo[Int]]] // OK
  implicitly[Getter[FooBarBaz1[Int], Bar[Int]]] // OK
  implicitly[Getter[FooBarBaz1[Int], Baz[Int]]] // OK
}

[Blaisorblade]

@TomasMikula IIUC, if you expanded implicitly into the needed calls to implicits, you need exactly this PR (and enabling the new behavior with -Ypartial-unification) to have the type arguments to the implicits inferred, right? Can you check if this works now? In principle it should, and e.g. the testcase https://github.com/scala/scala/pull/5102/files#diff-ecb4676a9b808a50a48374436ff39a29R17 suggests it also works in practice.

[TomasMikula]

@Blaisorblade huh, the example actually compiles as is. I probably added Miles's si2712fix-plugin to build.sbt and forgot to call reload or something similarly stupid before. Thanks for checking, anyway!

[OlivierBlanvillain]

I'm not sure the story is over, here are some examples which I think should compile with Ypartial-unification/si2712fix-plugin but don't.

[adriaanm]

Here's something to study: https://gist.github.com/paulp/71fa03ad85917f5fa02a3e8acbc98409 /cc @paulp

[djspiewak]

@adriaanm Wow… That definitely looks like a bug to me. Fabricating the Singleton out of nothingness is a neat trick.

[paulp]

Each extraneous factor I eliminate and it gets a little worse. It turns one doesn't need any compiler options at all - using the typelevel compiler is enough. I updated the gist to reflect this.

[djspiewak]

https://github.com/typelevel/scala/issues

[paulp]

Here's a sliver of a diff after adding logging. The side which mentions Singleton is of course TLC.

[djspiewak]

A guess would be that a change made to ensure inference doesn't throw away specific singleton types quite so aggressively that was meant to be behind a flag… isn't. It sounds more related to the 42.type implementation than SI-2712.

[paulp]

@djspiewak I think your guess will prove to be correct.

[paulp]

It figures to be this, from 8301e1f.

  case argTp@SingletonInstanceCheck(cmpOp, cmpArg) if settings.YliteralTypes =>

I'm supposing the side-effecting unapply is called, and then the settings guard is checked.

[milessabin]

Yup, this relates to the literal types PR rather than this one.