diff options
Diffstat (limited to 'docs/HigherKinded-v2.md')
| -rw-r--r-- | docs/HigherKinded-v2.md | 375 |
1 files changed, 0 insertions, 375 deletions
diff --git a/docs/HigherKinded-v2.md b/docs/HigherKinded-v2.md deleted file mode 100644 index 2ca6424de..000000000 --- a/docs/HigherKinded-v2.md +++ /dev/null @@ -1,375 +0,0 @@ -Higher-Kinded Types in Dotty V2 -=============================== - -This note outlines how we intend to represent higher-kinded types in -Dotty. The principal idea is to collapse the four previously -disparate features of refinements, type parameters, existentials and -higher-kinded types into just one: refinements of type members. All -other features will be encoded using these refinements. - -The complexity of type systems tends to grow exponentially with the -number of independent features, because there are an exponential -number of possible feature interactions. Consequently, a reduction -from 4 to 1 fundamental features achieves a dramatic reduction of -complexity. It also adds some nice usablilty improvements, notably in -the area of partial type application. - -This is a second version of the scheme which differs in a key aspect -from the first one: Following Adriaan's idea, we use traits with type -members to model type lambdas and type applications. This is both more -general and more robust than the intersections with type constructor -traits that we had in the first version. - -The duality ------------ - -The core idea: A parameterized class such as - - class Map[K, V] - -is treated as equivalent to a type with type members: - - class Map { type Map$K; type Map$V } - -The type members are name-mangled (i.e. `Map$K`) so that they do not conflict with other -members or parameters named `K` or `V`. - -A type-instance such as `Map[String, Int]` would then be treated as equivalent to - - Map { type Map$K = String; type Map$V = Int } - -Named type parameters ---------------------- - -Type parameters can have unmangled names. This is achieved by adding the `type` keyword -to a type parameter declaration, analogous to how `val` indicates a named field. For instance, - - class Map[type K, type V] - -is treated as equivalent to - - class Map { type K; type V } - -The parameters are made visible as fields. - -Wildcards ---------- - -A wildcard type such as `Map[_, Int]` is equivalent to - - Map { type Map$V = Int } - -I.e. `_`'s omit parameters from being instantiated. Wildcard arguments -can have bounds. E.g. - - Map[_ <: AnyRef, Int] - -is equivalent to - - Map { type Map$K <: AnyRef; type Map$V = Int } - - -Type parameters in the encodings --------------------------------- - -The notion of type parameters makes sense even for encoded types, -which do not contain parameter lists in their syntax. Specifically, -the type parameters of a type are a sequence of type fields that -correspond to parameters in the unencoded type. They are determined as -follows. - - - The type parameters of a class or trait type are those parameter fields declared in the class - that are not yet instantiated, in the order they are given. Type parameter fields of parents - are not considered. - - The type parameters of an abstract type are the type parameters of its upper bound. - - The type parameters of an alias type are the type parameters of its right hand side. - - The type parameters of every other type is the empty sequence. - -Partial applications --------------------- - -The definition of type parameters in the previous section leads to a simple model of partial applications. -Consider for instance: - - type Histogram = Map[_, Int] - -`Histogram` is a higher-kinded type that still has one type parameter. -`Histogram[String]` -would be a possible type instance, and it would be equivalent to `Map[String, Int]`. - - -Modelling polymorphic type declarations ---------------------------------------- - -The partial application scheme gives us a new -- and quite elegant -- -way to do certain higher-kinded types. But how do we interprete the -poymorphic types that exist in current Scala? - -More concretely, current Scala allows us to write parameterized type -definitions, abstract types, and type parameters. In the new scheme, -only classes (and traits) can have parameters and these are treated as -equivalent to type members. Type aliases and abstract types do not -allow the definition of parameterized types so we have to interprete -polymorphic type aliases and abstract types specially. - -Modelling polymorphic type aliases: simple case ------------------------------------------------ - -A polymorphic type alias such as - - type Pair[T] = Tuple2[T, T] - -where `Tuple2` is declared as - - class Tuple2[T1, T2] ... - -is expanded to a monomorphic type alias like this: - - type Pair = Tuple2 { type Tuple2$T2 = Tuple2$T1 } - -More generally, each type parameter of the left-hand side must -appear as a type member of the right hand side type. Type members -must appear in the same order as their corresponding type parameters. -References to the type parameter are then translated to references to the -type member. The type member itself is left uninstantiated. - -This technique can expand most polymorphic type aliases appearing -in Scala codebases but not all of them. For instance, the following -alias cannot be expanded, because the parameter type `T` is not a -type member of the right-hand side `List[List[T]]`. - - type List2[T] = List[List[T]] - -We scanned the Scala standard library for occurrences of polymorphic -type aliases and determined that only two occurrences could not be expanded. -In `io/Codec.scala`: - - type Configure[T] = (T => T, Boolean) - -And in `collection/immutable/HashMap.scala`: - - private type MergeFunction[A1, B1] = ((A1, B1), (A1, B1)) => (A1, B1) - -For these cases, we use a fall-back scheme that models a parameterized alias as a -`Lambda` type. - -Modelling polymorphic type aliases: general case ------------------------------------------------- - -A polymorphic type alias such as - - type List2D[T] = List[List[T]] - -is represented as a monomorphic type alias of a type lambda. Here's the expanded version of -the definition above: - - type List2D = Lambda$I { type Apply = List[List[$hkArg$0]] } - -Here, `Lambda$I` is a standard trait defined as follows: - - trait Lambda$I[type $hkArg$0] { type +Apply } - -The `I` suffix of the `Lambda` trait indicates that it has one invariant type parameter (named $hkArg$0). -Other suffixes are `P` for covariant type parameters, and `N` for contravariant type parameters. Lambda traits can -have more than one type parameter. For instance, here is a trait with contravariant and covariant type parameters: - - trait Lambda$NP[type -$hkArg$0, +$hkArg1] { type +Apply } extends Lambda$IP with Lambda$NI - -Aside: the `+` prefix in front of `Apply` indicates that `Apply` is a covariant type field. Dotty -admits variance annotations on type members. - -The definition of `Lambda$NP` shows that `Lambda` traits form a subtyping hierarchy: Traits which -have covariant or contravariant type parameters are subtypes of traits which don't. The supertraits -of `Lambda$NP` would themselves be written as follows. - - trait Lambda$IP[type $hkArg$0, +$hkArg1] { type +Apply } extends Lambda$II - trait Lambda$NI[type -$hkArg$0, $hkArg1] { type +Apply } extends Lambda$II - trait Lambda$II[type $hkArg$0, $hkArg1] { type +Apply } - -`Lambda` traits are special in that -they influence how type applications are expanded: If the standard type application `T[X1, ..., Xn]` -leads to a subtype `S` of a type instance - - LambdaXYZ { type Arg1 = T1; ...; type ArgN = Tn; type Apply ... } - -where all argument fields `Arg1, ..., ArgN` are concretely defined -and the definition of the `Apply` field may be either abstract or concrete, then the application -is further expanded to `S # Apply`. - -For instance, the type instance `List2D[String]` would be expanded to - - Lambda$I { type $hkArg$0 = String; type Apply = List[List[String]] } # Apply - -which in turn simplifies to `List[List[String]]`. - -2nd Example: Consider the two aliases - - type RMap[K, V] = Map[V, K] - type RRMap[K, V] = RMap[V, K] - -These expand as follows: - - type RMap = Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] } - type RRMap = Lambda$II { self2 => type Apply = RMap[self2.$hkArg$1, self2.$hkArg$0] } - -Substituting the definition of `RMap` and expanding the type application gives: - - type RRMap = Lambda$II { self2 => type Apply = - Lambda$II { self1 => type Apply = Map[self1.$hkArg$1, self1.$hkArg$0] } - { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply } - -Substituting the definitions for `self1.$hkArg${1,2}` gives: - - type RRMap = Lambda$II { self2 => type Apply = - Lambda$II { self1 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] } - { type $hkArg$0 = self2.$hkArg$1; type $hkArg$1 = self2.$hkArg$0 } # Apply } - -Simplifiying the `# Apply` selection gives: - - type RRMap = Lambda$II { self2 => type Apply = Map[self2.$hkArg$0, self2.$hkArg$1] } - -This can be regarded as the eta-expanded version of `Map`. It has the same expansion as - - type IMap[K, V] = Map[K, V] - - -Modelling higher-kinded types ------------------------------ - -The encoding of higher-kinded types uses again the `Lambda` traits to represent type constructors. -Consider the higher-kinded type declaration - - type Rep[T] - -We expand this to - - type Rep <: Lambda$I - -The type parameters of `Rep` are the type parameters of its upper bound, so -`Rep` is a unary type constructor. - -More generally, a higher-kinded type declaration - - type T[v1 X1 >: S1 <: U1, ..., vn XN >: S1 <: UN] >: SR <: UR - -is encoded as - - type T <: LambdaV1...Vn { self => - type v1 $hkArg$0 >: s(S1) <: s(U1) - ... - type vn $hkArg$N >: s(SN) <: s(UN) - type Apply >: s(SR) <: s(UR) - } - -where `s` is the substitution `[XI := self.$hkArg$I | I = 1,...,N]`. - -If we instantiate `Rep` with a type argument, this is expanded as was explained before. - - Rep[String] - -would expand to - - Rep { type $hkArg$0 = String } # Apply - -If we instantiate the higher-kinded type with a concrete type constructor (i.e. a parameterized -trait or class), we have to do one extra adaptation to make it work. The parameterized trait -or class has to be eta-expanded so that it comforms to the `Lambda` bound. For instance, - - type Rep = Set - -would expand to - - type Rep = Lambda1 { type Apply = Set[$hkArg$0] } - -Or, - - type Rep = Map[String, _] - -would expand to - - type Rep = Lambda1 { type Apply = Map[String, $hkArg$0] } - - -Full example ------------- - -Consider the higher-kinded `Functor` type class - - class Functor[F[_]] { - def map[A, B](f: A => B): F[A] => F[B] - } - -This would be represented as follows: - - class Functor[F <: Lambda1] { - def map[A, B](f: A => B): F { type $hkArg$0 = A } # Apply => F { type $hkArg$0 = B } # Apply - } - -The type `Functor[List]` would be represented as follows - - Functor { - type F = Lambda1 { type Apply = List[$hkArg$0] } - } - -Now, assume we have a value - - val ml: Functor[List] - -Then `ml.map` would have type - - s(F { type $hkArg$0 = A } # Apply => F { type $hkArg$0 = B } # Apply) - -where `s` is the substitution of `[F := Lambda1 { type Apply = List[$hkArg$0] }]`. -This gives: - - Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = A } # Apply - => Lambda1 { type Apply = List[$hkArg$0] } { type $hkArg$0 = B } # Apply - -This type simplifies to: - - List[A] => List[B] - -Status of # ------------ - -In the scheme above we have silently assumed that `#` "does the right -thing", i.e. that the types are well-formed and we can collapse a type -alias with a `#` projection, thereby giving us a form of beta -reduction. - -In Scala 2.x, this would not work, because `T#X` means `x.X forSome { val x: T }`. -Hence, two occurrences of `Rep[Int]` say, would not be recognized to be equal because the -existential would be opened each time afresh. - -In pre-existentials Scala, this would not have worked either. There, `T#X` was a fundamental -type constructor, but was restricted to alias types or classes for both `T` and `X`. -Roughly, `#` was meant to encode Java's inner classes. In Java, given the classes - - class Outer { class Inner } - class Sub1 extends Outer - class Sub2 extends Outer - -The types `Outer#Inner`, `Sub1#Inner` and `Sub2#Inner` would all exist and be -regarded as equal to each other. But if `Outer` had abstract type members this would -not work, since an abstract type member could be instantiated differently in `Sub1` and `Sub2`. -Assuming that `Sub1#Inner = Sub2#Inner` could then lead to a soundness hole. To avoid soundness -problems, the types in `X#Y` were restricted so that `Y` was (an alias of) a class type and -`X` was (an alias of) a class type with no abstract type members. - -I believe we can go back to regarding `T#X` as a fundamental type constructor, the way it -was done in pre-existential Scala, but with the following relaxed restriction: - - _In a type selection `T#x`, `T` is not allowed to have any abstract members different from `X`._ - -This would typecheck the higher-kinded types examples, because they only project with `# Apply` once all -`$hkArg$` type members are fully instantiated. - -It would be good to study this rule formally, trying to verify its soundness. - - - - - - - - |