Direct representation of higher-kinded types #1343

odersky · 2016-06-29T18:51:24Z

Rebased version of #1337 with commits squashed so that there are less than 100 commits in the PR.

This is (hopefully the last) attempt to model higher-kinded types in dotty. This time it's done directly, having specific types for type lambdas and higher-kinded applications.

This PR is based on #1282 but undoes most of it. Nevertheless I thought it would be good to have a trace of the history how we arrived here.

odersky · 2016-06-30T21:07:58Z

There are two areas that should be investigated further:

[] should we bring back named type parameters?
[] can we represent existential types as hk types applied to type bounds?

But the commit as is is ready for review.

DarkDimius · 2016-07-05T15:44:27Z

src/dotty/tools/dotc/core/SymDenotations.scala

@@ -1641,6 +1641,7 @@ object SymDenotations {
       */
      def isCachable(tp: Type): Boolean = tp match {
        case _: TypeErasure.ErasedValueType => false
+        case tp: TypeRef if tp.symbol.isClass => true


down to 22secs from 60secs with this change.
Now, need to do something with compareAliasedRefined to get back to 2.5secs.

odersky · 2016-07-06T13:03:57Z

There are some loose ends with support for "existential types", which can be encoded using a combination of hk applications and wildcards. E.g.

T { forSome type A <: U }

can be encoded as

 ([A] -> T)[_ <: U]

Subtyping and some other basic functionality works over these types, but other things crash the
compiler or lead to unintuitive results. That's no surprise as we do not really know what the right
rules for these types are. Bring existential types back? Would that not get us back into the same
intractable problems we have with scalac? On the other hand, if we want to forbid such types, the
question is how to do this in a clean way that's not too restrictive. The cleanest way would be
to not allow wildcards in hk type applications, period. But that would invalidate some patterns the
collections library, where we write definitions such as

type Coll = CC[_]

with CC a higher-kinded abstract type or type param.

DarkDimius · 2016-07-07T13:38:39Z

Was playing with how much does removing compareAliasedRefined affect linker.
Replacing it by false reduces analysis time from 12 seconds down to 2.5. Yheartbeat is also able to discover this: number of member selections goes from 33'045'060 down to 955'174

odersky · 2016-07-07T21:33:08Z

The PR is completed now as far as I am concerned. I mean to come back to named parameters, which would also affect compareAliasedDefined. But I think this is better done in a separate PR. For the moment the status of named type parameters is "in limbo".

smarter · 2016-07-11T05:16:58Z

src/dotty/tools/dotc/core/Constraint.scala

-   *                      or -1 if no such parameter exists.
+  /** Is entry associated with `pt` removable? This is the case if
+   *  all type parameters of the entry are associated with type variables
+   *  which have its `inst` fields set.


their inst fields

Use (cached) superType where possible.

Beta-reduce only if `Config.simplifyApplications` is true. Turning off beta-reduction revealed two problems which are also fixed in this commit: 1. Bad treatement of higher-kinded argyments in cyclicity checking 2. Wrong variance for higher-kinded arguments in TypeAccumulator

odersky · 2016-07-13T16:22:21Z

As far as I can see we should now have feature parity with Scala 2.x with SI-2712.

smarter · 2016-07-13T19:35:38Z

src/dotty/tools/dotc/core/Types.scala

-            else if (tparam.paramVariance == 0) variance = 0
+            val pvariance = tparam.paramVariance
+            if (pvariance < 0) variance = -variance
+            else if (pvariance == 0) variance = 0


variance *= tparam.paramVariance instead of the if/else ? (Same in the case below)

Great minds think alike :-) See next commit.

odersky · 2016-07-14T07:32:22Z

We decided to wait with several other PRs until this is in, so I want to merge by the end of the day, unless something important comes up.

smarter · 2016-07-14T09:31:44Z

src/dotty/tools/dotc/core/Types.scala

+    lazy val typeParams: List[LambdaParam] =
+      paramNames.indices.toList.map(new LambdaParam(this, _))
+
+    def derivedTypeLambda(paramNames: List[TypeName] = paramNames, paramBounds: List[TypeBounds] = paramBounds, resType: Type)(implicit ctx: Context): Type =


Every other derivedFoo method returns a Foo, but this one may return a TypeAlias or a TypeBounds instead of a TypeLambda, why is that? Could a different name be chosen to avoid confusion?

smarter · 2016-07-14T10:22:08Z

More bound checks are needed, this shouldn't compile:

class Foo[A]
class Bar[B]

object Test {
  type Alias[F[X] <: Foo[X]] = F[Int]
  val x: Alias[Bar] = new Bar[Int] // Bar[X] is not a subtype of Foo[X]
}

smarter · 2016-07-14T10:54:43Z

src/dotty/tools/dotc/core/Types.scala

@@ -850,6 +879,12 @@ object Types {
      case _ => this
    }

+    /** If this is a TypeAlias type, its alias, otherwise this type itself */
+    final def followTypeAlias(implicit ctx: Context): Type = this match {


This method is never called

smarter · 2016-07-14T11:52:20Z

Also tests/pos-scala2/t2994.scala fails to compile in scalac but compiles in dotty:

tests/pos-scala2/t2994.scala:23: error: type s takes type parameters
    trait curry[n[_, _], s[_]] { type f[z <: NAT] = n[s, z] }
                                                      ^

I think we should follow scalac here and enforce kind-correctness, for reference, the change to curry happened in 7f72143 in dotty

Previous logic could only handle classes as constructors. Also, address other reviewers comments.

smarter · 2016-07-15T05:20:29Z

Better, but I can still break it :)

class Foo[A]
class Bar[B]

object Test {
  type Alias[F[X] <: Foo[X]] = F[Int]

  def foo[M[_[_]], A[_]]: M[A] = null.asInstanceOf[M[A]]

  val x = foo[Alias, Bar]
}

scalac checks the bounds in the type of x and sees the issue:

error: type arguments [Bar] do not conform to type Alias's type parameter bounds [F[X] <: Foo[X]]
  val x = foo[Alias, Bar]
      ^

smarter · 2016-07-15T05:23:40Z

Interestingly, scalac will happily compile this code if I replace val x = foo[Alias, Bar] by just foo[Alias, Bar], not sure if this can be exploited to crash at runtime but it's still a bug.

Enable checking of bounds when comparing type lambdas. This invalidates a pattern used in t2994 and potentially other code, where a bound [X] -> Any is used as a template that is a legal supertype of all other bounds. The old behavior is still available under language:Scala2.

odersky · 2016-07-15T08:41:26Z

@smarter Bounds check is tigthened now "at the source", in a different way from how it's done in Scala-2. The alternative would have been to open a loophole by not comparing bounds of type lambdas and then fixing it by checking all * types for bound correctness. But as you noted that would have to include all types computed by typer, not just types written by the programmer. I am scared this would be too expensive and that error messages would suffer.

scalac seems to check inferred types of declared values and methods, but not other types. I agree this is not enough.

smarter · 2016-07-15T09:03:42Z

Yes, I was skeptical about that loophole too, would be interesting to figure out how much code relies on it. A proper migration warning seems tricky indeed, but maybe we could have a flag in the constraint set var unsoundLambdaSubtyping = false that we set to true if the check ever fails, if a the end of a compilation run the flag is set, then issue a warning

odersky · 2016-07-15T11:11:33Z

Going to merge now to let other PRs proceed. Many thanks to @smarter for the thorough review!

DarkDimius · 2016-07-15T11:14:48Z

Hooray! 🌟 🎆 🎆 🎆 ⭐

odersky · 2016-07-15T11:18:35Z

On Fri, Jul 15, 2016 at 11:03 AM, Guillaume Martres <
notifications@github.com> wrote:

Yes, I was skeptical about that loophole too, would be interesting to
figure out how much code relies on it. A proper migration warning seems
tricky indeed, but maybe we could have a flag in the constraint set var
unsoundLambdaSubtyping = false that we set to true if the check ever
fails, if a the end of a compilation run the flag is set, then issue a
warning

That sounds like a good strategy. I am reading this only now after having
merged the PR. So we would need a separate PR for this.

—
You are receiving this because you modified the open/close state.
Reply to this email directly, view it on GitHub
#1343 (comment), or mute
the thread
https://github.com/notifications/unsubscribe-auth/AAwlVtRpAaFiEaNlPl2ws4tcoNVlfpAJks5qV0zxgaJpZM4JBcu4
.

Prof. Martin Odersky
LAMP/IC, EPFL

felixmulder added the In progress label Jun 29, 2016

This was referenced Jun 29, 2016

[WIP] Direct representation of higher-kinded types #1337

Closed

[WIP] Change HK encoding #1282

Closed

odersky added Needs review and removed In progress labels Jun 30, 2016

DarkDimius mentioned this pull request Jul 1, 2016

[Deprecated] exhaustivity & redundancy check for pattern matching #1261

Closed

16 tasks

DarkDimius reviewed Jul 5, 2016
View reviewed changes

odersky force-pushed the change-hk-direct2 branch from 82c0026 to f93a975 Compare July 7, 2016 16:37

odersky closed this Jul 7, 2016

odersky reopened this Jul 7, 2016

felixmulder added In progress and removed Needs review labels Jul 7, 2016

odersky added Needs review and removed In progress labels Jul 7, 2016

smarter reviewed Jul 11, 2016
View reviewed changes

odersky added 4 commits July 13, 2016 13:47

Optimize hk comparisons

1443fd4

Use (cached) superType where possible.

Simplify variance computations

0ff5354

Allow hk parameters in lower bounds

18b3080

smarter reviewed Jul 13, 2016
View reviewed changes

smarter reviewed Jul 14, 2016
View reviewed changes

Fix bounds checking of hk applied typed

82fc27f

Previous logic could only handle classes as constructors. Also, address other reviewers comments.

odersky force-pushed the change-hk-direct2 branch from a6b6c08 to 82fc27f Compare July 14, 2016 17:52

Add test case for hk bounds checking

a737b47

odersky merged commit 409c6c3 into scala:master Jul 15, 2016

odersky removed the Needs review label Jul 15, 2016

odersky deleted the change-hk-direct2 branch July 15, 2016 11:12

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Direct representation of higher-kinded types #1343

Direct representation of higher-kinded types #1343

odersky commented Jun 29, 2016

odersky commented Jun 30, 2016

DarkDimius Jul 5, 2016

odersky commented Jul 6, 2016

DarkDimius commented Jul 7, 2016

odersky commented Jul 7, 2016

smarter Jul 11, 2016

odersky commented Jul 13, 2016

smarter Jul 13, 2016

odersky Jul 13, 2016

odersky commented Jul 14, 2016

smarter Jul 14, 2016 •

edited

Loading

smarter commented Jul 14, 2016

smarter Jul 14, 2016

smarter commented Jul 14, 2016

smarter commented Jul 15, 2016

smarter commented Jul 15, 2016

odersky commented Jul 15, 2016 •

edited

Loading

smarter commented Jul 15, 2016

odersky commented Jul 15, 2016

DarkDimius commented Jul 15, 2016

odersky commented Jul 15, 2016

Direct representation of higher-kinded types #1343

Direct representation of higher-kinded types #1343

Conversation

odersky commented Jun 29, 2016

odersky commented Jun 30, 2016

DarkDimius Jul 5, 2016

Choose a reason for hiding this comment

odersky commented Jul 6, 2016

DarkDimius commented Jul 7, 2016

odersky commented Jul 7, 2016

smarter Jul 11, 2016

Choose a reason for hiding this comment

odersky commented Jul 13, 2016

smarter Jul 13, 2016

Choose a reason for hiding this comment

odersky Jul 13, 2016

Choose a reason for hiding this comment

odersky commented Jul 14, 2016

smarter Jul 14, 2016 • edited Loading

Choose a reason for hiding this comment

smarter commented Jul 14, 2016

smarter Jul 14, 2016

Choose a reason for hiding this comment

smarter commented Jul 14, 2016

smarter commented Jul 15, 2016

smarter commented Jul 15, 2016

odersky commented Jul 15, 2016 • edited Loading

smarter commented Jul 15, 2016

odersky commented Jul 15, 2016

DarkDimius commented Jul 15, 2016

odersky commented Jul 15, 2016

smarter Jul 14, 2016 •

edited

Loading

odersky commented Jul 15, 2016 •

edited

Loading