You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Since variances are associated conceptually with higher-kinded type variables,
it makes no sense to write them on type lambdas. I believe it's better to disallow
writing variances there because it will only need to variance-bike-shedding otherwise.
TypeParam ::= {Annotation} (id [HkTypeParamClause] | ‘_’) TypeBounds
12
12
TypeBounds ::= [‘>:’ Type] [‘<:’ Type]
13
13
```
14
14
@@ -18,44 +18,28 @@ A type lambda such as `[X] =>> F[X]` defines a function from types to types. The
18
18
If a parameter is bounded, as in `[X >: L <: H] =>> F[X]` it is checked that arguments to the parameters conform to the bounds `L` and `H`.
19
19
Only the upper bound `H` can be F-bounded, i.e. `X` can appear in it.
20
20
21
-
A variance annotation on a parameter indicates a subtyping relationship on type instances. For instance, given
22
-
```scala
23
-
typeTL1= [+A] =>>F[A]
24
-
typeTL2= [-A] =>>F[A]
25
-
```
26
-
and two types `S <: T`, we have
27
-
```scala
28
-
TL1[S] <:TL1[T]
29
-
TL2[T] <:TL2[S]
30
-
```
31
-
It is checked that variance annotations on parameters of type lambdas are respected by the parameter occurrences on the type lambda's body.
32
-
33
-
**Note** No requirements hold for the variances of occurrences of type variables in their bounds. It is an open question whether we need to impose additional requirements here
34
-
(`scalac` doesn't check variances in bounds either).
35
-
36
21
## Subtyping Rules
37
22
38
23
Assume two type lambdas
39
24
```scala
40
-
typeTL1= [v1 X>:L1<:U1] =>>R1
41
-
typeTL2= [v2 X>:L2<:U2] =>>R2
25
+
typeTL1= [X>:L1<:U1] =>>R1
26
+
typeTL2= [X>:L2<:U2] =>>R2
42
27
```
43
-
where `v1` and `v2` are optional variance annotations: `+`, `-`, or absent.
44
28
Then `TL1 <: TL2`, if
45
29
46
30
- the type interval `L2..U2` is contained in the type interval `L1..U1` (i.e.
47
31
`L1 <: L2` and `U2 <: U1`),
48
-
- either `v2` is absent or `v1 = v2`
49
32
-`R1 <: R2`
50
33
51
34
Here we have relied on alpha renaming to bring match the two bound types `X`.
52
35
53
36
A partially applied type constructor such as `List` is assumed to be equivalent to
54
-
its eta expansion. I.e, `List = [+X] =>> List[X]`. This allows type constructors
55
-
to be compared with type lambdas.
37
+
its eta expansion. I.e, `List = [X] =>> List[X]`. This allows type constructors to be compared with type lambdas.
56
38
57
39
## Relationship with Parameterized Type Definitions
58
40
41
+
type F[X] <: List[F[X]]
42
+
59
43
A parameterized type definition
60
44
```scala
61
45
typeT[X] =R
@@ -64,6 +48,17 @@ is regarded as a shorthand for an unparameterized definition with a type lambda
64
48
```scala
65
49
typeT= [X] =>>R
66
50
```
51
+
If the a type definition carries `+` or `-` variance annotations,
52
+
it is checked that the variance annotations are satisfied by the type lambda.
53
+
For instance,
54
+
```scala
55
+
typeF2[A, +B] =A=>B
56
+
```scala
57
+
expands to
58
+
```scala
59
+
typeF2= [A, B] =>>A=>B
60
+
```
61
+
and at the same time it is checked that the parameter `B` appears covariantly in `A => B`.
67
62
68
63
A parameterized abstract type
69
64
```scala
@@ -75,15 +70,15 @@ type T >: ([X] =>> L) <: ([X] =>> U)
75
70
```
76
71
However, if `L` is `Nothing` it is not parameterized, since `Nothing` is treated as a bottom type for all kinds. For instance,
77
72
```scala
78
-
typeT[-X] <:X=>()
73
+
typeT[X] <:X=>X
79
74
```
80
75
is expanded to
81
76
```scala
82
-
typeT>:Nothing<: ([-X] =>>X=>())
77
+
typeT>:Nothing<: ([X] =>>X=>X)
83
78
```
84
79
instead of
85
80
```scala
86
-
typeT>: ([X] =>>Nothing) <: ([-X] =>>X=>())
81
+
typeT>: ([X] =>>Nothing) <: ([X] =>>X=>X)
87
82
```
88
83
89
84
The same expansions apply to type parameters. E.g.
@@ -94,6 +89,20 @@ is treated as a shorthand for
94
89
```scala
95
90
[F>:Nothing<: [X] =>>Coll[X]]
96
91
```
92
+
Abstract types and opaque type aliases remember the variances they were created with. So the type
93
+
```scala
94
+
defF2[-A, +B]
95
+
```
96
+
is known to be covariant in `A` and contravariant in `B` and can be instantiated only
97
+
with types that satisfy these constraints. Likewise
98
+
```scala
99
+
opaquetypeO[X] =List[X]
100
+
```
101
+
`O` is known to be invariant (and not covariant, as its right hand side would suggest). On the other hand, a transparent alias
102
+
```scala
103
+
typeO2[X] =List[X]
104
+
```
105
+
would be treated as covariant, `X` is used covariantly on its right-hand side.
97
106
98
107
**Note**: The decision to treat `Nothing` as universal bottom type is provisional, and might be changed afer further discussion.
0 commit comments