[WIP] Change HK encoding #1282

odersky · 2016-05-27T09:45:02Z

We would like to encode HK types directly into refined types, without type projections. This PR should eventually lead to this goal. Status:

Disentangle recursion and refinement through the introduction of RecType.
Drop the notion that type parameters are always symbols
Introduce new encoding
Drop superfluous code
Decide whether we should drop named type parameters

DarkDimius · 2016-05-27T10:35:11Z

src/dotty/tools/dotc/core/tasty/TastyFormat.scala

@@ -129,7 +129,7 @@ Standard-Section: "ASTs" TopLevelStat*
                  SUPERtype      Length this_Type underlying_Type
                  REFINEDtype    Length underlying_Type refinement_NameRef info_Type
                  APPLIEDtype    Length tycon_Type arg_Type*
-                  TYPEBOUNDS     Length low_Type high_Type
+                  TYPEBOUNDS     Length low_Type high_Type bindingKind_Nat?


why not bindingKind_BYTE?

odersky · 2016-05-27T13:20:44Z

Rebased to master

smarter · 2016-05-28T20:37:08Z

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


  /** A refined type parent { refinement }
   *  @param refinedName  The name of the refinement declaration
   *  @param infoFn: A function that produces the info of the refinement declaration,
   *                 given the refined type itself.
   */
-  abstract case class RefinedType(parent: Type, refinedName: Name)
-    extends CachedProxyType with BindingType with ValueType {
+  abstract case class RefinedType(private var myParent: Type, refinedName: Name, private var myRefinedInfo: Type)


The documentation of the params above needs to be updated

smarter · 2016-05-30T16:06:14Z

Note: the introduction of RecType will require some changes to the sbt ExtractAPI phase but nothing too complicated, I'll have a look once this PR is complete.

smarter · 2016-05-30T16:10:49Z

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

+    def apply(argBindingFns: List[RecType => TypeBounds],
+              bodyFn: RecType => Type)(implicit ctx: Context): Type = {
+      assert(Config.newHK)
+      val argNames = argBindingFns.indices.toList.map(tpnme.hkArg)


This val is unused

smarter · 2016-05-30T17:23:21Z

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

+            (rt: RecType) => (b1(rt) & b2(rt))
+              .withBindingKind(
+                BindingKind.fromVariance(
+                  (tparam1.memberVariance + tparam2.memberVariance) / 2))


tparam1.memberVariance.commonVariance(tparam2.memberVariance)

Will be used to encode higher-kinded type parameters.

Previously a refinement could only apply to a type bound in the parent. This restriction needs to be dropped for the new encoding of hk type parameters.

Treat parent like refinedInfo. Introduce isBinding convenience method in TypeBounds.

They not print similar to scalac: "?x" where `x` is a unique number. Todo: An offline explanation what they are, similar to javac. I.e. ... ?3 ... where ?3: T

TypeMaps do the same, so it is logical, and helps prevent subtle errors as when we mispredicted whether a RecType contains references that point to it.

Fixes some discrepancies in Tasty typing.

Without this step, anonymous functions can have dependent types which causes the parameter references to "leak out" to types in the environment in illegal ways. This caused a tasty failure for Typer before (not sure why the failure was not observed under the old hk scheme).

This seems to be required to make Typer compile, and it is logical that we should do this. We still need to study how it fits in the general context. Also, it required neg test to be fixed. With the change, the error is now reported earlier.

Skolem types are eliminated by pickling, so they should not appear in the "before-pickling" output.

compileMixed failed because there was a cycle between immutable.Seq (compiled) and parallel.ParSeq (loaded from classfile). Inspection of the completion log (turn completions Printer on) and the stack trace showed that there's nothing we can do here. The old hk scheme did not go into the cycle because it did not force an unrelated type. I believe with enough tweaking we would also hva egotten a cycle in the old hk scheme. The test is "fixed" by adding parallel.ParSeq to the files to compile.

Those tests do not work yet with the revised hk scheme. Before trying to fix this, we should first decide what parts of named parameters should be kept.

Updates to make dotty compile after rebase

odersky · 2016-06-08T13:08:59Z

Rebased to master

[This was an unncessessary and wrong fix. The real problem was in findMember] This seems to be required to make Typer compile, and it is logical that we should do this. We still need to study how it fits in the general context. Also, it required neg test to be fixed. With the change, the error is now reported earlier. (reverted from commit a6caf1c)

Improve explanation

The theory is that if two refined types have the same refined name, then they are likely to be of related classes. So it seems more fruitful to check the argument before the typeconstructor because that way we test the part that's more likely to fail first. Rough observations seem to indicate a 3% improvement in the junit test time.

Drop some unnecessary cases; improve comments.

Try to combine type constructor and arguments under a common LazyRef.

Make it check variances.

Drop recursive definition of RefinedThis - this is now taken over by RecType. Drop RefinedThis.

The logic avoiding forcing is no longer needed.

smarter · 2016-06-24T01:36:35Z

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

@@ -264,21 +264,7 @@ class TypeApplications(val self: Type) extends AnyVal {
        self.cls.typeParams
      case self: TypeRef =>
        val tsym = self.symbol
-        if (tsym.isClass) tsym.typeParams
-        else tsym.infoOrCompleter match {
-          case completer: TypeParamsCompleter =>


So why isn't this needed anymore? Does this mean that the TypeParamsCompleter class can be deleted?

odersky · 2016-06-29T18:53:02Z

Superseded by #1343

odersky force-pushed the change-hk-refinements branch from 7c1f511 to 775eb8a Compare May 27, 2016 09:49

DarkDimius reviewed May 27, 2016
View reviewed changes

odersky force-pushed the change-hk-refinements branch from e1a4cb0 to 1aed088 Compare May 27, 2016 13:20

smarter reviewed May 28, 2016
View reviewed changes

smarter reviewed May 30, 2016
View reviewed changes

odersky force-pushed the change-hk-refinements branch from 5cd8627 to 2019307 Compare May 30, 2016 17:00

smarter reviewed May 30, 2016
View reviewed changes

felixmulder added the In progress label Jun 2, 2016

felixmulder assigned odersky Jun 2, 2016

odersky added 8 commits June 8, 2016 12:15

Record binding kind in TypeBounds

468b499

Will be used to encode higher-kinded type parameters.

Allow refinements of new types

2d8d291

Previously a refinement could only apply to a type bound in the parent. This restriction needs to be dropped for the new encoding of hk type parameters.

Allow general recursion in refined types.

10ef004

Refinements to refinement types

3c99610

Treat parent like refinedInfo. Introduce isBinding convenience method in TypeBounds.

Add type lambdas

461fe3d

Better printing of skolems

3960710

They not print similar to scalac: "?x" where `x` is a unique number. Todo: An offline explanation what they are, similar to javac. I.e. ... ?3 ... where ?3: T

New type lambda scheme for hk types

a3a6108

Add mapInfo method to Denotations

e768331

odersky added 8 commits June 8, 2016 12:19

Make TypeAccumulators follow LazyRefs

db4d934

TypeMaps do the same, so it is logical, and helps prevent subtle errors as when we mispredicted whether a RecType contains references that point to it.

Add normalizeHkApply to homogenize

3560e56

Fixes some discrepancies in Tasty typing.

Homogenize skolem types

392090a

Skolem types are eliminated by pickling, so they should not appear in the "before-pickling" output.

Disable named parameter tests

5e448ff

Those tests do not work yet with the revised hk scheme. Before trying to fix this, we should first decide what parts of named parameters should be kept.

Fix merge errors

5a20984

Updates to make dotty compile after rebase

odersky force-pushed the change-hk-refinements branch from 4b59b1e to 5a20984 Compare June 8, 2016 13:08

odersky added 13 commits June 9, 2016 13:25

Deal with nested findMember calls over the same RecType

b4f21d0

Add explanation why generizing compreHkApply is not needed.

7cc0308

Fix comments

b88cfec

Improve explanation

Add TODO comment in TreePickler

7abd0cc

Cleanups

7c99c8a

Drop some unnecessary cases; improve comments.

Smarter handling of LazyRefs in betaReduce

4c51505

Try to combine type constructor and arguments under a common LazyRef.

Optimize RecType/RecType comparisons

eb6cfb4

Fi compareHkLambda

6d6afbf

Make it check variances.

Remove old hk scheme

745a718

Simoplify RefinedType

79a7976

Drop recursive definition of RefinedThis - this is now taken over by RecType. Drop RefinedThis.

Simplify typeParams

57bf237

The logic avoiding forcing is no longer needed.

smarter reviewed Jun 24, 2016
View reviewed changes

This was referenced Jun 28, 2016

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

Closed

Direct representation of higher-kinded types #1343

Merged

odersky closed this Jun 29, 2016

felixmulder removed the In progress label Jun 29, 2016

Provide feedback

Saved searches

Use saved searches to filter your results more quickly

Uh oh!

[WIP] Change HK encoding #1282

[WIP] Change HK encoding #1282

Uh oh!

odersky commented May 27, 2016 •

edited

Loading

Uh oh!

DarkDimius May 27, 2016

Uh oh!

odersky commented May 27, 2016

Uh oh!

smarter May 28, 2016 •

edited

Loading

Uh oh!

smarter commented May 30, 2016

Uh oh!

smarter May 30, 2016

Uh oh!

smarter May 30, 2016

Uh oh!

odersky commented Jun 8, 2016

Uh oh!

smarter Jun 24, 2016

Uh oh!

odersky commented Jun 29, 2016

Uh oh!

Uh oh!

[WIP] Change HK encoding #1282

[WIP] Change HK encoding #1282

Uh oh!

Conversation

odersky commented May 27, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Uh oh!

DarkDimius May 27, 2016

Choose a reason for hiding this comment

Uh oh!

odersky commented May 27, 2016

Uh oh!

smarter May 28, 2016 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Choose a reason for hiding this comment

Uh oh!

smarter commented May 30, 2016

Uh oh!

smarter May 30, 2016

Choose a reason for hiding this comment

Uh oh!

smarter May 30, 2016

Choose a reason for hiding this comment

Uh oh!

odersky commented Jun 8, 2016

Uh oh!

smarter Jun 24, 2016

Choose a reason for hiding this comment

Uh oh!

odersky commented Jun 29, 2016

Uh oh!

Uh oh!

odersky commented May 27, 2016 •

edited

Loading

smarter May 28, 2016 •

edited

Loading