|
| 1 | +package dotty.tools |
| 2 | +package dotc |
| 3 | +package cc |
| 4 | + |
| 5 | +import core.* |
| 6 | +import Types.*, Symbols.*, Contexts.*, Annotations.*, Flags.* |
| 7 | +import CaptureSet.IdempotentCaptRefMap |
| 8 | +import StdNames.nme |
| 9 | + |
| 10 | +/** |
| 11 | +
|
| 12 | +Handling existentials in CC: |
| 13 | +
|
| 14 | +In adapt: |
| 15 | +
|
| 16 | + - If an EX is toplevel in expected type, replace with a fresh capture set variable |
| 17 | + - If an EX is toplevel in actual type, find a trackable replacement `x` as follows: |
| 18 | + + If actual type is a trackable ref, pick that |
| 19 | + + Otherwise, create a fresh skolem val symbol with currently enclosing |
| 20 | + method as owner, and use its termRef |
| 21 | + Then, |
| 22 | + + If the EX-bound variable appears only at toplevel, replace it with `x` |
| 23 | + + Otherwise, replace it with a fresh reach capability `x*`. |
| 24 | +
|
| 25 | +In avoidance of a type T: |
| 26 | +
|
| 27 | + - Replace all co-variant occurrences of locals variables in T (including locally |
| 28 | + created EX-skolems) with single fresh EX-bound variable, which wraps T. |
| 29 | + - Contravariant occurrences of local variables are approximated by the empty capture set, |
| 30 | + as was the case before. |
| 31 | + - Invariant occurrences of local variables produce errors, as was the case before. |
| 32 | + - Check that no existentially quantified local variable appears under a box. |
| 33 | +
|
| 34 | +The reason it is done this way is that it produces the smallest existential type |
| 35 | +wrt the existential type ordering shown below. For instance, consider the type |
| 36 | +
|
| 37 | + (A^{x}, B^{y}) |
| 38 | +
|
| 39 | +where `x` and `y` are local. We widen to |
| 40 | +
|
| 41 | + EX a.(A^{a}, B^{a}) |
| 42 | +
|
| 43 | +rather than |
| 44 | +
|
| 45 | + EX a.EX b.(A^{a}, A^{b}) |
| 46 | +
|
| 47 | +In the subtype ordering of existentials the first of these types is a subtype of |
| 48 | +the other, but not _vice versa_. |
| 49 | +
|
| 50 | +In cv-computation (markFree): |
| 51 | +
|
| 52 | + - Reach capabilities x* of a parameter x cannot appear in the capture set of |
| 53 | + the owning method. They have to be widened to dcs(x), or, where this is not |
| 54 | + possible, it's an error. |
| 55 | +
|
| 56 | +In well-formedness checking of explicitly written type T: |
| 57 | +
|
| 58 | + - If T is not the type of a parameter, check that no EX-bound variable appears |
| 59 | + under a box. |
| 60 | +
|
| 61 | +Subtype rules |
| 62 | +
|
| 63 | + - new alphabet: existentially bound variables `a`. |
| 64 | + - they can be stored in environments Gamma. |
| 65 | + - they are alpha-renable, usual hygiene conditions apply |
| 66 | +
|
| 67 | + Gamma |- EX a.T <: U |
| 68 | + if Gamma, a |- T <: U |
| 69 | +
|
| 70 | + Gamma |- T <: EX a.U |
| 71 | + if a in Gamma, T <: U |
| 72 | +
|
| 73 | + Note that this is a fairly restrictive ordering. A more permissive ordering would |
| 74 | + allow us to instantiate EX-quantified variables to sets of other EX-quantified |
| 75 | + variables since in the end all we need to do is ensure subcapturing of sets. But |
| 76 | + that would be algorithmically more complicated. |
| 77 | +
|
| 78 | +Representation: |
| 79 | +
|
| 80 | + EX a.T[a] is represented as |
| 81 | +
|
| 82 | + r @ RecType(T[TermRef[r.recThis, caps.cap]] |
| 83 | +
|
| 84 | +Subtype checking algorithm, general scheme: |
| 85 | +
|
| 86 | + Maintain two structures in TypeComparer: |
| 87 | +
|
| 88 | + openExistentials: List[RecThis] |
| 89 | + assocExistentials: Map[RecThis, List[RecThis]] |
| 90 | +
|
| 91 | + `openExistentials` corresponds to the list of existential variables stored in the environment. |
| 92 | + `assocExistentials` maps existential variables bound by existentials appearing on the right |
| 93 | + of a subtype judgement to a list of possible associations. Initally this is openExistentials |
| 94 | + at the time when the existential on the right was dropped. It can become a single existential |
| 95 | + when the existentially bound key variable is unified with one of the variables in the |
| 96 | + environment. |
| 97 | +
|
| 98 | +Subtype checking algorithm, steps to add for tp1 <:< tp2: |
| 99 | +
|
| 100 | + If tp1 is an existential EX a.tp1a: |
| 101 | +
|
| 102 | + val saved = openExistentials |
| 103 | + openExistentials = tp1.recThis :: openExistentials |
| 104 | + try tp1a <:< tp2 |
| 105 | + finally openExistentials = saved |
| 106 | +
|
| 107 | + If tp2 is an existential EX a.tp2a: |
| 108 | +
|
| 109 | + val saved = assocExistentials |
| 110 | + assocExistentials = assocExistentials + (tp2.recThis -> openExistentials |
| 111 | + try tp1 <:< tp2a |
| 112 | + finally assocExistentials = saved |
| 113 | +
|
| 114 | + If tp1 and tp2 are existentially bound variables `TermRef(pre1/pre2: RecThis, cap)`: |
| 115 | +
|
| 116 | + assocExistentials(pre2).contains(pre1) && |
| 117 | + { assocExistentials(pre2) = List(pre1); true } |
| 118 | +
|
| 119 | +Existential source syntax: |
| 120 | +
|
| 121 | + Existential types are ususally not written in source, since we still allow the `^` |
| 122 | + syntax that can express most of them more concesely (see below for translation rules). |
| 123 | + But we should also allow to write existential types explicity, even if it ends up mainly |
| 124 | + for debugging. To express them, we add the following trait definition in the caps object: |
| 125 | +
|
| 126 | + trait Exists[X] |
| 127 | +
|
| 128 | + A typical expression of an existential is then |
| 129 | +
|
| 130 | + Exists[(x: Capability) => A ->{x} B] |
| 131 | +
|
| 132 | + Existential types are expanded at Typer to the RecType syntax presented above. It is checked |
| 133 | + that the type argument is a dependent function type with one argument of type `Capability` and |
| 134 | + that this argument is used only in capture sets of the result type. |
| 135 | +
|
| 136 | + Existential types can only appear at the top-level of _legal existential scopes_. These are: |
| 137 | +
|
| 138 | + - The type of a binding: i.e a type of a parameter or val, a result type of a def, or |
| 139 | + a self type of a class. |
| 140 | + - The type of a type ascription in an expression or pattern |
| 141 | + - The argument and result types of a function. |
| 142 | +
|
| 143 | +Expansion of ^: |
| 144 | +
|
| 145 | + We drop `cap` as a capture reference, but keep the unqualified `^` syntax. |
| 146 | + This now expands to existentials. The translation treats each legal existential scope |
| 147 | + separately. If existential scopes nest, the inner ones are translated first. |
| 148 | +
|
| 149 | + The expansion algorithm is then defined as follows: |
| 150 | +
|
| 151 | + 1. In an existential scope, replace every occurrence of ^ with a fresh existentially |
| 152 | + bound variable and quantify over all variables such introduced. |
| 153 | +
|
| 154 | + 2. After this step, type aliases are expanded. If aliases have aliases in arguments, |
| 155 | + the outer alias is expanded before the aliases in the arguments. Each time an alias |
| 156 | + is expanded that reveals a `^`, apply step (1). |
| 157 | +
|
| 158 | + 3. The algorithm ends when no more alieases remain to be expanded. |
| 159 | +
|
| 160 | + ^ captures outside an existential scope or the right hand side of a type alias (e.g. in |
| 161 | + a class parent) are not allowed. |
| 162 | +
|
| 163 | + Examples: |
| 164 | +
|
| 165 | + - `A => B` is an alias type that expands to `(A -> B)^`, which expands to `EX c. A ->{c} B`. |
| 166 | +
|
| 167 | + - `Iterator[A => B]` expands to `EX c. Iterator[A ->{c} B]` |
| 168 | +
|
| 169 | + - `A -> B^` expands to `A -> EX c.B^{c}`. |
| 170 | +
|
| 171 | + - If we define `type Fun[T] = A -> T`, then `Fun[B^]` expands to `EX c.Fun[B^{c}]`, which |
| 172 | + dealiases to `EX c.A -> B^{c}`. |
| 173 | +
|
| 174 | + - If we define |
| 175 | +
|
| 176 | + type F = A -> Fun[B^] |
| 177 | +
|
| 178 | + then the type alias expands to |
| 179 | +
|
| 180 | + type F = A -> EX c.A -> B^{c} |
| 181 | +
|
| 182 | + since the result type of the RHS is a legal existential scope. |
| 183 | +*/ |
| 184 | +object Existential: |
| 185 | + |
| 186 | + private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap: |
| 187 | + def apply(tp: Type): Type = tp match |
| 188 | + case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.captureRoot) |
| 189 | + case _ => mapOver(tp) |
| 190 | + |
| 191 | + /** Unpack current type from an existential `rt` so that all references bound by `rt` |
| 192 | + * are recplaced by `ref`. |
| 193 | + */ |
| 194 | + private class OpenMap(rt: RecType, ref: Type)(using Context) extends DeepTypeMap, IdempotentCaptRefMap: |
| 195 | + def apply(tp: Type): Type = |
| 196 | + if isExBound(tp, rt) then ref else mapOver(tp) |
| 197 | + |
| 198 | + /** Is `tp` a reference to the bound variable of `rt`? */ |
| 199 | + private def isExBound(tp: Type, rt: Type)(using Context) = tp match |
| 200 | + case tp @ TermRef(RecThis(rt1), _) => (rt1 eq rt) && tp.symbol == defn.captureRoot |
| 201 | + case _ => false |
| 202 | + |
| 203 | + /** Open existential, replacing the bund variable by `ref` */ |
| 204 | + def open(rt: RecType, ref: Type)(using Context): Type = OpenMap(rt, ref)(rt.parent) |
| 205 | + |
| 206 | + /** Create an existential type `ex c.<tp>` so that all references to `sym` in `tp` |
| 207 | + * become references to the existentially bound variable `c`. |
| 208 | + */ |
| 209 | + def fromSymbol(tp: Type, sym: Symbol)(using Context): RecType = |
| 210 | + RecType(PackMap(sym, _)(tp)) |
| 211 | + |
| 212 | + def unapply(rt: RecType)(using Context): Option[Type] = |
| 213 | + if isCaptureChecking && rt.parent.existsPart(isExBound(_, rt)) |
| 214 | + then Some(rt.parent) |
| 215 | + else None |
| 216 | + |
| 217 | +end Existential |
0 commit comments