Skip to content

Change HK types scheme #731

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

Closed
wants to merge 42 commits into from
Closed

Change HK types scheme #731

wants to merge 42 commits into from

Conversation

odersky
Copy link
Contributor

@odersky odersky commented Jul 22, 2015

I recently found out that the original scheme for hk types in dotty
that I proposed does not work. Here is a counter example:

trait Iterable[IA, C <: Iterable]
trait Seq[SA, C <: Seq] extends Iterable[A, C]
val s: Seq[Int, Seq] = ???
val i: Iterable[Int, Iterable]

Now, we said that the type C in Iterable has two type parameters, the
IA and the C. So if C <: Iterable, then

C[T, D] would translate to C { type IA = D, type C = D }.

Analogously, if C <: Seq, then

C[T, D] would translate to C { type SA = D, type C = D }

The problem is when we see a C defined to be <: Seq as a subtype of Iterable.
The two versions have the same number parameters, but the fields are different!
We'd be translating then C[T, D] to C { type IA = D, type C = D } which makes no
sense, it would just give us a double binding of IA. It turns out this
cannot be worked around in general; asSeenFrom interacts in fatal ways
with the scheme.

To fix this, we now always use the (formerly backup) scheme of type lambdas, paired
by a new notion of "eta-reduction" to keep types small.

Review by @adriaanm

odersky added 30 commits July 16, 2015 17:48
Avoid forcing info if the reference goes to a class. This avoided
a CyclicReference when reading Scala's standard library form pos/collections
when fiddling with the hk logic.
In Namer, eta expand any type argument that corresponds to a higher-kinded type parameter.
Also, check that all type parameter lists are fully applied.
With the hk-types schem changed, we need to make sure that actual and formal argument lists
of parameterized types have the same length.
It used to be "assertion error: NoType" whenever sigName git
a projection of a missing member. Now we find out about
what type was projected.
Now catches attempts to recursively force a LazyRef type
that's in train of being evaluated.
Erreneous programs could have a difference in lengths
between type parameters and type args, but this is tested
anyway in Typer.
... and move to TypeApplications. isLambda test
was the wrong way before.
Without the additional `typeParams.nonEmpty` condition we got a crash
in t1439.scala
Previously, we did this only in applications in rhs of type definitions.
Need to do it everywhere.
This would lead to a crash. Example is in Predef:

    object Pair
    type Pair
EtaReduce will be used to keep applications on eta expanded methods small.
parameterizeWith picked between simple hk types and lambda abstraction.
No longer needed because now we always lambda abstract.
Needed to avoid cycles involving F-boundes hk-types when reading Scala2 collection classes
with new hk-scheme.
When unpickling from Scala2 TypeRefs with arguments which do not
refer to classes, use EtaExpand instead of LambdaAbstract. Lambda Abstrct
is wrong since it drops type arguments.
New hk-scheme caused cycles in elimExistentials which are fixed
by this patch.
Derived types already contain the lambda abstractoion; lambda abstracting
them again would cause a double lambda.
Discrepancies between numbers of formal and actual type arguments were
observed when typing partialFunctions.scala under new scheme.

Should come back to this when subtyping is rewrittem/simplified to
work with new hk-scheme. Maybe testLifted is no longer needed at all.
This aligns typeParams and rawTypeParams. It's not strictly to necessary, though.
Rewrite a type application like

    ([HK$0] => C[HK$0])(T)   to   C[T]

Avoids application cahins to become unnecessarly large.
Used to be just instantiated lambdas. With the new scheme
every type with a kind higher than * needs to be projected
with #Apply.
Turn a possible NPE into an AssertionError. The latter
are caught in pickleTree, so an error leaves a trace about
what was pickled.
Previously, only pattern bound arguments were adapated. This was an oversight.
Also, change logix so that we survive empty type parameter lists. This was
also an oversight before.
odersky added 12 commits July 20, 2015 10:36
Want to have a unique name for Apply, so that tests for higher-kinded types become cheaper.
by removing dead case.
These are not user-accessible types, so no need to follow
type convention and write in upper case.

Also, rename occurrences of lambda to Lambda, to make clear
we mean a type lambda.
It's no longer needed with new hk scheme.
Replace occurrences of isLambda with isHK, because isHK is
a bit faster and simplier.
Accidentally forwarded to rawTypeParams. This solved the problem with mismatching
type params in appliedTo that was caught in testLifted.
Now also allows to reduce something like

  ([T] => Map[T, String])

to

  Map[_, String]
...unless the HK type can be eta-reduced to a class type.
1) Lambda abstract now records bounds of abstracted type parameters in TypeLambda
2) Eta-reduce likewise keeps the bounds it finds in the TypeLambda
3) Eta-reduce now also translates hk$i references to type parameters of the reduced type.
The original IterableSelfRec is not syntactically legal after
the hk changes. I attempted to fix, but there's still a type error.
Need to investigate whether this is a true error or a bug.
* - `bounds` consists of type declarations `type hk$i >: toHK(L) <: toHK(U),
* one for each type parameter in `T` with non-trivial bounds L,U.
* - `toHK` is a substitution that replaces every bound symbol sym_i by
* `this.Arg$i`.
Copy link
Member

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Should be this.hk$i.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Yes, I fixed the comments in #802

@odersky odersky mentioned this pull request Sep 21, 2015
@odersky
Copy link
Contributor Author

odersky commented Sep 21, 2015

Closed in favor of #802

@odersky odersky closed this Sep 21, 2015
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants