Add kind polymorphism #4108

odersky · 2018-03-12T18:39:19Z

This is an attempt to develop a minimal type safe form of (subtype-) kind polymorphism. At present, it's intended as a basis for discussion. @milessabin @adriaanm, others: It would be great to get your opinion.

An overview of the proposed scheme is in kind-polymorphism.md

julienrf · 2018-03-12T19:51:35Z

This is an interesting feature. It would be nice to see if it helps dealing with the kind-alignment issues we have in the new collections (between Map[_, _] and Iterable[_]). I remember having tried to play with typelevel-scala kind polymorphism support (which seems to have been the main source of inspiration here) and the result wasn’t better that without kind polymorphism: scala/scala-lang#651 (comment)

Also, I find it confusing to use an upper bound constraint to qualify the fact that a type parameter is poly-kinded. I think these are unrelated concepts. Maybe there is an analogy with the following at the value level? def foo(bar: Any), where bar is “polymorphic” by virtue of the fact that Any is a supertype of all types. But I’m not sure that’s a solid reason… Maybe we should think of a special syntax?

odersky · 2018-03-12T20:00:44Z

See also: scala/scala#5538

julienrf · 2018-03-12T21:11:23Z

docs/docs/reference/kind-polymorphism.md

+
+(todo: insert good concise example)
+
+Some technical details: `AnyKind` is a synthesized class just like `Any`, but without any members. It extends no other class.


So, no equals nor hashCode?

Since there's no way to create instances of AnyKind, I suppose it doesn't matter.

what is expected of .asInstanceOf[AnyKind]?

As "just as regular user" a ClassCastException seems perfectly reasonable.

AsInstanceOf[AnyKind] should probably be a no-op, no?

-- Error: ../neg/anykind2.scala:19:17 ------------------------------------------ 19 | 1.asInstanceOf[AnyKind] // error | ^^^^^^^ | missing type parameter(s) for AnyKind

jvican · 2018-03-12T21:13:33Z

docs/docs/reference/kind-polymorphism.md

+Kind polymorphism relies on the special type `scala.AnyKind` that can be used as an upper bound of a type.
+
+```scala
+def f[T <: AnyKind] = ...


So this seems to be true top parametric type that you proposed some time ago in Scala Contributors? 😄

Yes, it's even topper than top since it's also above type constructors 😄

adriaanm · 2018-03-12T21:20:49Z

Maybe add a few words on how this relates to Any/Nothing's implicit any-kindedness? At least in scalac, they are used whenever type inference hits its limits, regardless of the actual kind of the inferred type param. We can't use AnyKind instead of Any here, since it generally wouldn't meet the bounds.

milessabin · 2018-03-13T08:53:14Z

This is great news! Happy to iterate on it here and on scala/scala#5538.

odersky · 2018-03-13T09:11:23Z

@adriaanm I don't think Any can be used as a kind-polymorphic super. Here's what I tried:

scala> def f[X] = ()
f: [X]=> Unit

scala> f[Int]

scala> f[List]
<console>:14: error: type List takes type parameters
      f[List]
        ^

scala> def f[X[_]] = ()
f: [X[_]]=> Unit

scala> f[Int]
<console>:14: error: Int takes no type parameters, expected: one
      f[Int]
        ^

scala> f[Any]
// OK!

So, curiously, an Any type argument seems to be compatible with types of any variance, but it's not the other way round - an Any bounded type variable only accepts *-types.

In dotty, Any is only a supertype of *-types. That's a difference wrt scalc.

mandubian · 2018-03-13T09:42:26Z

hi guys, happy to see this old draft PR reviving in dotty after I had left it in a draft state as nobody was giving me any return on it!
I had left it in a state where my 2 main issues were:

between 2 compiling units, I couldn't reuse AnyKind information as I was erasing a bit harshly (as far as I can remember)
to be able to write truly kind-polymorphic useful code, I would have really really liked to be able to identify a Kind & say "Type T and type U have same kind". Something like:

def f[T <: AnyKind[K], U <: AnyKind[K]] = ???

I don't know what would be K in this case but being able to "manipulate" the Kind of a type is the graal and maybe a step further than our original idea about minimalistic KP with @milessabin

milessabin · 2018-03-13T09:48:19Z

I also came to the conclusion that to be useful and not cumbersome we needed a little more than the bare bones in the PoC.

The idea I'd like to experiment with is something along the lines of a KindOf[T] yielding a kind which can then be used as a bound. When I tweeted my New Year's "kind-polymorphism or bust" resolution Conor McBride responded: "The best way to achieve kind polymorphism in a language with type polymorphism is to abolish the distinction between types and kinds." "Haskell faced/faces the same problem. Going the long way round in small bursts has significant advantages. Any taxi driver will tell you.". I think this is good advice. Embedding kinds in the space of types fits quite nicely with a kind being a bound on a type variable.

TomasMikula · 2018-03-13T12:48:37Z

I am very interested in kind polymorphism, but I see no mention of kind variables and "kind constructors" (Kind = * | Kind -> Kind) in this proposal. As a result, I don't see much use for the present limited form of kind polymorphism.

For example, how would I express that two type constructors are of the same kind?

// How to express that F and G are of the same kind?
trait Foo[F <: AnyKind, G <: AnyKind]

Or that one type constructor has the suitable kind to be passed as argument to another type constructor?

// How to express that F[G] is well-kinded?
trait Bar[F <: AnyKind, G <: AnyKind]

mandubian · 2018-03-13T13:45:13Z

@TomasMikula Yes, I agree. I've rapidly encountered cases in which one wants to write:
def foo[F[_ <: AnyKind[K]], G <: AnyKind[K]]

odersky · 2018-03-13T15:11:06Z

How about delegating kind comparisons to implicits? I.e. define

trait SameKind[A <: AnyKind, B <: AnyKind]

implicit def same0[A, B]: SameKind[A, B] = new {}
implicit def same1[A[_], B[_]]: SameKind[A, B] = new {}
implicit def same2[A[_, _], B[_, _]]: SameKind[A, B] = new {}
...

Then one could write

def foo[F[X <: AnyKind], G <: AnyKind](implicit ev: SameKind[X, G])

Could that work?

odersky · 2018-03-13T15:12:52Z

@TomasMikula I believe kind variables and kind constructors are way out of our complexity budget here.

milessabin · 2018-03-13T15:15:23Z

@odersky I think that using implicits is the right way to go for the most part, but I think we need one or two more primitives, otherwise we end up with unacceptable amounts of boilerplate which would be better handled as a language primitive.

@mandubian and I pushed about as far as is possible with something equivalent to this PR combined with implicits of the sort you're suggesting and it wasn't quite enough.

odersky · 2018-03-13T15:23:57Z

@milessabin I'll be interested to see what you come up with!

TomasMikula · 2018-03-13T15:29:14Z

How about delegating kind comparisons to implicits? I.e. define

trait SameKind[A <: AnyKind, B <: AnyKind]

implicit def same0[A, B]: SameKind[A, B] = new {}
implicit def same1[A[_], B[_]]: SameKind[A, B] = new {}
implicit def same2[A[_, _], B[_, _]]: SameKind[A, B] = new {}
...

I guess this would work, but is somewhat unsatisfactory 😕

def foo[F[X <: AnyKind], G <: AnyKind](implicit ev: SameKind[X, G])

Could that work?

Not sure about this. Doesn't X in F[X <: AnyKind] go out of scope after that ]?

I believe kind variables and kind constructors are way out of our complexity budget here.

For now or for ever? If just for now, then I would rather wait. 😊

odersky · 2018-03-13T15:38:49Z

Not sure about this. Doesn't X in F[X <: AnyKind] go out of scope after that ]?

Indeed it does. Back to the drawing board, I guess.
[UPDATE] I guess we can still do it if we have implicits that reason about arguments. Something like:

trait SameArgKind[F <: AnyKind, B <: AnyKind]

implicit def sameArg0[F[X], B]: SameArgKind[F, B] = new {}
implicit def sameArg1[F[X[_], B[_]]: SameArgKind[F, B] = new {}
implicit def sameArg2[F[X[_, _]], B[_, _]]: SameArgKind[F, B] = new {}
...
def foo[F[X <: AnyKind], G <: AnyKind](implicit ev: SameArgKind[F, G])

But I agree it gets tedious rather quickly.

For now or for ever? If just for now, then I would rather wait. 😊

Well, the future is hard to predict... But I would say, for the foreseeable future it's out of budget.

mandubian · 2018-03-13T15:58:18Z

If you want some crazier cases, I've refound these LoC proposed to me by Alexander Konovalov when he tried Kind-Poly and that couldn't work with current kind-poly.

The idea was to write kind-polymorphic Leibniz which would be extremely powerful for people writing libraries about abstract structures without rewriting 10 times the same code.

What was clearly missing was the possibility to manipulate a kind-polymorphic type constructors:

* -> (T <: AnyKind) or F[_ <: AnyKind]

and write funny things like:

def lift[F[_ <: AnyKind, _ <: AnyKind], A <: AnyKind, B <: AnyKind]
    (ab: A === B): ({ type l[α <: AnyKind] = F[A, α] })#l === ({ type l[α <: AnyKind] = F[B, α] })#l

The full quite hairy code 👍

import scala.language.higherKinds

object Test extends App {

  type F[A <: AnyKind] = Nothing
  type X = F[({type L[α <: AnyKind] = Unit})#L]

  sealed abstract class ===[A <: AnyKind, B <: AnyKind] {
    def subst[F[_<: AnyKind]](fa: F[A]): F[B]
  }
  /**
    * Given `A === B` we can prove that `F[A, ?] === F[B, ?]`.
    *
    * @see [[lift2]]
    * @see [[lift3]]
    */
  def lift[F[_ <: AnyKind, _ <: AnyKind], A <: AnyKind, B <: AnyKind]
    (ab: A === B): ({ type l[α <: AnyKind] = F[A, α] })#l === ({ type l[α <: AnyKind] = F[B, α] })#l = {
  // fails on the line above with:
  // type Λ$ takes type parameters
    type f[β <: AnyKind] = ({ type l[α <: AnyKind] = F[A, α] })#l === ({ type l[α <: AnyKind] = F[B, α] })#l
    ab.subst[f](refl[({ type l[α <: AnyKind] = F[A, α] })#l])
  }

  final case class Refl[A <: AnyKind]() extends ===[A, A] {
    def subst[F[_ <: AnyKind]](fa: F[A]): F[A] = fa
  }
  val anyRefl = Refl[AnyKind]()
  def unsafeForce[A <: AnyKind, B <: AnyKind]: A === B = anyRefl.asInstanceOf[A === B]
  def refl[A <: AnyKind]: A === A = unsafeForce[A, A]


  refl[List]

  trait Foo[F[_], A]
  val l: ({ type l[t] = Foo[List, t] })#l === ({ type l[t] = Foo[List, t] })#l = lift[Foo, List, List](refl[List])

  trait Bar[F[_], G[_]]
  val l2: ({ type l[t[_]] = Bar[List, t] })#l === ({ type l[t[_]] = Bar[List, t] })#l = lift[Bar, List, List](refl[List])


  type Ξ = scala.AnyKind

  trait Forall[F[_ <: Ξ]] {
    def apply[A <: Ξ]: F[A]
  }

  trait Exists[F[_ <: Ξ]] { fa =>
    type A <: Ξ
    def apply: F[A]
  }

  type ∀[F[_ <: Ξ]] = Forall[F]
  type ∃[F[_ <: Ξ]] = Exists[F]
  type ~>[A[_ <: Ξ], B[_ <: Ξ]] = FunctionK[A, B]
  type =~=[A[_ <: Ξ], B[_ <: Ξ]] = ===[A, B]

  abstract class FunctionK[F[_ <: Ξ], G[_ <: Ξ]] {
    def apply[A <: Ξ](fa: F[A]): G[A]
  }
  object FunctionK {
    def id[F[_ <: Ξ]]: FunctionK[F, F] = new FunctionK[F, F] {
      override def apply[A <: Ξ](fa: F[A]): F[A] = fa
    }
    def const[K](k: K): ∀[ ({ type λ[α[_ <: Ξ]] = α ~> ({ type λ[β <: Ξ] = K })#λ })#λ] = new ∀[({ type λ[α[_ <: Ξ]] = α ~> ({ type λ[β <: Ξ] = K })#λ })#λ] {
      override def apply[A[_ <: Ξ]]: A ~> ({ type λ[β <: Ξ] = K })#λ = new (A ~> ({ type λ[β <: Ξ] = K })#λ) {
        override def apply[B <: Ξ](fa: A[B]): K = k
      }
    }

    val t: List ~> ({ type λ[β <: Ξ] = Unit })#λ = const(()).apply[List]
  }

  // trait Foo2[F[_]]
  // new FunctionK[Foo2, List]{
  //   def apply[A[_]](fa: Foo2[A]): List[A] = ???
  // }

  // trait Category[->[_ <: Ξ, _ <: Ξ]] {
  //   def id[A <: Ξ]: A -> A
  // }
  // implicit val catzBaseFunctionKCategory: Category[FunctionK] = new Category[~>] {
  //   override def id[A <: Ξ]: A ~> A = FunctionK.id[A] // Impossible to define?
  // }

  sealed abstract class Liskov[-A <: Ξ, +B <: Ξ] { ab =>
    def subst[F[-_ <: Ξ]](fb: F[B]): F[A]
  }

  type <~<[A<:Ξ, B<:Ξ] = Liskov[A, B]

  private final case class Refl2[A <: Ξ]() extends Liskov[A, A] {
    def subst[F[-_ <: Ξ]](fa: F[A]): F[A] = fa
  }
  def id[A <: Ξ]: A <~< A = Refl2[A]()
  implicit def reify[A <: Ξ, B >: A <: Ξ]: A <~< B = id
  // all of these work:
  reify[Int, Any]
  reify[Int, AnyVal]
  reify[List, Any]

  reify[List, Int]
  reify[Right, Either]
}

odersky · 2018-03-13T16:25:22Z

@mandubian that looks rather ... scary

mandubian · 2018-03-13T17:37:31Z

@odersky yes it is scary XD, alex was testing advanced ideas... But, it's showing the superior limit where we can certainly not go so IMHO it's interesting...

I wrote wrong things above: F[_ <: AnyKind] is not * -> T <: AnyKind but more (* <: AnyKind) -> *.

Ideally, I'd like to write such things in pseudo-scala-code:

trait Kinded[F <: AnyKind] {
   type WellFormed[_ <: AnyKind]
}

Kinded[Int] { type WellFormed = Int }
Kinded[List] { type WellFormed[A] = List[A] }
Kinded[Map] { type WellFormed[A, B] = Map[A, B] }
Kinded[Monad] { type K[F[_]] = Monad[F] }

trait SameKind[F <: AnyKind, G <: AnyKind]

abstract class FunctionK[F <: AnyKind, G <: AnyKind](implicit sk: SameKind[F, G]) {
  def apply[A <: AnyKind](fa: Kinded[F].WellFormed[A]): Kinded[G].WellFormed[A]
}

milessabin · 2018-03-13T18:29:19Z

@odersky even as things stand there are immediate applications to things like ClassTag, TypeTag, shapeless's Typeable and the like.

odersky · 2018-03-13T19:06:29Z

Test failed with:

failed Vulpix meta: the output of sbt differs from the expected output
expected : [info] Test dotty.tools.vulpix.VulpixMetaTests.compilePos started
actual   : Testing tests/vulpix-tests/meta/pos/does-not-compile.scala

Who can help debug/fix this?

smarter · 2018-03-13T19:09:12Z

Who can help debug/fix this?

The meta-tests were added by @OlivierBlanvillain

odersky · 2018-03-13T19:48:16Z

Seemed to have been a transient failure. After restart it passed. Let's watch it and disable if it occurs more often.

odersky · 2018-03-13T19:59:01Z

I think this is ready to be reviewed. I would argue it is an addition with lots of upsides. With AnyKind we get the missing top-type over all kinds, which is the analogue of Nothing. So the result is more symmetric than before, and the added use cases are interesting. This does not preclude further refinements in later PRs, but for these we need more time to work them out and study them.

There's still a gap in the docs where we wanted to show a simple example. @milessabin, @mandubian do you have something that could illustrate working with AnyKind in a shortish, non-synthetic example? (say 10-20 lines).

odersky · 2018-03-13T22:05:00Z

test performance please

dottybot · 2018-03-13T22:05:53Z

performance test scheduled: 1 job(s) in queue, 0 running.

dottybot · 2018-03-13T23:48:12Z

Performance test finished successfully:

Visit http://dotty-bench.epfl.ch/4108/ to see the changes.

Benchmarks is based on merging with master (a27bc12)

Blaisorblade · 2018-03-23T15:02:22Z

docs/docs/reference/kind-polymorphism.md

+Nevertheless, this is enough to achieve some interesting generalizations that work across kinds, typicially
+through advanced uses of implicits.
+
+(todo: insert good concise example)


Afraid this should still be done. And we should update the docs to mark this as experimental.

Blaisorblade · 2018-03-23T15:11:34Z

I'd prefer to see the flag only cover the impredicative version rather both that and the predicative version. If we're agreed that the the restriction is safe then it'd be good to be able to move it forward in Scala.

Makes sense to me, but somebody would have to implement the restriction (and I don't have the needed skills yet). In fact one should spec the semantics — if you need to allow subtyping between AnyKind-polymorphic types, you end up with a separate subtyping lattice... I can try to think about the second part.

The best-known example of predicative polymorphism is type polymorphism in ML/Haskell98, where type arguments of polymorphic functions cannot be polymorphic types but must be monomorphic types.

if we decided that any type with an AnyKind-bounded type variable (or member) is not <: AnyKind would mean F[_ <: AnyKind] <: AnyKind can't be written, right?

Correct.

is impredicative case something like [...]

The example is simpler: consider trait F[X <: AnyKind]; trait G[X <: AnyKind]. Right now F <: AnyKind and G <: AnyKind, and that would be forbidden by predicative kind-polymorphism.
So, right now you can construct F[F] and also G[F], and those applications would be forbidden as well.

(EDIT) But if F <: AnyKind but F is a type variable, it can't be applied to anything, so F[F] is forbidden. (Had to remind myself of that).

in current implementation, would imprecative case be possible or not?

It'd be possible: This PR implements (under -Ykind-polymorphism) impredicative kind-polymorphism.

Allow a form of type polymorphism by adding an AnyKind upper bound. Types of any kind are subtypes of `AnyKind`. The "any-kinded types" are `AnyKind` itself, and all type parameters and abstract types having it as an upper bound. Any-kinded types cannot be used as types of values, nor can they be applied to type parameters. About the only thing one can do with them is use them as parameters for implicit searches.

These show that the technique used in mandubian/any-order-ubiklist.scala does not work here, since intersections are only allowed over *-types and AnyKind is not a *-type.

So we could not delete the two lines that never returned a result. It turns out they were necessary for their effect on the constraint. If they are removed, i3422.scala fails.

When compiling kind-incorrect code in neg/anykind3.scala, substParams fails with an index-out-bounds exception. It is called from tryReduce via instantiate. We know there are several scenarios where this can happen - Sandro has detected a couple of others. This commit avoids the problem by aborting the reduce if there is an index out of bounds.

When doing the changes to higher-kinded types, an error popped up in pos/i3976.scala that a wildcard argument `_` was illegal because the corresponding type parameter is higher-kinded. This seemed to have been masked by an incorrect subtype check before. We now use the parameter bounds as the argument in this case.

Several fixes to make sure that Any is a supertype only of * types. Before there were some types that slipped through the net. Also, new tests.

We keep the test as a neg test anyway. The old and new error messages are both uninteresting.

smarter · 2018-03-23T19:35:16Z

Merging this now because this PR contains useful subtyping fixes, but feel free to continue discussing here.

Add the rule T <: Any for any *-Type T. This was not include fully before. We did have the rule that T <: Any, if Any is in the base types of T. However, it could be that the base type wrt Any does not exist. Example: Any#L <: Any yielded false before, now yields true. This error manifested itself in i4031.scala. With the new rule, we can drop again the special case in derivedSelect. TODO: in the context of scala#4108, this seems questionable. Also, `Any#L` seems an invalid type (even tho it is sound to consider it empty), and we'd probably not want to accept it if the user writes it; here it is only OK because it's introduced by avoidance. Or are user-written types checked elsewhere?

julienrf reviewed Mar 12, 2018

View reviewed changes

jvican reviewed Mar 12, 2018

View reviewed changes

SethTisue mentioned this pull request Mar 13, 2018

Providing minimalistic & controlled kind-polymorphism [ci: last-only] scala/scala#5538

Closed

odersky changed the title ~~Add kind polymorphism [WIP]~~ Add kind polymorphism Mar 13, 2018

Blaisorblade reviewed Mar 23, 2018

View reviewed changes

odersky and others added 15 commits March 23, 2018 17:15

Add docs

c825eb5

More negative tests

321b616

These show that the technique used in mandubian/any-order-ubiklist.scala does not work here, since intersections are only allowed over *-types and AnyKind is not a *-type.

Fix regression in TypeComparer

1bb183a

So we could not delete the two lines that never returned a result. It turns out they were necessary for their effect on the constraint. If they are removed, i3422.scala fails.

Update comparisons of higher-kinded types

060e1de

Several fixes to make sure that Any is a supertype only of * types. Before there were some types that slipped through the net. Also, new tests.

Remove failing repl test

462a401

We keep the test as a neg test anyway. The old and new error messages are both uninteresting.

Rename isHK -> isLambdaSub

5bc9927

Add hook to make AnyKind support conditional

0031ca9

Fix accidental replacement

99e0dc6

Hide kind-polymorphism behind -Ykind-polymorphism

92a941a

Fix flag description

ee44f8f

Disable tracing again

05162fe

Fix typos in new docs

e51db1c

allanrenucci force-pushed the add-kind-poly branch from 14253af to e51db1c Compare March 23, 2018 16:16

Fix scala#4167: Add regression test

91e7fc4

Blaisorblade mentioned this pull request Mar 23, 2018

Incomplete error message for higher-kinded bounds violations #4164

Closed

smarter merged commit a0e1000 into scala:master Mar 23, 2018

allanrenucci deleted the add-kind-poly branch March 23, 2018 22:16

karolchmist mentioned this pull request Jun 7, 2018

dotty: 0.6.0-RC1 -> 0.8.0-RC1 NixOS/nixpkgs#41626

Merged

8 tasks

smarter mentioned this pull request Jun 17, 2018

[Proof of concept] Polymorphic function types #4672

Merged


		(todo: insert good concise example)

		Some technical details: `AnyKind` is a synthesized class just like `Any`, but without any members. It extends no other class.

Add kind polymorphism #4108

Add kind polymorphism #4108

Conversation

odersky commented Mar 12, 2018

julienrf commented Mar 12, 2018 • edited Loading

odersky commented Mar 12, 2018

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

Choose a reason for hiding this comment

Choose a reason for hiding this comment

Choose a reason for hiding this comment

adriaanm commented Mar 12, 2018

milessabin commented Mar 13, 2018

odersky commented Mar 13, 2018 • edited Loading

mandubian commented Mar 13, 2018

milessabin commented Mar 13, 2018

TomasMikula commented Mar 13, 2018

mandubian commented Mar 13, 2018

odersky commented Mar 13, 2018 • edited Loading

odersky commented Mar 13, 2018

milessabin commented Mar 13, 2018

odersky commented Mar 13, 2018

TomasMikula commented Mar 13, 2018

odersky commented Mar 13, 2018 • edited Loading

mandubian commented Mar 13, 2018 • edited Loading

odersky commented Mar 13, 2018

mandubian commented Mar 13, 2018

milessabin commented Mar 13, 2018

odersky commented Mar 13, 2018

smarter commented Mar 13, 2018

odersky commented Mar 13, 2018

odersky commented Mar 13, 2018 • edited Loading

odersky commented Mar 13, 2018

dottybot commented Mar 13, 2018

dottybot commented Mar 13, 2018

Choose a reason for hiding this comment

Blaisorblade commented Mar 23, 2018 • edited Loading

smarter commented Mar 23, 2018

julienrf commented Mar 12, 2018 •

edited

Loading

odersky commented Mar 13, 2018 •

edited

Loading

odersky commented Mar 13, 2018 •

edited

Loading

odersky commented Mar 13, 2018 •

edited

Loading

mandubian commented Mar 13, 2018 •

edited

Loading

odersky commented Mar 13, 2018 •

edited

Loading

Blaisorblade commented Mar 23, 2018 •

edited

Loading