Type Lambdas Spec

Author: odersky

docs/docs/reference/type-lambdas-spec.md

@@ -0,0 +1,49 @@
+---
+layout: doc-page
+title: "Type Lambdas - More Details"
+---
+
+## Syntax
+
+```
+Type              ::=  ... |  HkTypeParamClause ‘=>’ Type
+HkTypeParamClause ::=  ‘[’ HkTypeParam {‘,’ HkTypeParam} ‘]’
+HkTypeParam       ::=  {Annotation} [‘+’ | ‘-’] (Id[HkTypeParamClause] | ‘_’) TypeBounds
+TypeBounds        ::=  [‘>:’ Type] [‘<:’ Type]
+```
+
+### Type Checking
+
+A type lambda such `[X] => F[X]` defines a function from types to types. The parameter(s) may carry bounds and variance annotations.
+If a parameter is is bounded, as in `[X >: L <: H] => F[X]` it is checked that arguments to the parameters conform to the bounds `L` and `H`.
+Only the upper bound `H` can be F-bounded, i.e. `X` can appear in it.
+
+A variance annotation on a parameter indicates a subtyping relationship on type instances. For instance, given
+```
+type TL1 = [+A] => F[A]
+type TL2 = [-A] => F[A]
+```
+and two types `S <: T`, we have
+```
+TL1[S] <: TL1[T
+TL2[T] <: TL2[S]
+```
+It is checked that variance annotations on parameters of type lambdas are respected by the parameter occurrences on the
+type lambda's body.
+
+## Subtyping Rules
+
+Assume two type lambdas
+```
+type TL1  =  [v1 X >: L1 <: U1] => R1
+type TL2  =  [v2 X >: L2 <: U2] => R2
+```
+where `v1` and `v2` are optional variance annotations: `+`, `-`, or absent.
+Then `TL1 <: TL2`, if the type interval `L2..U2` is contained in the type interval `L1..U1` (i.e.
+`L1 <: L2` and `U2 <: U1`), and either `v2` is absent or `v1 = v2`.
+
+
+
+
+
+

docs/docs/reference/type-lambdas.md

@@ -20,3 +20,5 @@ is a shorthand for a plain type definition with a type-lambda as its
 right-hand side:
 
     type T = [X] => (X, X)
+
+[More details](./type-lambdas-spec.md)

tests/neg/type-lambdas.scala

@@ -0,0 +1,29 @@
+object Test extends App {
+
+  trait Ord[X]
+
+  type TL1 = [X <: Ord[X]] => (X, X) // OK
+  type TL2 = [X >: Ord[X]] => (X, X) // error
+
+  class C extends Ord[C]
+
+  type T1 = TL1[Int] // will be discovered later
+  type T2 = TL1[C]   // OK
+
+  class Ref[X](init: X) {
+    var x: X = init
+  }
+
+  type TL3 = [+X] => Ref[X]
+
+  def f[F <: [+X] => Any](x: F[String]): F[Any] = x
+
+  val sref = new Ref[String]("abc")
+  val aref: Ref[Any] = f[TL3](sref)
+  aref.x = 1
+  val s: String = sref.x
+
+
+
+
+}