|
| 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 every local variable in T (including locally created EX-skolems) |
| 28 | + with a fresh EX-bound variable, and EX-quantify T over all freshly created EX-bound variables. |
| 29 | + - Check that no local variable appears under a box. |
| 30 | +
|
| 31 | +In cv-computation (markFree): |
| 32 | +
|
| 33 | + - Reach capabilities x* of a parameter x cannot appear in the capture set of |
| 34 | + the owning method. They have to be widened to dcs(x), or, where this is not |
| 35 | + possible, it's an error. |
| 36 | +
|
| 37 | +In well-formedness checking of explicitly written type T: |
| 38 | +
|
| 39 | + - If T is not the type of a parameter, check that no EX-bound variable appears |
| 40 | + under a box. |
| 41 | +
|
| 42 | +Subtype rules |
| 43 | +
|
| 44 | + - new alphabet: existentially bound variables `a`. |
| 45 | + - they can be stored in environments Gamma. |
| 46 | + - they are alpha-renable, usual hygiene conditions apply |
| 47 | +
|
| 48 | + Gamma |- EX a.T <: U |
| 49 | + if Gamma, a |- T <: U |
| 50 | +
|
| 51 | + Gamma |- T <: EX a.U |
| 52 | + if a in Gamma, T <: U |
| 53 | +
|
| 54 | +Representation: |
| 55 | +
|
| 56 | + EX a.T[a] is represented as |
| 57 | +
|
| 58 | + r @ RecType(T[TermRef[r.recThis, excap]] |
| 59 | +
|
| 60 | + where `excap` is a global synthetic symbol. |
| 61 | +
|
| 62 | +Subtype checking algorithm, general scheme: |
| 63 | +
|
| 64 | + Maintain two structures in TypeComparer: |
| 65 | +
|
| 66 | + openExistentials: List[RecThis] |
| 67 | + assocExistentials: Map[RecThis, List[RecThis]] |
| 68 | +
|
| 69 | + `openExistentials` corresponds to the list of existential variables stored in the environment. |
| 70 | + `assocExistentials` maps existential variables bound by existentials appearing on the right |
| 71 | + of a subtype judgement to a list of possible associations. Initally this is openExistentials |
| 72 | + at the time when the existential on the right was dropped. It can become a single existential |
| 73 | + when the existentially bound key variable is unified with one of the variables in the |
| 74 | + environment. |
| 75 | +
|
| 76 | +Subtype checking algorithm, steps to add for tp1 <:< tp2: |
| 77 | +
|
| 78 | + If tp1 is an existential EX a.tp1a: |
| 79 | +
|
| 80 | + val saved = openExistentials |
| 81 | + openExistentials = tp1.recThis :: openExistentials |
| 82 | + try tp1a <:< tp2 |
| 83 | + finally openExistentials = saved |
| 84 | +
|
| 85 | + If tp2 is an existential EX a.tp2a: |
| 86 | +
|
| 87 | + val saved = assocExistentials |
| 88 | + assocExistentials = assocExistentials + (tp2.recThis -> openExistentials |
| 89 | + try tp1 <:< tp2a |
| 90 | + finally assocExistentials = saved |
| 91 | +
|
| 92 | + If tp1 and tp2 are existentially bound variables `TermRef(pre1/pre2: RecThis, excap)`: |
| 93 | +
|
| 94 | + assocExistentials(pre2).contains(pre1) && |
| 95 | + { assocExistentials(pre2) = List(pre1); true } |
| 96 | +
|
| 97 | +Existential source syntax: |
| 98 | +
|
| 99 | + Existential types are ususally not written in source, since we still allow the `^` |
| 100 | + syntax that can express most of them more concesely (see below for translation rules). |
| 101 | + But we should also allow to write existential types explicity, even if it ends up mainly |
| 102 | + for debugging. To express them, we add the following trait definition in the caps object: |
| 103 | +
|
| 104 | + trait Exists[X] |
| 105 | +
|
| 106 | + A typical expression of an existential is then |
| 107 | +
|
| 108 | + Exists[(x: Capability) => A ->{x} B] |
| 109 | +
|
| 110 | + Existential types are expanded at Typer to the RecType syntax presented above. It is checked |
| 111 | + that the type argument is a dependent function type with one argument of type `Capability` and |
| 112 | + that this argument is used only in capture sets of the result type. |
| 113 | +
|
| 114 | + Existential types can only appear at the top-level of _legal existential scopes_. These are: |
| 115 | +
|
| 116 | + - The type of a binding: i.e a type of a parameter or val, a result type of a def, or |
| 117 | + a self type of a class. |
| 118 | + - The type of a type ascription in an expression or pattern |
| 119 | + - The argument and result types of a function. |
| 120 | +
|
| 121 | +Expansion of ^: |
| 122 | +
|
| 123 | + We drop `cap` as a capture reference, but keep the unqualified `^` syntax. |
| 124 | + This now expands to existentials. The translation treats each legal existential scope |
| 125 | + separately. If existential scopes nest, the inner ones are translated first. |
| 126 | +
|
| 127 | + The expansion algorithm is then defined as follows: |
| 128 | +
|
| 129 | + 1. In an existential scope, replace every occurrence of ^ with a fresh existentially |
| 130 | + bound variable and quantify over all variables such introduced. |
| 131 | +
|
| 132 | + 2. After this step, type aliases are expanded. If aliases have aliases in arguments, |
| 133 | + the outer alias is expanded before the aliases in the arguments. Each time an alias |
| 134 | + is expanded that reveals a `^`, apply step (1). |
| 135 | +
|
| 136 | + 3. The algorithm ends when no more alieases remain to be expanded. |
| 137 | +
|
| 138 | + ^ captures outside an existential scope or the right hand side of a type alias (e.g. in |
| 139 | + a class parent) are not allowed. |
| 140 | +
|
| 141 | + Examples: |
| 142 | +
|
| 143 | + - `A => B` is an alias type that expands to `(A -> B)^`, which expands to `EX c. A ->{c} B`. |
| 144 | +
|
| 145 | + - `Iterator[A => B]` expands to `EX c. Iterator[A ->{c} B]` |
| 146 | +
|
| 147 | + - `A -> B^` expands to `A -> EX c.B^{c}`. |
| 148 | +
|
| 149 | + - If we define `type Fun[T] = A -> T`, then `Fun[B^]` expands to `EX c.Fun[B^{c}]`, which |
| 150 | + dealiases to `EX c.A -> B^{c}`. |
| 151 | +
|
| 152 | + - If we define |
| 153 | +
|
| 154 | + type F = A -> Fun[B^] |
| 155 | +
|
| 156 | + then the type alias expands to |
| 157 | +
|
| 158 | + type F = A -> EX c.A -> B^{c} |
| 159 | +
|
| 160 | + since the result type of the RHS is a legal existential scope. |
| 161 | +*/ |
| 162 | +object Existential: |
| 163 | + |
| 164 | + /** Pack current type into an existential so that all references to `sym` |
| 165 | + * become bound references of the new existential `rt`. |
| 166 | + */ |
| 167 | + private class PackMap(sym: Symbol, rt: RecType)(using Context) extends DeepTypeMap, IdempotentCaptRefMap: |
| 168 | + def apply(tp: Type): Type = tp match |
| 169 | + case ref: TermRef if ref.symbol == sym => TermRef(rt.recThis, defn.globalExcapSymbol) |
| 170 | + case _ => mapOver(tp) |
| 171 | + |
| 172 | + /** Unpack current type from an existential `rt` so that all references bound by `rt` |
| 173 | + * are recplaced by `ref`. |
| 174 | + */ |
| 175 | + private class OpenMap(rt: RecType, ref: Type)(using Context) extends DeepTypeMap, IdempotentCaptRefMap: |
| 176 | + def apply(tp: Type): Type = |
| 177 | + if isExBound(tp, rt) then ref else mapOver(tp) |
| 178 | + |
| 179 | + /** Is `tp` a reference to the bound variable of `rt`? */ |
| 180 | + private def isExBound(tp: Type, rt: Type)(using Context) = tp match |
| 181 | + case tp @ TermRef(RecThis(rt1), _) => (rt1 eq rt) && tp.symbol == defn.globalExcapSymbol |
| 182 | + case _ => false |
| 183 | + |
| 184 | + /** Open existential, replacing the bund variable by `ref` */ |
| 185 | + def open(rt: RecType, ref: Type)(using Context): Type = OpenMap(rt, ref)(rt.parent) |
| 186 | + |
| 187 | + /** Create a new existential skolem symbol with given `owner`. Nesting of existential |
| 188 | + * skolem symbols is represented by their owner chain. |
| 189 | + */ |
| 190 | + def newSkolem(owner: Symbol)(using Context): Symbol = |
| 191 | + Symbols.newSymbol(owner, nme.EXCAP, Synthetic, defn.Caps_Cap.typeRef) |
| 192 | + |
| 193 | + /** Create an existential type `ex c.<tp>` so that all references to `sym` in `tp` |
| 194 | + * become references to the existentially bound variable `c`. |
| 195 | + */ |
| 196 | + def fromSymbol(tp: Type, sym: Symbol)(using Context): RecType = |
| 197 | + RecType(PackMap(sym, _)(tp)) |
| 198 | + |
| 199 | + def unapply(rt: RecType)(using Context): Option[Type] = |
| 200 | + if isCaptureChecking && rt.parent.existsPart(isExBound(_, rt)) |
| 201 | + then Some(rt.parent) |
| 202 | + else None |
| 203 | + |
| 204 | +end Existential |
0 commit comments