-
Notifications
You must be signed in to change notification settings - Fork 1.1k
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
Add kind polymorphism #4108
Add kind polymorphism #4108
Conversation
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 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? |
See also: scala/scala#5538 |
|
||
(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. |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So, no equals
nor hashCode
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Since there's no way to create instances of AnyKind
, I suppose it doesn't matter.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
what is expected of .asInstanceOf[AnyKind]
?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
As "just as regular user" a ClassCastException seems perfectly reasonable.
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
AsInstanceOf[AnyKind] should probably be a no-op, no?
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
-- Error: ../neg/anykind2.scala:19:17 ------------------------------------------
19 | 1.asInstanceOf[AnyKind] // error
| ^^^^^^^
| missing type parameter(s) for AnyKind
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] = ... |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
So this seems to be true top parametric type that you proposed some time ago in Scala Contributors? 😄
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Yes, it's even topper than top since it's also above type constructors 😄
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. |
This is great news! Happy to iterate on it here and on scala/scala#5538. |
@adriaanm I don't think
So, curiously, an In dotty, |
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 don't know what would be |
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 |
I am very interested in kind polymorphism, but I see no mention of kind variables and "kind constructors" ( 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] |
@TomasMikula Yes, I agree. I've rapidly encountered cases in which one wants to write: |
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? |
@TomasMikula I believe kind variables and kind constructors are way out of our complexity budget here. |
@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. |
@milessabin I'll be interested to see what you come up with! |
I guess this would work, but is somewhat unsatisfactory 😕
Not sure about this. Doesn't
For now or for ever? If just for now, then I would rather wait. 😊 |
Indeed it does. Back to the drawing board, I guess. 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.
Well, the future is hard to predict... But I would say, for the foreseeable future it's out of budget. |
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:
and write funny things like:
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]
}
|
@mandubian that looks rather ... scary |
@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: 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]
} |
@odersky even as things stand there are immediate applications to things like |
Test failed with:
Who can help debug/fix this? |
The meta-tests were added by @OlivierBlanvillain |
Seemed to have been a transient failure. After restart it passed. Let's watch it and disable if it occurs more often. |
I think this is ready to be reviewed. I would argue it is an addition with lots of upsides. With 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 |
test performance please |
performance test scheduled: 1 job(s) in queue, 0 running. |
Performance test finished successfully: Visit http://dotty-bench.epfl.ch/4108/ to see the changes. Benchmarks is based on merging with master (a27bc12) |
Nevertheless, this is enough to achieve some interesting generalizations that work across kinds, typicially | ||
through advanced uses of implicits. | ||
|
||
(todo: insert good concise example) |
There was a problem hiding this comment.
Choose a reason for hiding this comment
The reason will be displayed to describe this comment to others. Learn more.
Afraid this should still be done. And we should update the docs to mark this as experimental.
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 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.
Correct.
The example is simpler: consider (EDIT) But if
It'd be possible: This PR implements (under |
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.
14253af
to
e51db1c
Compare
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?
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?
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?
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?
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?
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