diff --git a/compiler/src/dotty/tools/dotc/ast/untpd.scala b/compiler/src/dotty/tools/dotc/ast/untpd.scala index 96c8c4c4f845..76a584ef146a 100644 --- a/compiler/src/dotty/tools/dotc/ast/untpd.scala +++ b/compiler/src/dotty/tools/dotc/ast/untpd.scala @@ -559,6 +559,9 @@ object untpd extends Trees.Instance[Untyped] with UntypedTreeInfo { def makeOnlyAnnot(qid: Tree)(using Context) = New(AppliedTypeTree(ref(defn.OnlyCapabilityAnnot.typeRef), qid :: Nil), Nil :: Nil) + def makeConsumeAnnot()(using Context): Tree = + New(ref(defn.ConsumeAnnot.typeRef), Nil :: Nil) + def makeConstructor(tparams: List[TypeDef], vparamss: List[List[ValDef]], rhs: Tree = EmptyTree)(using Context): DefDef = DefDef(nme.CONSTRUCTOR, joinParams(tparams, vparamss), TypeTree(), rhs) diff --git a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala index f5589caf3872..a3f3d40a42f6 100644 --- a/compiler/src/dotty/tools/dotc/cc/SepCheck.scala +++ b/compiler/src/dotty/tools/dotc/cc/SepCheck.scala @@ -22,9 +22,9 @@ import Capabilities.* * * - Hidden sets of arguments must not be referred to in the same application * - Hidden sets of (result-) types must not be referred to alter in the same scope. - * - Returned hidden sets can only refer to @consume parameters. + * - Returned hidden sets can only refer to consume parameters. * - If returned hidden sets refer to an encloding this, the reference must be - * from a @consume method. + * from a consume method. * - Consumed entities cannot be used subsequently. * - Entitites cannot be consumed in a loop. */ @@ -422,7 +422,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def consumeError(ref: Capability, loc: SrcPos, pos: SrcPos)(using Context): Unit = report.error( em"""Separation failure: Illegal access to $ref, which was passed to a - |@consume parameter or was used as a prefix to a @consume method on line ${loc.line + 1} + |consume parameter or was used as a prefix to a consume method on line ${loc.line + 1} |and therefore is no longer available.""", pos) @@ -433,7 +433,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: def consumeInLoopError(ref: Capability, pos: SrcPos)(using Context): Unit = report.error( em"""Separation failure: $ref appears in a loop, therefore it cannot - |be passed to a @consume parameter or be used as a prefix of a @consume method call.""", + |be passed to a consume parameter or be used as a prefix of a consume method call.""", pos) // ------------ Checks ----------------------------------------------------- @@ -587,16 +587,16 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: /** Check validity of consumed references `refsToCheck`. The references are consumed * because they are hidden in a Fresh result type or they are referred - * to in an argument to a @consume parameter or in a prefix of a @consume method -- + * to in an argument to a consume parameter or in a prefix of a consume method -- * which one applies is determined by the role parameter. * * This entails the following checks: * - The reference must be defined in the same as method or class as * the access. * - If the reference is to a term parameter, that parameter must be - * marked as @consume as well. + * marked as consume as well. * - If the reference is to a this type of the enclosing class, the - * access must be in a @consume method. + * access must be in a consume method. * * References that extend caps.Sharable are excluded from checking. * As a side effect, add all checked references with the given position `pos` @@ -631,7 +631,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: then report.error( em"""Separation failure: $descr non-local this of class ${ref.cls}. - |The access must be in a @consume method to allow this.""", + |The access must be in a consume method to allow this.""", pos) case _ => @@ -643,7 +643,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: val (pluralS, singleS) = if badParams.tail.isEmpty then ("", "s") else ("s", "") report.error( em"""Separation failure: $descr parameter$pluralS ${paramsStr(badParams.toList)}. - |The parameter$pluralS need$singleS to be annotated with @consume to allow this.""", + |The parameter$pluralS need$singleS to be annotated with consume to allow this.""", pos) role match @@ -769,7 +769,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: /** If `tpe` appears as a (result-) type of a definition, treat its * hidden set minus its explicitly declared footprint as consumed. - * If `tpe` appears as an argument to a @consume parameter, treat + * If `tpe` appears as an argument to a consume parameter, treat * its footprint as consumed. */ def checkLegalRefs() = role match @@ -786,7 +786,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: case TypeRole.Argument(arg) => if tpe.hasAnnotation(defn.ConsumeAnnot) then val capts = captures(arg).footprint - checkConsumedRefs(capts, tpe, role, i"argument to @consume parameter with type ${arg.nuType} refers to", pos) + checkConsumedRefs(capts, tpe, role, i"argument to consume parameter with type ${arg.nuType} refers to", pos) case _ => if !tpe.hasAnnotation(defn.UntrackedCapturesAnnot) then @@ -910,7 +910,7 @@ class SepCheck(checker: CheckCaptures.CheckerAPI) extends tpd.TreeTraverser: checkConsumedRefs( captures(qual).footprint, qual.nuType, TypeRole.Qualifier(qual, tree.symbol), - i"call prefix of @consume ${tree.symbol} refers to", qual.srcPos) + i"call prefix of consume ${tree.symbol} refers to", qual.srcPos) case tree: GenericApply => traverseChildren(tree) tree.tpe match diff --git a/compiler/src/dotty/tools/dotc/cc/Setup.scala b/compiler/src/dotty/tools/dotc/cc/Setup.scala index ec312631a61b..aa9b9f399634 100644 --- a/compiler/src/dotty/tools/dotc/cc/Setup.scala +++ b/compiler/src/dotty/tools/dotc/cc/Setup.scala @@ -758,8 +758,8 @@ class Setup extends PreRecheck, SymTransformer, SetupAPI: && !(sym.is(Method) && sym.owner.isClass) then report.error( - em"""@consume cannot be used here. Only member methods and their term parameters - |can have @consume annotations.""", + em"""consume cannot be used here. Only member methods and their term parameters + |can have a consume modifier.""", tree.srcPos) else if annotCls == defn.UseAnnot then if !ccConfig.allowUse then diff --git a/compiler/src/dotty/tools/dotc/core/Definitions.scala b/compiler/src/dotty/tools/dotc/core/Definitions.scala index 79fa0e94e06a..35febde2d307 100644 --- a/compiler/src/dotty/tools/dotc/core/Definitions.scala +++ b/compiler/src/dotty/tools/dotc/core/Definitions.scala @@ -1076,8 +1076,8 @@ class Definitions { @tu lazy val UncheckedCapturesAnnot: ClassSymbol = requiredClass("scala.annotation.unchecked.uncheckedCaptures") @tu lazy val UntrackedCapturesAnnot: ClassSymbol = requiredClass("scala.caps.unsafe.untrackedCaptures") @tu lazy val UseAnnot: ClassSymbol = requiredClass("scala.caps.use") - @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.consume") @tu lazy val ReserveAnnot: ClassSymbol = requiredClass("scala.caps.reserve") + @tu lazy val ConsumeAnnot: ClassSymbol = requiredClass("scala.caps.internal.consume") @tu lazy val RefineOverrideAnnot: ClassSymbol = requiredClass("scala.caps.internal.refineOverride") @tu lazy val VolatileAnnot: ClassSymbol = requiredClass("scala.volatile") @tu lazy val LanguageFeatureMetaAnnot: ClassSymbol = requiredClass("scala.annotation.meta.languageFeature") diff --git a/compiler/src/dotty/tools/dotc/core/StdNames.scala b/compiler/src/dotty/tools/dotc/core/StdNames.scala index 0bde164186b7..a061220b9b69 100644 --- a/compiler/src/dotty/tools/dotc/core/StdNames.scala +++ b/compiler/src/dotty/tools/dotc/core/StdNames.scala @@ -454,6 +454,7 @@ object StdNames { val compiletime : N = "compiletime" val compose: N = "compose" val conforms_ : N = "$conforms" + val consume: N = "consume" val contents: N = "contents" val copy: N = "copy" val create: N = "create" diff --git a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala index f6dd3c2396d4..530a2c29a94c 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Parsers.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Parsers.scala @@ -35,6 +35,7 @@ import config.SourceVersion.* import config.SourceVersion import dotty.tools.dotc.config.MigrationVersion import dotty.tools.dotc.util.chaining.* +import dotty.tools.dotc.config.Feature.ccEnabled object Parsers { @@ -216,6 +217,8 @@ object Parsers { def isPureArrow: Boolean = isPureArrow(nme.PUREARROW) || isPureArrow(nme.PURECTXARROW) def isErased = isIdent(nme.erased) && in.erasedEnabled && in.isSoftModifierInParamModifierPosition + def isConsume = + isIdent(nme.consume) && ccEnabled //\&& in.isSoftModifierInParamModifierPosition def isSimpleLiteral = simpleLiteralTokens.contains(in.token) || isIdent(nme.raw.MINUS) && numericLitTokens.contains(in.lookahead.token) @@ -3325,11 +3328,15 @@ object Parsers { private def addModifier(mods: Modifiers): Modifiers = { val tok = in.token val name = in.name - val mod = atSpan(in.skipToken()) { modOfToken(tok, name) } - - if mods.isOneOf(mod.flags) then - syntaxError(RepeatedModifier(mod.flags.flagsString, source, mod.span), mod.span) - addMod(mods, mod) + if isConsume then + val consumeAnnot = atSpan(in.skipToken())(makeConsumeAnnot()) + mods.withAddedAnnotation(consumeAnnot) + else + val mod = atSpan(in.skipToken()): + modOfToken(tok, name) + if mods.isOneOf(mod.flags) then + syntaxError(RepeatedModifier(mod.flags.flagsString, source, mod.span), mod.span) + addMod(mods, mod) } def addFlag(mods: Modifiers, flag: FlagSet): Modifiers = @@ -3555,7 +3562,8 @@ object Parsers { * UsingParamClause ::= ‘(’ ‘using’ (DefTermParams | ContextTypes) ‘)’ * DefImplicitClause ::= [nl] ‘(’ ‘implicit’ DefTermParams ‘)’ * DefTermParams ::= DefTermParam {‘,’ DefTermParam} - * DefTermParam ::= {Annotation} [‘erased’] [‘inline’] Param + * DefTermParam ::= {Annotation} TermParamMods Param + * TermParamMods ::= [‘erased‘] [‘inline’] | [‘consume‘] * * Param ::= id `:' ParamType [`=' Expr] * @@ -3592,7 +3600,7 @@ object Parsers { def param(): ValDef = { val start = in.offset var mods = impliedMods.withAnnotations(annotations()) - if isErased then + if isConsume || isErased then mods = addModifier(mods) if paramOwner.isClass then mods = addFlag(modifiers(start = mods), ParamAccessor) @@ -3664,6 +3672,7 @@ object Parsers { var mods = EmptyModifiers if in.lookahead.isColon then (mods, true) + else if isConsume then (mods, true) else if isErased then mods = addModifier(mods) val paramsAreNamed = diff --git a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala index ca2f5da3df3c..52e03de60dea 100644 --- a/compiler/src/dotty/tools/dotc/parsing/Scanners.scala +++ b/compiler/src/dotty/tools/dotc/parsing/Scanners.scala @@ -1228,7 +1228,8 @@ object Scanners { && (softModifierNames.contains(name) || name == nme.erased && erasedEnabled || name == nme.tracked && trackedEnabled - || name == nme.update && Feature.ccEnabled) + || name == nme.update && Feature.ccEnabled + || name == nme.consume && Feature.ccEnabled) def isSoftModifierInModifierPosition: Boolean = isSoftModifier && inModifierPosition() diff --git a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala index cda3e7d4b6f2..4a23f00f3c53 100644 --- a/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/PlainPrinter.scala @@ -15,7 +15,7 @@ import util.SourcePosition import scala.util.control.NonFatal import scala.annotation.switch import config.{Config, Feature} -import ast.tpd +import ast.{tpd, untpd} import cc.* import CaptureSet.Mutability import Capabilities.* @@ -716,8 +716,12 @@ class PlainPrinter(_ctx: Context) extends Printer { case _ => literalText(String.valueOf(const.value)) } - /** Usual target for `Annotation#toText`, overridden in RefinedPrinter */ - def annotText(annot: Annotation): Text = s"@${annot.symbol.name}" + /** Usual target for `Annotation#toText`, overridden in RefinedPrinter, which also + * looks at trees. + */ + override def annotText(annot: Annotation): Text = annotText(annot.symbol) + + protected def annotText(sym: Symbol): Text = s"@${sym.name}" def toText(annot: Annotation): Text = annot.toText(this) diff --git a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala index 1e58268c2e38..30934b615649 100644 --- a/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala +++ b/compiler/src/dotty/tools/dotc/printing/RefinedPrinter.scala @@ -1140,6 +1140,8 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { /** Textual representation of an instance creation expression without the leading `new` */ protected def constrText(tree: untpd.Tree): Text = toTextLocal(tree).stripPrefix(keywordStr("new ")) // DD + override def annotText(annot: Annotation): Text = annotText(annot.symbol, annot.tree) + protected def annotText(sym: Symbol, tree: untpd.Tree): Text = def recur(t: untpd.Tree): Text = t match case Apply(fn, Nil) => recur(fn) @@ -1152,9 +1154,12 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { case New(tpt) => recur(tpt) case _ => val annotSym = sym.orElse(tree.symbol.enclosingClass) - s"@${if annotSym.exists then annotSym.name.toString else t.show}" + if annotSym.exists then annotText(annotSym) else s"@${t.show}" recur(tree) + protected override def annotText(sym: Symbol): Text = + if sym == defn.ConsumeAnnot then "consume" else super.annotText(sym) + protected def modText(mods: untpd.Modifiers, sym: Symbol, kw: String, isType: Boolean): Text = { // DD val suppressKw = if (enclDefIsClass) mods.isAllOf(LocalParam) else mods.is(Param) var flagMask = @@ -1175,8 +1180,6 @@ class RefinedPrinter(_ctx: Context) extends PlainPrinter(_ctx) { Text(annotTexts, " ") ~~ flagsText ~~ (Str(kw) provided !suppressKw) } - override def annotText(annot: Annotation): Text = annotText(annot.symbol, annot.tree) - def optText(name: Name)(encl: Text => Text): Text = if (name.isEmpty) "" else encl(toText(name)) diff --git a/compiler/src/dotty/tools/dotc/typer/Namer.scala b/compiler/src/dotty/tools/dotc/typer/Namer.scala index e86414cc2183..4e74b558b5db 100644 --- a/compiler/src/dotty/tools/dotc/typer/Namer.scala +++ b/compiler/src/dotty/tools/dotc/typer/Namer.scala @@ -995,6 +995,10 @@ class Namer { typer: Typer => end if } + private def normalizeFlags(denot: SymDenotation)(using Context): Unit = + if denot.is(Method) && denot.hasAnnotation(defn.ConsumeAnnot) then + denot.setFlag(Mutable) + /** Intentionally left without `using Context` parameter. We need * to pick up the context at the point where the completer was created. */ @@ -1004,6 +1008,7 @@ class Namer { typer: Typer => addInlineInfo(sym) denot.info = typeSig(sym) invalidateIfClashingSynthetic(denot) + normalizeFlags(denot) Checking.checkWellFormed(sym) denot.info = avoidPrivateLeaks(sym) } diff --git a/docs/_docs/internals/exclusive-capabilities.md b/docs/_docs/internals/exclusive-capabilities.md index 938eb5ccdd55..07d3de3f124a 100644 --- a/docs/_docs/internals/exclusive-capabilities.md +++ b/docs/_docs/internals/exclusive-capabilities.md @@ -6,21 +6,19 @@ Language design draft ## Capability Kinds A capability is called - - _exclusive_ if it is `cap` or it has an exclusive capability in its capture set. - - _shared_ otherwise. - -There is a new top capability `shared` which can be used as a capability for deriving shared capture sets. Other shared capabilities are created as read-only versions of exclusive capabilities. + - _shared_ if it is classified as a `SharedCapability` + - _exclusive_ otherwise. ## Update Methods We introduce a new trait ```scala -trait Mutable +trait Mutable extends ExclusiveCapability, Classifier ``` It is used as a base trait for types that define _update methods_ using a new soft modifier `update`. -`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters. +`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters. **Example:** ```scala @@ -115,11 +113,6 @@ a method that accesses exclusive capabilities. If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated, shared _read-only_ capability. -`shared` can be understood as the read-only capability corresponding to `cap`. -```scala - shared = cap.rd -``` - A _top capability_ is either `cap` or `shared`. @@ -134,7 +127,7 @@ The meaning of `^` and `=>` is the same as before: **Implicitly added capture sets** -A reference to a type extending any of the traits `Capability` or `Mutable` gets an implicit capture set `{shared}` in case no explicit capture set is given. +A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. For instance, a matrix multiplication method can be expressed as follows: @@ -148,7 +141,7 @@ def mul(a: Matrix, b: Matrix, c: Matrix^): Unit = ``` Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read: ```scala -def mul(a: Matrix^{shared}, b: Matrix^{shared}, c: Matrix^{cap}): Unit +def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit ``` Separation checking will then make sure that `a` and `b` must be different from `c`. @@ -173,8 +166,6 @@ The read-only function `ro` maps capture sets to read-only capture sets. It is d - `ro(x) = x` if `x` is shared - `ro(x) = x.rd` if `x` is exclusive - - ## Subcapturing Subcapturing has to take the mode of capture sets into account. We let `m` stand for arbitrary modes. @@ -271,7 +262,7 @@ A reference `p.m` to an update method or class `m` of a mutable type is allowed If `e` is an expression of a type `T^cs` extending `Mutable` and the expected type is a value type that is not a mutable type, then the type of `e` is mapped to `T^ro(cs)`. - + + +To integrate exception and capture checking, only two changes are needed: + + - `CanThrow` is declared as a class extending `Control`, so all references to `CanThrow` instances are tracked. + - Escape checking is extended to `try` expressions. The result type of a `try` is not allowed to + capture capabilities defined in the body of the `try`. diff --git a/docs/_docs/reference/experimental/capture-checking/classes.md b/docs/_docs/reference/experimental/capture-checking/classes.md new file mode 100644 index 000000000000..9f9269915233 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/classes.md @@ -0,0 +1,233 @@ +--- +layout: doc-page +title: "Capture Checking of Classes" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/classes.html +--- + +## Introduction + +The principles for capture checking closures also apply to classes. For instance, consider: +```scala +class Logger(using fs: FileSystem): + def log(s: String): Unit = ... summon[FileSystem] ... + +def test(xfs: FileSystem): Logger^{xfs} = + Logger(xfs) +``` +Here, class `Logger` retains the capability `fs` as a (private) field. Hence, the result +of `test` is of type `Logger^{xfs}` + +Sometimes, a tracked capability is meant to be used only in the constructor of a class, but +is not intended to be retained as a field. This fact can be communicated to the capture +checker by declaring the parameter as `@constructorOnly`. Example: +```scala +import annotation.constructorOnly + +class NullLogger(using @constructorOnly fs: FileSystem): + ... +def test2(using fs: FileSystem): NullLogger = NullLogger() // OK +``` + +The captured references of a class include _local capabilities_ and _argument capabilities_. Local capabilities are capabilities defined outside the class and referenced from its body. Argument capabilities are passed as parameters to the primary constructor of the class. Local capabilities are inherited: +the local capabilities of a superclass are also local capabilities of its subclasses. Example: + +```scala +class Cap extends caps.SharedCapability + +def test(a: Cap, b: Cap, c: Cap) = + class Super(y: Cap): + def f = a + class Sub(x: Cap) extends Super(x) + def g = b + Sub(c) +``` +Here class `Super` has local capability `a`, which gets inherited by class +`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence, +the capture set of that call is `{a, b, c}`. + +The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one: +```scala +class C: + self: D^{a, b} => ... +``` +The inference observes the following constraints: + + - The type of `this` of a class `C` includes all captured references of `C`. + - The type of `this` of a class `C` is a subtype of the type of `this` + of each parent class of `C`. + - The type of `this` must observe all constraints where `this` is used. + +For instance, in +```scala +class Cap extends caps.SharedCapability +def test(c: Cap) = + class A: + val x: A = this + def f = println(c) // error +``` +we know that the type of `this` must be pure, since `this` is the right hand side of a `val` with type `A`. However, in the last line we find that the capture set of the class, and with it the capture set of `this`, would include `c`. This leads to a contradiction, and hence to a checking error: +``` + | def f = println(c) // error + | ^ + | reference (c : Cap) is not included in the allowed capture set {} + | of the enclosing class A +``` + +## Capture Tunnelling + +Consider the following simple definition of a `Pair` class: +```scala +class Pair[+A, +B](x: A, y: B): + def fst: A = x + def snd: B = y +``` +What happens if `Pair` is instantiated like this (assuming `ct` and `fs` are two capabilities in scope)? +```scala +def x: Int ->{ct} String +def y: Logger^{fs} +def p = Pair(x, y) +``` +The last line will be typed as follows: +```scala +def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y) +``` +This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside? + +The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the +capture is not propagated beyond this point. On the other hand, if the type variable is instantiated +again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g. +```scala +() => p.fst : () -> Int ->{ct} String +``` +In other words, references to capabilities "tunnel through" in generic instantiations from creation to access; they do not affect the capture set of the enclosing generic data constructor applications. +This principle plays an important part in making capture checking concise and practical. + + +## A Larger Example + +As a larger example, we present an implementation of lazy lists and some use cases. For simplicity, +our lists are lazy only in their tail part. This corresponds to what the Scala-2 type `Stream` did, whereas Scala 3's `LazyList` type computes strictly less since it is also lazy in the first argument. + +Here is the base trait `LzyList` for our version of lazy lists: +```scala +trait LzyList[+A]: + def isEmpty: Boolean + def head: A + def tail: LzyList[A]^{this} +``` +Note that `tail` carries a capture annotation. It says that the tail of a lazy list can +potentially capture the same references as the lazy list as a whole. + +The empty case of a `LzyList` is written as usual: +```scala +object LzyNil extends LzyList[Nothing]: + def isEmpty = true + def head = ??? + def tail = ??? +``` +Here is a formulation of the class for lazy cons nodes: +```scala +import scala.compiletime.uninitialized + +final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: + private var forced = false + private var cache: LzyList[A]^{this} = uninitialized + private def force = + if !forced then { cache = tl(); forced = true } + cache + + def isEmpty = false + def head = hd + def tail: LzyList[A]^{this} = force +end LzyCons +``` +The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function +returning a `LzyList`. Both the function and its result can capture arbitrary capabilities. +The result of applying the function is memoized after the first dereference of `tail` in +the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets. + +Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous +to `::` but instead of a strict list it produces a lazy list without evaluating its right operand. +```scala +extension [A](x: A) + def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} = + LzyCons(x, () => xs1) +``` +Note that `#:` takes an impure call-by-name parameter `xs1` as its right argument. The result +of `#:` is a lazy list that captures that argument. + +As an example usage of `#:`, here is a method `tabulate` that creates a lazy list +of given length with a generator function `gen`. The generator function is allowed +to have side effects. +```scala +def tabulate[A](n: Int)(gen: Int => A): LzyList[A]^{gen} = + def recur(i: Int): LzyList[A]^{gen} = + if i == n then LzyNil + else gen(i) #: recur(i + 1) + recur(0) +``` +Here is a use of `tabulate`: +```scala +class LimitExceeded extends Exception +def squares(n: Int)(using ct: CanThrow[LimitExceeded]) = + tabulate(10): i => + if i > 9 then throw LimitExceeded() + i * i +``` +The inferred result type of `squares` is `LzyList[Int]^{ct}`, i.e it is a lazy list of +`Int`s that can throw the `LimitExceeded` exception when it is elaborated by calling `tail` +one or more times. + +Here are some further extension methods for mapping, filtering, and concatenating lazy lists: +```scala +extension [A](xs: LzyList[A]^) + def map[B](f: A => B): LzyList[B]^{xs, f} = + if xs.isEmpty then LzyNil + else f(xs.head) #: xs.tail.map(f) + + def filter(p: A => Boolean): LzyList[A]^{xs, p} = + if xs.isEmpty then LzyNil + else if p(xs.head) then xs.head #: xs.tail.filter(p) + else xs.tail.filter(p) + + def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} = + if xs.isEmpty then ys + else xs.head #: xs.tail.concat(ys) + + def drop(n: Int): LzyList[A]^{xs} = + if n == 0 then xs else xs.tail.drop(n - 1) +``` +Their capture annotations are all as one would expect: + + - Mapping a lazy list produces a lazy list that captures the original list as well + as the (possibly impure) mapping function. + - Filtering a lazy list produces a lazy list that captures the original list as well + as the (possibly impure) filtering predicate. + - Concatenating two lazy lists produces a lazy list that captures both arguments. + - Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful. + +Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function +argument will _not_ show up in the result type of `map` or `filter`. For instance: +```scala +val xs = squares(10) +val ys: LzyList[Int]^{xs} = xs.map(_ + 1) +``` +The type of the mapped list `ys` has only `xs` in its capture set. The actual function +argument does not show up since it is pure. Likewise, if the lazy list +`xs` was pure, it would not show up in any of the method results. +This demonstrates that capability-based +effect systems with capture checking are naturally _effect polymorphic_. + +This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since +these elements are represented by a type variable. This means we don't need to annotate anything there either. + +Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this: +```scala +extension [A](xs: LzyList[A]) + def map[B](f: A -> B): LzyList[B] = ... +``` +That variant would not require any capture annotations either. + +To summarize, there are two "sweet spots" of data structure design: strict lists in +side-effecting or resource-aware code and lazy lists in purely functional code. +Both are already correctly capture-typed without requiring any explicit annotations. Capture annotations only come into play where the semantics gets more complicated because we deal with delayed effects such as in impure lazy lists or side-effecting iterators over strict lists. This property is probably one of the greatest plus points of our approach to capture checking compared to previous techniques which tend to be more noisy. diff --git a/docs/_docs/reference/experimental/capture-checking/classifiers.md b/docs/_docs/reference/experimental/capture-checking/classifiers.md new file mode 100644 index 000000000000..bbba42c37da9 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/classifiers.md @@ -0,0 +1,109 @@ +--- +layout: doc-page +title: "Capability Classifiers" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/classifiers.html +--- + +## Introduction + +Capabilities are extremely versatile. They can express concepts from many different domains. Exceptions, continuations, I/O, mutation, information flow, security permissions, are just some examples, the list goes on. + +Sometimes it is important to restrict, or: _classify_ what kind of capabilities are expected or returned in a context. For instance, we might want to allow only control capabilities such as `CanThrow`s or boundary `Label`s but no +other capabilities. Or might want to allow mutation, but no other side effects. This is achieved by having a capability class extend a _classifier_. + +For instance, the `scala.caps` package defines a classifier trait called `Control`, +like this: +```scala + trait Control extends SharedCapability, Classifier +``` +The [Gears library](https://lampepfl.github.io/gears/) then defines a capability class `Async` which extends `Control`. + +```scala + trait Async extends Control +``` +Unlike normal inheritance, classifiers also restrict the capture set of a capability. For instance, say we have a function +```scala + def f(using async: Async^) = body +``` +(the `^` is as usual redundant here since `Async` is a capability trait). +Then we have the guarantee that any actual `async` argument can only capture +capabilities that have types extending `Control`. No other capabilities such as mutation or I/O are allowed. + +A class or trait becomes a classifier by extending directly the marker trait +`caps.Classifier`. So with the definitions above, `Control` is a classifier trait, but `Async` is not, since it extends `Classifier` only indirectly, through `Control`. + +Classifiers are unique: a class cannot extend directly or transitively at the same time two unrelated classifier traits. So if a class transitively extends two classifier traits `C1` and `C2` then one of them must be a subtrait of the other. + +### Predefined Classifiers + +The `caps` object defines the `Classifier` trait itself and some traits that extend it: +```scala +trait Classifier + +sealed trait Capability + +trait SharedCapability extends Capability Classifier +trait Control extends SharedCapability, Classifier + +trait ExclusiveCapability extends Capability, Classifier +trait Mutable extends ExclusiveCapability, Classifier +``` +Here is a graph showing the hierarchy of predefined classifier traits: +``` + Capability + / \ + / \ + / \ + / \ + SharedCapability ExclusiveCapability + | | + | | + | | + | | + Control Mutable +``` +At the top of the hierarchy, we distinguish between _shared_ and _exclusive_ capabilities in two classifier traits `SharedCapability` and `ExclusiveCapability`. All capability classes we have seen so far are shared. +`ExclusiveCapability` is a base trait for capabilities that allow only un-aliased access to the data they represent, with the rules governed by [separation checking](separation-checking.md). Separation checking is currently an optional extension of capture checking, enabled by a different language import. Since `Capability` is a sealed trait, all capability classes are either shared or exclusive. + +`Control` capabilities are shared. This means they cannot directly or indirectly capture exclusive capabilities such as capabilities that control access to mutable state. Typical `Control` capabilities are: + + - `Label`s that enable to return from a `boundary`, + - `CanThrow` capabilities that enable throwing exceptions, or + - `Async` capabilities that allow to suspend. + +These are all expressed by having their capability classes extend `Control`. + +### Classifier Restriction + +Consider the following problem: The `Try.apply` method takes in its `body` parameter a computation, and runs it while catching any exceptions or `boundary.break` aborts. The exception or break will be re-issued when calling +the `get` method of a `Try` object. What should a capability-aware signature of `Try` be? + +The body passed to `Try.apply` can have arbitrary effects, so it can retain arbitrary capabilities. Yet the resulting `Try` object will retain only those capabilities of `body` which are classified as `Control`. So the signature of `Try.apply` should look like this: +```scala +object Try: + def apply[T](body: => T): Try[T]^{body.only[Control]} +``` +Note a new form of capability in the result's capture set: `body.only[Control]`. This is called a _restricted capability_. The general form of a restricted capability is +`c.only[A]` where + + - `c` is a regular, unrestricted capability + - `A` is a classifier trait. + + When substituting a capability set for the underlying capability, we drop all capabilities that are known to be unrelated to the classifier. For instance, say we have an actual body `{ expr }` that uses a capture set `{io, async}` where + + - `io` is an `IO` capability, where IO is assumed to extend `SharedCapability` but not `Control`. + - `async` is a `Control` capability. + +Then the result of `Try { expr }` would have type `Try^{async}`. We drop `io` since +`io`'s type is a `Capability` class that does not extend `Control`. + +If `expr` would use an additional capability `proc: () => Unit`, then `proc` would also show up in the result capture set. Since `proc` is fully effect-polymorphic, we can't exclude that it retains `Control` capabilities, so we have to keep it in the restricted capture set. These elements are shown together in the following example: +```scala +class IO extends caps.SharedCapability +class Async extends caps.Control + +def test(io: IO, async: Async, proc: () => Unit) = + val r = Try: + // code accessing `io`, `async`, and `proc` and returning an `Int. + val _: Try[Int]^{async, proc} = r +``` diff --git a/docs/_docs/reference/experimental/capture-checking/how-to-use.md b/docs/_docs/reference/experimental/capture-checking/how-to-use.md new file mode 100644 index 000000000000..d08125dc3fc8 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/how-to-use.md @@ -0,0 +1,19 @@ +--- +layout: doc-page +title: "How to Use the Capture Checker" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/how-to-use.html +--- + +## Enabling Capture Checking + +TODO + +## Compilation Options + +The following options are relevant for capture checking. + + - **-Vprint:cc** Prints the program with capturing types as inferred by capture checking. + - **-Ycc-verbose** Prints capabilities and capturing types in more detail. + - **-Ycc-debug** Gives more detailed, implementation-oriented information about capture checking, as described in the next section. + + The implementation supporting capture checking with these options is currently in branch `cc-experiment` on dotty.epfl.ch. diff --git a/docs/_docs/reference/experimental/capture-checking/internals.md b/docs/_docs/reference/experimental/capture-checking/internals.md new file mode 100644 index 000000000000..6aff9b208fd9 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/internals.md @@ -0,0 +1,84 @@ +--- +layout: doc-page +title: "Capture Checking Internals" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/internals.html +--- + +The capture checker is architected as a propagation constraint solver, which runs as a separate phase after type-checking and some initial transformations. + +Constraint variables stand for unknown capture sets. A constraint variable is introduced + + - for every part of a previously inferred type, + - for the accessed references of every method, class, anonymous function, or by-name argument, + - for the parameters passed in a class constructor call. + +Capture sets in explicitly written types are treated as constants (before capture checking, such sets are simply ignored). + +The capture checker essentially rechecks the program with the usual typing rules. Every time a subtype requirement between capturing types is checked, this translates to a subcapturing test on capture sets. If the two sets are constant, this is simply a yes/no question, where a no will produce an error message. + +If the lower set `C₁` of a comparison `C₁ <: C₂` is a variable, the set `C₂` is recorded +as a _superset_ of `C₁`. If the upper set `C₂` is a variable, the elements of `C₁` are _propagated_ to `C₂`. Propagation of an element `x` to a set `C` means that `x` is included as an element in `C`, and it is also propagated +to all known supersets of `C`. If such a superset is a constant, it is checked that `x` is included in it. If that's not the case, the original comparison `C₁ <: C₂` has no solution and an error is reported. + +The type checker also performs various maps on types, for instance when substituting actual argument types for formal parameter types in dependent functions, or mapping +member types with "as-seen-from" in a selection. Maps keep track of the variance +of positions in a type. The variance is initially covariant, it flips to +contravariant in function parameter positions, and can be either covariant, +contravariant, or nonvariant in type arguments, depending on the variance of +the type parameter. + +When capture checking, the same maps are also performed on capture sets. If a capture set is a constant, its elements (which are capabilities) are mapped as regular types. If the result of such a map is not a capability, the result is approximated according to the variance of the type. A covariant approximation replaces a type by its capture set. +A contravariant approximation replaces it with the empty capture set. A nonvariant +approximation replaces the enclosing capturing type with a range of possible types +that gets propagated and resolved further out. + +When a mapping `m` is performed on a capture set variable `C`, a new variable `Cm` is created that contains the mapped elements and that is linked with `C`. If `C` subsequently acquires further elements through propagation, these are also propagated to `Cm` after being transformed by the `m` mapping. `Cm` also gets the same supersets as `C`, mapped again using `m`. + +One interesting aspect of the capture checker concerns the implementation of capture tunnelling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunnelling explicit through so-called _box_ and +_unbox_ operations. Boxing hides a capture set and unboxing recovers it. The capture checker inserts virtual box and unbox operations based on actual and expected types similar to the way the type checker inserts implicit conversions. When capture set variables are first introduced, any capture set in a capturing type that is an instance of a type parameter instance is marked as "boxed". A boxing operation is +inserted if the expected type of an expression is a capturing type with +a boxed capture set variable. The effect of the insertion is that any references +to capabilities in the boxed expression are forgotten, which means that capture +propagation is stopped. Dually, if the actual type of an expression has +a boxed variable as capture set, an unbox operation is inserted, which adds all +elements of the capture set to the environment. + +Boxing and unboxing has no runtime effect, so the insertion of these operations is only simulated; the only visible effect is the retraction and insertion +of variables in the capture sets representing the environment of the currently checked expression. + +The `-Ycc-debug` option provides some insight into the workings of the capture checker. +When it is turned on, boxed sets are marked explicitly and capture set variables are printed with an ID and some information about their provenance. For instance, the string `{f, xs}33M5V` indicates a capture set +variable that is known to hold elements `f` and `xs`. The variable's ID is `33`. The `M` +indicates that the variable was created through a mapping from a variable with ID `5`. The latter is a regular variable, as indicated + by `V`. + +Generally, the string following the capture set consists of alternating numbers and letters where each number gives a variable ID and each letter gives the provenance of the variable. Possible letters are + + - `V` : a regular variable, + - `M` : a variable resulting from a _mapping_ of the variable indicated by the string to the right, + - `B` : similar to `M` but where the mapping is a _bijection_, + - `F` : a variable resulting from _filtering_ the elements of the variable indicated by the string to the right, + - `I` : a variable resulting from an _intersection_ of two capture sets, + - `D` : a variable resulting from the set _difference_ of two capture sets. + - `R` : a regular variable that _refines_ a class parameter, so that the capture + set of a constructor argument is known in the class instance type. + +At the end of a compilation run, `-Ycc-debug` will print all variable dependencies of variables referred to in previous output. Here is an example: +``` +Capture set dependencies: + {}2V :: + {}3V :: + {}4V :: + {f, xs}5V :: {f, xs}31M5V, {f, xs}32M5V + {f, xs}31M5V :: {xs, f} + {f, xs}32M5V :: +``` +This section lists all variables that appeared in previous diagnostics and their dependencies, recursively. For instance, we learn that + + - variables 2, 3, 4 are empty and have no dependencies, + - variable `5` has two dependencies: variables `31` and `32` which both result from mapping variable `5`, + - variable `31` has a constant fixed superset `{xs, f}` + - variable `32` has no dependencies. + + + diff --git a/docs/_docs/reference/experimental/capture-checking/polymorphism.md b/docs/_docs/reference/experimental/capture-checking/polymorphism.md new file mode 100644 index 000000000000..8853b54c82a2 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/polymorphism.md @@ -0,0 +1,92 @@ +--- +layout: doc-page +title: "Capability Polymorphism" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/polymorphism.html +--- + +## Introduction + +It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources +`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`: +```scala +class Source[X^]: + private var listeners: Set[Listener^{X}] = Set.empty + def register(x: Listener^{X}): Unit = + listeners += x + + def allListeners: Set[Listener^{X}] = listeners +``` +The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above +we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type +and assigns it to the variable. + +Capture-set variables `X^` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types. + +Under the hood, such capture-set variables are represented as regular type variables within the special interval + `>: CapSet <: CapSet^`. +For instance, `Source` from above could be equivalently +defined as follows: +```scala +class Source[X >: CapSet <: CapSet^]: + ... +``` +`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only +purpose is to identify type variables which are capture sets. In non-capture-checked +usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas +with capture checking enabled, it will take the annotated capture sets into account, +so that `CapSet^{a}` and `CapSet^{a,b}` are distinct. +This representation based on `CapSet` is subject to change and +its direct use is discouraged. + +Capture-set variables can be inferred like regular type variables. When they should be instantiated +explicitly one supplies a concrete capture set. For instance: +```scala +class Async extends caps.SharedCapability + +def listener(async: Async): Listener^{async} = ??? + +def test1(async1: Async, others: List[Async]) = + val src = Source[{async1, others*}] + ... +``` +Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows: +```scala + src.register(listener(async1)) + others.map(listener).foreach(src.register) + val ls: Set[Listener^{async, others*}] = src.allListeners +``` +A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating +effectful iterators: +```scala +class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): + def concat(it: IterableOnce[A]^): ConcatIterator[A, {C, it}]^{this, it} = + iterators ++= it // ^ + this // track contents of `it` in the result +``` +In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become +inaccessible after invoking its `concat` method. This is achieved with [mutation and separation tracking](separation-checking.md) which are currently in development. + +## Capability Members + +Just as parametrization by types can be equally expressed with type members, we could +also define the `Source[X^]` class above using a _capability member_: +```scala +class Source: + type X^ + private var listeners: Set[Listener^{this.X}] = Set.empty + ... // as before +``` +Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members, +capability members can be upper- and lower-bounded with capture sets: +```scala +trait Thread: + type Cap^ + def run(block: () ->{this.Cap} -> Unit): Unit + +trait GPUThread extends Thread: + type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap} +``` +Since `caps.cap` is the top element for subcapturing, we could have also left out the +upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`. + +**Advanced uses:** We discuss more advanced uses cases for capability members [here](advanced.md). diff --git a/docs/_docs/reference/experimental/capture-checking/scoped-caps.md b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md new file mode 100644 index 000000000000..b0296fb47b03 --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/scoped-caps.md @@ -0,0 +1,122 @@ +--- +layout: doc-page +title: "Scoped Caps" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/scoped-caps.html +--- + +## Scoped Universal Capabilities + +When discussing escape checking, we referred to a scoping discipline. That is, capture sets can contain only capabilities that are visible at the point where the set is defined. But that raises the question where a universal capability `cap` is defined? In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. Usually a `cap` refers to a universal capability defined in the scope where the `cap` appears. + +Special rules apply to `cap`s in method and function parameters and results. For example, take this method: + +```scala + def makeLogger(fs: FileSystem^): Logger^ = new Logger(fs) +``` +This creates a `Logger` that captures `fs`. +We could have been more specific in specifying `Logger^{fs}` as the return type of makeLogger, but the current definition is also valid, and might be preferable if we want to hide details what the returned logger captures. If we write it as above then certainly the implied `cap` in the return type of `Logger` should be able subsume the capability `fs`. This means that this `cap` has to be defined in a scope in which +`fs` is visible. + +In logic, the usual way to achieve this scoping is with an existential binder. We can express the type of `makeLogger` like this: +```scala +makeLogger: (fs: ∃cap₁.FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} +``` +In words: `makeLogger` takes a parameter `fs` of type `Filesystem` capturing _some_ universal capability `cap` and returns a `Logger` capturing some other (possibly different) universal `cap`. + +We can also turn the existential in the function parameter to a universal "forall" +in the function itself. In that alternative notation, the type of makeLogger would read like this: +```scala +makeLogger: ∀cap₁.(fs: FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂} +``` +There's a connection with [capture polymorphism](polymorphism.md) here. `cap`s in function parameters behave like additional +capture parameters that can be instantiated at the call site to arbitrary capabilities. + +The conventions for method types carry over to function types. A function type +```scala + (x: T) -> U^ +``` +is interpreted as having an existentially bound `cap` in the result, like this +```scala + (x: T) -> ∃cap.U^{cap} +``` +The same rules hold for the other kinds of function arrows, `=>`, `?->`, and `?=>`. So `cap` can in this case +subsume the function parameter `x` since it is locally bound in the function result. + +However, the expansion of `cap` into an existentially bound variable only applies to functions that use +the dependent function style syntax, with explicitly named parameters. Parametric functions such as +`A => B^` or `(A₍, ..., Aₖ) -> B^` don't bind their result cap in an existential quantifier. +For instance, the function +```scala + (x: A) -> B -> C^ +``` +is interpreted as +```scala + (x: A) -> ∃cap.B -> C^{cap} +``` +In other words, existential quantifiers are only inserted in results of function arrows that follow an explicitly named parameter list. + +To summarize: + + - If a function result type follows a named parameter list and contains covariant occurrences of `cap`, + we replace these occurrences with a fresh existential variable which + is bound by a quantifier scoping over the result type. + - If a function parameter type contains covariant occurrences of `cap`, we replace these occurrences with + a fresh existential variable scoping over the parameter type. + - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential in the + scope of the definition in which they appear. + +**Examples:** + + - `A => B` is an alias type that expands to `A ->{cap} B`, therefore + `(x: T) -> A => B` expands to `(x: T) -> ∃cap.(A ->{cap} B)`. + + - `(x: T) -> Iterator[A => B]` expands to `() -> ∃cap.Iterator[A ->{cap} B]` + + + \ No newline at end of file diff --git a/docs/_docs/reference/experimental/capture-checking/separation-checking.md b/docs/_docs/reference/experimental/capture-checking/separation-checking.md new file mode 100644 index 000000000000..6bb0fd3bf47c --- /dev/null +++ b/docs/_docs/reference/experimental/capture-checking/separation-checking.md @@ -0,0 +1,396 @@ +--- +layout: doc-page +title: "Separation Checking" +nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/capture-checking/separation-checking.html +--- + +## Introduction + +Separation checking is an extension of capture checking that enforces unique, un-aliased access to capabilities. It is enabled by a language import +```scala +import language.experimental.separationChecking +``` +(or the corresponding setting `-language:experimental.separationChecking`). +The import has to be given in addition to the `language.experimental.captureChecking` import that enables capture checking. +The reason for the second language import is that separation checking is less mature than capture checking proper, so we are less sure +we got the balance of safety and expressivity right for it at the present time. + +The purpose of separation checking is to ensure that certain accesses to capabilities are not aliased. As an example, consider matrix multiplication. A method that multiplies matrices `a`, and `b` into `c`, could be declared like this: +```scala +def multiply(a: Matrix, b: Matrix, c: Matrix): Unit +``` +But that signature alone does not tell us which matrices are supposed to be inputs and which one is the output. Nor does it guarantee that an input matrix is not re-used as the output, which would lead to wrong results. + +With separation checking, we can declare `Matrix` as a `Mutable` type, like this: +```scala +class Matrix(nrows: Int, ncols: Int) extends Mutable: + update def setElem(i: Int, j: Int, x: Double): Unit = ... + def getElem(i: Int, j: Int): Double = ... +``` +We further declare that the `setElem` method in a `Matrix` is an `update` method, which means it has a side effect. + +Separation checking gives a special interpretation to the following modified signature of `multiply`: +```scala +def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit +``` +In fact, only a single character was added: `c`'s type now carries a universal capability. This signature enforces at the same time two desirable properties: + + - Matrices `a`, and `b` are read-only; `multiply` will not call their update method. By contrast, the `c` matrix can be updated. + - Matrices `a` and `b` are different from matrix `c`, but `a` and `b` could refer to the same matrix. + +So, effectively, anything that can be updated must be unaliased. + + + +## Capability Kinds + +A capability is called + - _shared_ if it is [classified](../classifiers.md) as a `SharedCapability` + - _exclusive_ otherwise. + +## The Mutable Trait + +We introduce a new trait +```scala +trait Mutable extends ExclusiveCapability, Classifier +``` +It is used as a [classifier](../classifiers.md) trait for types that define _update methods_ using +a new soft modifier `update`. + +**Example:** +```scala +class Ref(init: Int) extends Mutable: + private var current = init + def get: Int = current + update def set(x: Int): Unit = current = x +``` +`update` can only be used in classes or objects extending `Mutable`. An update method is allowed to access exclusive capabilities in the method's environment. By contrast, a normal method in a type extending `Mutable` may access exclusive capabilities only if they are defined locally or passed to it in parameters. + +In class `Ref`, the `set` should be declared as an update method since it accesses the exclusive write capability of the variable `current` in its environment. + +`update` can also be used on an inner class of a class or object extending `Mutable`. It gives all code in the class the right +to access exclusive capabilities in the class environment. Normal classes +can only access exclusive capabilities defined in the class or passed to it in parameters. + +```scala +object Registry extends Mutable: + var count = 0 + update class Counter: + update def next: Int = + count += 1 + count +``` +Normal method members of `Mutable` classes cannot call update methods. This is indicated since accesses in the callee are recorded in the caller. So if the callee captures exclusive capabilities so does the caller. + +An update method cannot implement or override a normal method, whereas normal methods may implement or override update methods. Since methods such as `toString` or `==` inherited from Object are normal methods, it follows that none of these methods may be implemented as an update method. + +The `apply` method of a function type is also a normal method, hence `Mutable` classes may not implement a function type using an update method as the `apply` method. + +## Mutable Types + +A type is called a _mutable_ if it extends `Mutable` and it has an update method or an update class as non-private member or constructor. + +When we create an instance of a mutable type we always add `cap` to its capture set. For instance, if class `Ref` is declared as shown previously then `new Ref(1)` has type `Ref[Int]^`. + +**Restriction:** A non-mutable type cannot be downcast by a pattern match to a mutable type. + +**Definition:** A class is _read_only_ if the following conditions are met: + + 1. It does not extend any exclusive capabilities from its environment. + 2. It does not take parameters with exclusive capabilities. + 3. It does not contain mutable fields, or fields that take exclusive capabilities. + +**Restriction:** If a class or trait extends `Mutable` all its parent classes or traits must either extend `Mutable` or be read-only. + +The idea is that when we upcast a reference to a type extending `Mutable` to a type that does not extend `Mutable`, we cannot possibly call a method on this reference that uses an exclusive capability. Indeed, by the previous restriction this class must be a read-only class, which means that none of the code implemented +in the class can access exclusive capabilities on its own. And we +also cannot override any of the methods of this class with a method +accessing exclusive capabilities, since such a method would have +to be an update method and update methods are not allowed to override regular methods. + + + +**Example:** + +Consider trait `IterableOnce` from the standard library. + +```scala +trait IterableOnce[+T] extends Mutable: + def iterator: Iterator[T]^{this} + update def foreach(op: T => Unit): Unit + update def exists(op: T => Boolean): Boolean + ... +``` +The trait is a mutable type with many update methods, among them `foreach` and `exists`. These need to be classified as `update` because their implementation in the subtrait `Iterator` uses the update method `next`. +```scala +trait Iterator[T] extends IterableOnce[T]: + def iterator = this + def hasNext: Boolean + update def next(): T + update def foreach(op: T => Unit): Unit = ... + update def exists(op; T => Boolean): Boolean = ... + ... +``` +But there are other implementations of `IterableOnce` that are not mutable types (even though they do indirectly extend the `Mutable` trait). Notably, collection classes implement `IterableOnce` by creating a fresh +`iterator` each time one is required. The mutation via `next()` is then restricted to the state of that iterator, whereas the underlying collection is unaffected. These implementations would implement each `update` method in `IterableOnce` by a normal method without the `update` modifier. + +```scala +trait Iterable[T] extends IterableOnce[T]: + def iterator = new Iterator[T] { ... } + def foreach(op: T => Unit) = iterator.foreach(op) + def exists(op: T => Boolean) = iterator.exists(op) +``` +Here, `Iterable` is not a mutable type since it has no update method as member. +All inherited update methods are (re-)implemented by normal methods. + +**Note:** One might think that we don't need a base trait `Mutable` since in any case +a mutable type is defined by the presence of update methods, not by what it extends. In fact the importance of `Mutable` is that it defines _the other methods_ as read-only methods that _cannot_ access exclusive capabilities. For types not extending `Mutable`, this is not the case. For instance, the `apply` method of a function type is not an update method and the type itself does not extend `Mutable`. But `apply` may well be implemented by +a method that accesses exclusive capabilities. + +## Read-only Capabilities + +If `x` is an exclusive capability of a type extending `Mutable`, `x.rd` is its associated _read-only_ capability. It counts as a shared capability. A read-only capability does not permit access to the mutable fields of a matrix. + +A read-only capability can be seen as a classified capability +using a classifier trait `Read` that extends `Mutable`. I.e. +`x.rd` can be seen as being essentially the same as `x.only[Read]`. +(Currently, this precise equivalence is still waiting to be implemented.) + +**Implicitly added capture sets** + +A reference to a type extending trait `Mutable` gets an implicit capture set `{cap.rd}` provided no explicit capture set is given. This is different from +other capability traits which implicitly add `{cap}`. + +For instance, consider the matrix multiplication method mentioned previously: +```scala +def multiply(a: Matrix, b: Matrix, c: Matrix^): Unit +``` +Here, `a` and `b` are implicitly read-only, and `c`'s type has capture set `cap`. I.e. with explicit capture sets this would read: +```scala +def mul(a: Matrix^{cap.rd}, b: Matrix^{cap.rd}, c: Matrix^{cap}): Unit +``` +Separation checking will then make sure that `a` and `b` must be different from `c`. + +## Accesses to Mutable Types + +An access `p.m` to an update method or class `m` in a mutable type is permitted only if the type `M` of the prefix `p` retains exclusive capabilities. If `M` is pure or its capture set has only shared +capabilities then the access is not permitted. + +A _read-only access_ is a reference `x` to a type extending `Mutable` that is either + + - widened to a value type that is not a mutable type, or + - immediately followed by a selection with a member that is a normal method or class (not an update method or class). + +A read-only access charges the read-only capability `x.rd` to its environment. Other accesses charge the full capability `x`. + +**Example:** + +Consider a reference `x` and two closures `f` and `g`. + +```scala +val x = Ref(1) +val f = () => x.get // f: () ->{x.rd} Unit +val g = () => x.set(1) // g: () ->{x} Unit +``` + +`f` accesses a regular method, so it charges only `x.rd` to its environment which shows up in its capture set. By contrast, `g` +accesses an update method of `x`, so its capture set is `{x}`. + +A reference to a mutable type with an exclusive capture set can be widened to a reference with a read-only set. For instance, the following is OK: +```scala +val a: Ref^ = Ref(1) +val b1: Ref^{a.rd} = a +val b2: Ref^{cap.rd} = a +``` + +## Read-Only Capsets + +If we consider subtyping and subcapturing, we observe what looks like a contradiction: `x.rd` is seen as a restricted capability, so `{x.rd}` should subcapture `{x}`. Yet, we have seen in the example above that sometimes it goes the other way: `a`'s capture set is either `{a}` or `{cap}`, yet `a` can be used to define `b1` and `b2`, with capture sets `{a.rd}` and `{cap.rd}`, respectively. + +The contradiction can be explained by noting that we use a capture set in two different roles. + +First, and as always, a capture set defines _retained capabilities_ that may or may be not used by a value. More capabilities give larger types, and the empty capture set is the smallest set according to that ordering. That makes sense: If a higher-order function like `map` is willing to accept a function `A => B` that can have arbitrary effects it's certainly OK to pass a pure function of type `A -> B` to it. + +But for mutations, we use a capture set in a second role, in which it defines a set of _access permissions_. If we have a `Ref^`, we can access all its methods, but if we have a `Ref^{cap.rd}`, we can access only regular methods, not update methods. From that viewpoint a mutable type with exclusive capabilities lets you do more than a mutable type with just read-only capabilities. So by the Liskov substitution principle, sets with exclusive capabilities subcapture sets with only read-only capabilities. + +The contradiction can be solved by distinguishing these two roles. For access permissions, we express read-only sets with an additional _qualifier_ `RD`. That qualifier is used only in the formal theory and the implementation, it currently cannot be expressed in source. +We add an implicit read-only qualifier `RD` to all capture sets on mutable types that consist only of shared or read-only capabilities. +So when we write +```scala +val b1: Ref^{a.rd} = a +``` +we really mean +```scala +val b1: Ref^{a.rd}.RD = a +``` + +The subcapturing theory for sets is then as before, with the following additional rules: + + - `C <: C.RD` + - `C₁.RD <: C₂.RD` if `C₍ <: C₂` + - `{x, ...}.RD = {x.rd, ...}.RD` + - `{x.rd, ...} <: {x, ...}` + +## Separation Checking + +The idea behind separation checking is simple: We now interpret each occurrence of `cap` as a separate top capability. This includes derived syntaxes like `A^` and `B => C`. We further keep track during capture checking which capabilities are subsumed by each `cap`. If capture checking widens a capability `x` to a top capability `capᵢ`, we say `x` is _hidden_ by `capᵢ`. The rule then is that any capability hidden by a top capability `capᵢ` cannot be referenced independently or hidden in another `capⱼ` in code that can see `capᵢ`. + +Here's an example: +```scala +val x: C^ = y + ... x ... // ok + ... y ... // error +``` +This principle ensures that capabilities such as `x` that have `cap` as underlying capture set are un-aliased or "fresh". Any previously existing aliases such as `y` in the code above are inaccessible as long as `x` is also visible. + +Separation checking applies only to exclusive capabilities and their read-only versions. Any capability extending `SharedCapability` in its type is exempted; the following definitions and rules do not apply to them. + +**Definitions:** + + - The _transitive capture set_ `tcs(c)` of a capability `c` with underlying capture set `C` is `c` itself, plus the transitive capture set of `C`. + + - The _transitive capture set_ `tcs(C)` of a capture set C is the union + of `tcs(c)` for all elements `c` of `C`. + + - Two capture sets _interfere_ if one contains an exclusive capability `x` and the other also contains `x` or contains the read-only capability `x.rd`. Conversely, two capture sets are _separated_ if their transitive capture sets don't interfere. + +Separation checks are applied in the following scenarios: + +### Checking Applications + +When checking a function application `f(e_1, ..., e_n)`, we instantiate each `cap` in a formal parameter of `f` to a fresh top capability and compare the argument types with these instantiated parameter types. We then check that the hidden set of each instantiated top capability for an argument `eᵢ` is separated from the capture sets of all the other arguments as well as from the capture sets of the function prefix and the function result. For instance a +call to +```scala +multiply(a, b, a) +``` +would be rejected since `a` appears in the hidden set of the last parameter of multiply, which has type `Matrix^` and also appears in the capture set of the +first parameter. + +We do not report a separation error between two sets if a formal parameter's capture set explicitly names a conflicting parameter. For instance, consider a method `seq` to apply two effectful function arguments in sequence. It can be declared as follows: +```scala +def seq(f: () => Unit; g: () ->{cap, f} Unit): Unit = + f(); g() +``` +Here, the `g` parameter explicitly mentions `f` in its potential capture set. This means that the `cap` in the same capture set would not need to hide the first argument, since it already appears explicitly in the same set. Consequently, we can pass the same function twice to `compose` without violating the separation criteria: +```scala +val r = Ref(1) +val plusOne = r.set(r.get + 1) +seq(plusOne, plusOne) +``` +Without the explicit mention of parameter `f` in the capture set of parameter `g` of `seq` we'd get a separation error, since the transitive capture sets of both arguments contain `r` and are therefore not separated. + +### Checking Statement Sequences + +When a capability `x` is used at some point in a statement sequence, we check that `{x}` is separated from the hidden sets of all previous definitions. + +Example: +```scala +val a: Ref^ = Ref(1) +val b: Ref^ = a +val x = a.get // error +``` +Here, the last line violates the separation criterion since it uses in `a.get` the capability `a`, which is hidden by the definition of `b`. +Note that this check only applies when there are explicit top capabilities in play. One could very well write +```scala +val a: Ref^ = Ref(1) +val b: Ref^{a} = a +val x = a.get // ok +``` +One can also drop the explicit type of `b` and leave it to be inferred. That would +not cause a separation error either. +```scala +val a: Ref^ = Ref(0 +val b = a +val x = a.get // ok +``` + +### Checking Types + +When a type contains top capabilities we check that their hidden sets don't interfere with other parts of the same type. + +Example: +```scala +val b: (Ref^, Ref^) = (a, a) // error +val c: (Ref^, Ref^{a}) = (a, a) // error +val d: (Ref^{a}, Ref^{a}) = (a, a) // ok +``` +Here, the definition of `b` is in error since the hidden sets of the two `^`s in its type both contain `a`. Likewise, the definition of `c` is in error since the hidden set of the `^` in its type contains `a`, which is also part of a capture set somewhere else in the type. On the other hand, the definition of `d` is legal since there are no hidden sets to check. + +### Checking Return Types + +When a `cap` appears in the return type of a function it means a "fresh" top capability, different from what is known at the call site. Separation checking makes sure this is the case. For instance, the following is OK: +```scala +def newRef(): Ref^ = Ref(1) +``` +And so is this: +```scala +def newRef(): Ref^ = + val a = Ref(1) + a +``` +But the next definitions would cause a separation error: +```scala +val a = Ref(1) +def newRef(): Ref^ = a // error +``` +The rule is that the hidden set of a fresh cap in a return type cannot reference exclusive or read-only capabilities defined outside of the function. What about parameters? Here's another illegal version: +```scala +def incr(a: Ref^): Ref^ = + a.set(a.get + 1) + a +``` +These needs to be rejected because otherwise we could have set up the following bad example: +```scala +val a = Ref(1) +val b: Ref^ = incr(a) +``` +Here, `b` aliases `a` but does not hide it. If we referred to `a` afterwards we would be surprised to see that the reference has now a value of 2. +Therefore, parameters cannot appear in the hidden sets of fresh result caps either, at least not in general. An exception to this rule is described in the next section. + +### Consume Parameters + +Returning parameters in fresh result caps is safe if the actual argument to the parameter is not used afterwards. We can signal and enforce this pattern by adding a `consume` modifier to a parameter. With that new soft modifier, the following variant of `incr` is legal: +```scala +def incr(consume a: Ref^): Ref^ = + a.set(a.get + 1) + a +``` +Here, we increment the value of a reference and then return the same reference while enforcing the condition that the original reference cannot be used afterwards. Then the following is legal: +```scala +val a1 = Ref(1) +val a2 = incr(a1) +val a3 = incr(a2) +println(a3) +``` +Each reference `aᵢ` is unused after it is passed to `incr`. But the following continuation of that sequence would be in error: +```scala +val a4 = println(a2) // error +val a5 = incr(a1) // error +``` +In both of these assignments we use a capability that was consumed in an argument +of a previous application. + +Consume parameters enforce linear access to resources. This can be very useful. As an example, consider Scala's buffers such as `ListBuffer` or `ArrayBuffer`. We can treat these buffers as if they were purely functional, if we can enforce linear access. + +For instance, we can define a function `linearAdd` that adds elements to buffers in-place without violating referential transparency: +```scala +def linearAdd[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ = + buf += elem +``` +`linearAdd` returns a fresh buffer resulting from appending `elem` to `buf`. It overwrites `buf`, but that's OK since the `consume` modifier on `buf` ensures that the argument is not used after the call. + +### Consume Methods + +Buffers in Scala's standard library use a single-argument method `+=` instead of a two argument global function like `linearAdd`. We can enforce linearity in this case by adding the `consume` modifier to the method itself. +```scala +class Buffer[T] extends Mutable: + consume def +=(x: T): Buffer[T]^ = this // ok +``` +`consume` on a method implies `update`, so there's no need to label `+=` separately as an update method. Then we can write +```scala +val b = Buffer[Int]() += 1 += 2 +val c = b += 3 +// b cannot be used from here +``` +This code is equivalent to functional append with `+`, and is at the same time more efficient since it re-uses the storage of the argument buffer. + diff --git a/docs/_docs/reference/experimental/cc.md b/docs/_docs/reference/experimental/cc.md deleted file mode 100644 index 0fdcf143ae72..000000000000 --- a/docs/_docs/reference/experimental/cc.md +++ /dev/null @@ -1,887 +0,0 @@ ---- -layout: doc-page -title: "Capture Checking" -nightlyOf: https://docs.scala-lang.org/scala3/reference/experimental/cc.html ---- - -Capture checking is a research project that modifies the Scala type system to track references to capabilities in values. It can be enabled by the language import -```scala -import language.experimental.captureChecking -``` -At present, capture checking is still highly experimental and unstable, and it evolves quickly. -Before trying it out, make sure you have the latest version of Scala. - -To get an idea what capture checking can do, let's start with a small example: -```scala -def usingLogFile[T](op: FileOutputStream => T): T = - val logFile = FileOutputStream("log") - val result = op(logFile) - logFile.close() - result -``` -The `usingLogFile` method invokes a given operation with a fresh log file as parameter. Once the operation has ended, the log file is closed and the -operation's result is returned. This is a typical _try-with-resources_ pattern, similar to many other such patterns which are often supported by special language constructs in other languages. - -The problem is that `usingLogFile`'s implementation is not entirely safe. One can -undermine it by passing an operation that performs the logging at some later point -after it has terminated. For instance: -```scala -val later = usingLogFile { file => () => file.write(0) } -later() // crash -``` -When `later` is executed it tries to write to a file that is already closed, which -results in an uncaught `IOException`. - -Capture checking gives us the mechanism to prevent such errors _statically_. To -prevent unsafe usages of `usingLogFile`, we can declare it like this: -```scala -def usingLogFile[T](op: FileOutputStream^ => T): T = - // same body as before -``` -The only thing that's changed is that the `FileOutputStream` parameter of `op` is now -followed by `^`. We'll see that this turns the parameter into a _capability_ whose lifetime is tracked. - -If we now try to define the problematic value `later`, we get a static error: -``` - | val later = usingLogFile { f => () => f.write(0) } - | ^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit - | Required: java.io.FileOutputStream^ => () ->'s3 Unit - | - | Note that capability f cannot be included in outer capture set 's3. -``` -In this case, it was easy to see that the `logFile` capability escapes in the closure passed to `usingLogFile`. But capture checking also works for more complex cases. -For instance, capture checking is able to distinguish between the following safe code: -```scala -val xs = usingLogFile { f => - List(1, 2, 3).map { x => f.write(x); x * x } -} -``` -and the following unsafe one: -```scala -val xs = usingLogFile { f => - LzyList(1, 2, 3).map { x => f.write(x); x * x } -} -``` -An error would be issued in the second case, but not the first one (this assumes a capture-aware -formulation `LzyList` of lazily evaluated lists, which we will present later in this page). - -It turns out that capture checking has very broad applications. Besides the various -try-with-resources patterns, it can also be a key part to the solutions of many other long standing problems in programming languages. Among them: - - - How to have a simple and flexible system for checked exceptions. We show later - how capture checking enables a clean and fully safe system for checked exceptions in Scala. - - How to address the problem of effect polymorphism in general. - - How to solve the "what color is your function?" problem of mixing synchronous - and asynchronous computations. - - How to do region-based allocation, safely, - - How to reason about capabilities associated with memory locations. - -The following sections explain in detail how capture checking works in Scala 3. - - -## Overview - -The capture checker extension introduces a new kind of types and it enforces some rules for working with these types. - -## Capabilities and Capturing Types - -Capture checking is done in terms of _capturing types_ of the form -`T^{c₁, ..., cᵢ}`. Here `T` is a type, and `{c₁, ..., cᵢ}` is a _capture set_ consisting of references to capabilities `c₁, ..., cᵢ`. - -An _object capability_ is syntactically a method- or class-parameter, a local variable, or the `this` of an enclosing class. The type of a capability -must be a capturing type with a non-empty capture set. We also say that -variables that are capabilities are _tracked_. - -In a sense, every -capability gets its authority from some other, more sweeping capability which it captures. The recursion stops with a _universal capability_, written `cap`, from which all other capabilities are ultimately derived. -If `T` is a type, then `T^` is a shorthand for `T^{cap}`, meaning `T` can capture arbitrary capabilities. - -Here is an example: -```scala -class FileSystem - -class Logger(fs: FileSystem^): - def log(s: String): Unit = ... // Write to a log file, using `fs` - -def test(fs: FileSystem^) = - val l: Logger^{fs} = Logger(fs) - l.log("hello world!") - val xs: LzyList[Int]^{l} = - LzyList.from(1) - .map { i => - l.log(s"computing elem # $i") - i * i - } - xs -``` -Here, the `test` method takes a `FileSystem` as a parameter. `fs` is a capability since its type has a non-empty capture set. The capability is passed to the `Logger` constructor -and retained as a field in class `Logger`. Hence, the local variable `l` has type -`Logger^{fs}`: it is a `Logger` which retains the `fs` capability. - -The second variable defined in `test` is `xs`, a lazy list that is obtained from -`LzyList.from(1)` by logging and mapping consecutive numbers. Since the list is lazy, -it needs to retain the reference to the logger `l` for its computations. Hence, the -type of the list is `LzyList[Int]^{l}`. On the other hand, since `xs` only logs but does -not do other file operations, it retains the `fs` capability only indirectly. That's why -`fs` does not show up in the capture set of `xs`. - -Capturing types come with a subtype relation where types with "smaller" capture sets are subtypes of types with larger sets (the _subcapturing_ relation is defined in more detail below). If a type `T` does not have a capture set, it is called _pure_, and is a subtype of -any capturing type that adds a capture set to `T`. - -## Function Types - -The usual function type `A => B` now stands for a function that can capture arbitrary capabilities. We call such functions -_impure_. By contrast, the new single arrow function type `A -> B` stands for a function that cannot capture any capabilities, or otherwise said, is _pure_. -One can add a capture set after the arrow of an otherwise pure function. -For instance, `A ->{c, d} B` would be a function that can capture capabilities `c` and `d`, but no others. -This type is a shorthand for `(A -> B)^{c, d}`, i.e. the function type `A -> B` with possible captures `{c, d}`. - -The impure function type `A => B` is treated as an alias for `A ->{cap} B`. That is, impure functions are functions that can capture anything. - -A capture annotation `^` binds more strongly than a function arrow. So -`A -> B^{c}` is read as `A -> (B^{c})` and `A -> B^` is read as `A -> (B^{cap})`. - -Analogous conventions apply to context function types. `A ?=> B` is an impure context function, with `A ?-> B` as its pure complement. - -**Note 1:** The identifiers `->` and `?->` are now treated as soft keywords when used as infix type operators. They are -still available as regular identifiers for terms. For instance, the mapping syntax `Map("x" -> 1, "y" -> 2)` is still supported since it only applies to terms. - -**Note 2:** The distinctions between pure vs impure function types do not apply to methods. In fact, since methods are not values they never capture anything directly. References to -capabilities in a method are instead counted in the capture set of the enclosing object. - -## By-Name Parameter Types - -A convention analogous to function types also extends to by-name parameters. In -```scala -def f(x: => Int): Int -``` -the actual argument can refer to arbitrary capabilities. So the following would be OK: -```scala -f(if p(y) then throw Ex() else 1) -``` -On the other hand, if `f` was defined like this -```scala -def f(x: -> Int): Int -``` -the actual argument to `f` could not refer to any capabilities, so the call above would be rejected. -One can also allow specific capabilities like this: -```scala -def f(x: ->{c} Int): Int -``` -Here, the actual argument to `f` is allowed to use the `c` capability but no others. - -## Subtyping and Subcapturing - -Capturing influences subtyping. As usual we write `T₁ <: T₂` to express that the type -`T₁` is a subtype of the type `T₂`, or equivalently, that `T₁` conforms to `T₂`. An -analogous _subcapturing_ relation applies to capture sets. If `C₁` and `C₂` are capture sets, we write `C₁ <: C₂` to express that `C₁` _is covered by_ `C₂`, or, swapping the operands, that `C₂` _covers_ `C₁`. - -Subtyping extends as follows to capturing types: - - - Pure types are subtypes of capturing types. That is, `T <: C T`, for any type `T`, capturing set `C`. - - For capturing types, smaller capturing sets produce subtypes: `C₁ T₁ <: C₂ T₂` if - `C₁ <: C₂` and `T₁ <: T₂`. - -A subcapturing relation `C₁ <: C₂` holds if `C₂` _accounts for_ every element `c` in `C₁`. This means one of the following three conditions must be true: - - - `c ∈ C₂`, - - `c` refers to a parameter of some class `Cls` and `C₂` contains `Cls.this`, - - `c`'s type has capturing set `C` and `C₂` accounts for every element of `C` (that is, `C <: C₂`). - - -**Example 1.** Given -```scala -fs: FileSystem^ -ct: CanThrow[Exception]^ -l : Logger^{fs} -``` -we have -``` -{l} <: {fs} <: {cap} -{fs} <: {fs, ct} <: {cap} -{ct} <: {fs, ct} <: {cap} -``` -The set consisting of the root capability `{cap}` covers every other capture set. This is -a consequence of the fact that, ultimately, every capability is created from `cap`. - -**Example 2.** Consider again the FileSystem/Logger example from before. `LzyList[Int]` is a proper subtype of `LzyList[Int]^{l}`. So if the `test` method in that example -was declared with a result type `LzyList[Int]`, we'd get a type error. Here is the error message: -``` -11 |def test(using fs: FileSystem^): LzyList[Int] = { - | ^ - | Found: LzyList[Int]^{fs} - | Required: LzyList[Int] -``` -Why does it say `LzyList[Int]^{fs}` and not `LzyList[Int]^{l}`, which is, after all, the type of the returned value `xs`? The reason is that `l` is a local variable in the body of `test`, so it cannot be referred to in a type outside that body. What happens instead is that the type is _widened_ to the smallest supertype that does not mention `l`. Since `l` has capture set `fs`, we have that `{fs}` covers `{l}`, and `{fs}` is acceptable in a result type of `test`, so `{fs}` is the result of that widening. -This widening is called _avoidance_; it is not specific to capture checking but applies to all variable references in Scala types. - -## Capability Classes - -Classes like `CanThrow` or `FileSystem` have the property that their values are always intended to be capabilities. We can make this intention explicit and save boilerplate by letting these classes extend the `Capability` class defined in object `cap`. - -The capture set of a `Capability` subclass type is always `{cap}`. This means we could equivalently express the `FileSystem` and `Logger` classes as follows: -```scala -import caps.Capability - -class FileSystem extends Capability - -class Logger(using FileSystem): - def log(s: String): Unit = ??? - -def test(using fs: FileSystem) = - val l: Logger^{fs} = Logger() - ... -``` -In this version, `FileSystem` is a capability class, which means that the `{cap}` capture set is implied on the parameters of `Logger` and `test`. Writing the capture set explicitly produces a warning: -```scala -class Logger(using FileSystem^{cap}): - ^^^^^^^^^^^^^^ - redundant capture: FileSystem already accounts for cap -``` -Another, unrelated change in the version of the last example here is that the `FileSystem` capability is now passed as an implicit parameter. It is quite natural to model capabilities with implicit parameters since it greatly reduces the wiring overhead once multiple capabilities are in play. - -## Capture Checking of Closures - -If a closure refers to capabilities in its body, it captures these capabilities in its type. For instance, consider: -```scala -def test(fs: FileSystem): String ->{fs} Unit = - (x: String) => Logger(fs).log(x) -``` -Here, the body of `test` is a lambda that refers to the capability `fs`, which means that `fs` is retained in the lambda. -Consequently, the type of the lambda is `String ->{fs} Unit`. - -**Note:** Function values are always written with `=>` (or `?=>` for context functions). There is no syntactic -distinction for pure _vs_ impure function values. The distinction is only made in their types. - -A closure also captures all capabilities that are captured by the functions -it calls. For instance, in -```scala -def test(fs: FileSystem) = - def f() = g() - def g() = (x: String) => Logger(fs).log(x) - f -``` -the result of `test` has type `String ->{fs} Unit` even though function `f` itself does not refer to `fs`. - -## Capture Checking of Classes - -The principles for capture checking closures also apply to classes. For instance, consider: -```scala -class Logger(using fs: FileSystem): - def log(s: String): Unit = ... summon[FileSystem] ... - -def test(xfs: FileSystem): Logger^{xfs} = - Logger(xfs) -``` -Here, class `Logger` retains the capability `fs` as a (private) field. Hence, the result -of `test` is of type `Logger^{xfs}` - -Sometimes, a tracked capability is meant to be used only in the constructor of a class, but -is not intended to be retained as a field. This fact can be communicated to the capture -checker by declaring the parameter as `@constructorOnly`. Example: -```scala -import annotation.constructorOnly - -class NullLogger(using @constructorOnly fs: FileSystem): - ... -def test2(using fs: FileSystem): NullLogger = NullLogger() // OK -``` - -The captured references of a class include _local capabilities_ and _argument capabilities_. Local capabilities are capabilities defined outside the class and referenced from its body. Argument capabilities are passed as parameters to the primary constructor of the class. Local capabilities are inherited: -the local capabilities of a superclass are also local capabilities of its subclasses. Example: - -```scala -class Cap extends caps.Capability - -def test(a: Cap, b: Cap, c: Cap) = - class Super(y: Cap): - def f = a - class Sub(x: Cap) extends Super(x) - def g = b - Sub(c) -``` -Here class `Super` has local capability `a`, which gets inherited by class -`Sub` and is combined with `Sub`'s own local capability `b`. Class `Sub` also has an argument capability corresponding to its parameter `x`. This capability gets instantiated to `c` in the final constructor call `Sub(c)`. Hence, -the capture set of that call is `{a, b, c}`. - -The capture set of the type of `this` of a class is inferred by the capture checker, unless the type is explicitly declared with a self type annotation like this one: -```scala -class C: - self: D^{a, b} => ... -``` -The inference observes the following constraints: - - - The type of `this` of a class `C` includes all captured references of `C`. - - The type of `this` of a class `C` is a subtype of the type of `this` - of each parent class of `C`. - - The type of `this` must observe all constraints where `this` is used. - -For instance, in -```scala -class Cap extends caps.Capability -def test(c: Cap) = - class A: - val x: A = this - def f = println(c) // error -``` -we know that the type of `this` must be pure, since `this` is the right hand side of a `val` with type `A`. However, in the last line we find that the capture set of the class, and with it the capture set of `this`, would include `c`. This leads to a contradiction, and hence to a checking error: -``` -16 | def f = println(c) // error - | ^ - |(c : Cap) cannot be referenced here; it is not included in the allowed capture set {} -``` - -## Capture Tunnelling - -Consider the following simple definition of a `Pair` class: -```scala -class Pair[+A, +B](x: A, y: B): - def fst: A = x - def snd: B = y -``` -What happens if `Pair` is instantiated like this (assuming `ct` and `fs` are two capabilities in scope)? -```scala -def x: Int ->{ct} String -def y: Logger^{fs} -def p = Pair(x, y) -``` -The last line will be typed as follows: -```scala -def p: Pair[Int ->{ct} String, Logger^{fs}] = Pair(x, y) -``` -This might seem surprising. The `Pair(x, y)` value does capture capabilities `ct` and `fs`. Why don't they show up in its type at the outside? - -The answer is capture tunnelling. Once a type variable is instantiated to a capturing type, the -capture is not propagated beyond this point. On the other hand, if the type variable is instantiated -again on access, the capture information "pops out" again. For instance, even though `p` is technically pure because its capture set is empty, writing `p.fst` would record a reference to the captured capability `ct`. So if this access was put in a closure, the capability would again form part of the outer capture set. E.g. -```scala -() => p.fst : () -> Int ->{ct} String -``` -In other words, references to capabilities "tunnel through" in generic instantiations from creation to access; they do not affect the capture set of the enclosing generic data constructor applications. -This principle plays an important part in making capture checking concise and practical. - -## Escape Checking - - -Capabilities follow the usual scoping discipline, which means that capture sets -can contain only capabilities that are visible at the point where the set is defined. - -We now reconstruct how this principle produced the error in the introductory example, where -`usingLogFile` was declared like this: -```scala -def usingLogFile[T](op: FileOutputStream^ => T): T = ... -``` -The error message was: -``` - | val later = usingLogFile { f => () => f.write(0) } - | ^^^^^^^^^^^^^^^^^^^^^^^^^ - | Found: (f: java.io.FileOutputStream^'s1) ->'s2 () ->{f} Unit - | Required: java.io.FileOutputStream^ => () ->'s3 Unit - | - | Note that capability f cannot be included in outer capture set 's3. -``` -This error message was produced by the following logic: - - - The `f` parameter has type `FileOutputStream^`, which makes it a capability. - - Therefore, the type of the expression `() => f.write(0)` is `() ->{f} Unit`. - - This makes the type of the whole closure passed to `usingLogFile` the dependent function type - `(f: FileOutputStream^'s1) ->'s2 () ->{f} Unit`, - for some as yet uncomputed capture sets `'s1` and `'s2`. - - The expected type of the closure is a simple, parametric, impure function type `FileOutputStream^ => T`, - for some instantiation of the type variable `T`. - - Matching with the found type, `T` must have the shape `() ->'s3 Unit`, for - some capture set `'s3` defined at the level of value `later`. - - That capture set cannot include the capability `f` since `f` is locally bound. - This causes the error. - -An analogous restriction applies to the type of a mutable variable. -Another way one could try to undermine capture checking would be to -assign a closure with a local capability to a global variable. Maybe -like this: -```scala -var loophole: () => Unit = () => () -usingLogFile { f => - loophole = () => f.write(0) -} -loophole() -``` -But this will not compile either, since the capture set of the mutable variable `loophole` cannot refer to variable `f`, which is not visible -where `loophole` is defined. - -Looking at object graphs, we observe a monotonicity property: The capture set of an object `x` covers the capture sets of all objects reachable through `x`. This property is reflected in the type system by the following _monotonicity rule_: - - - In a class `C` with a field `f`, the capture set `{this}` covers the capture set `{this.f}` as well as the capture set of any application of `this.f` to pure arguments. - -## Checked Exceptions - -Scala enables checked exceptions through a language import. Here is an example, -taken from the [safer exceptions page](./canthrow.md), and also described in a -[paper](https://infoscience.epfl.ch/record/290885) presented at the - 2021 Scala Symposium. -```scala -import language.experimental.saferExceptions - -class LimitExceeded extends Exception - -val limit = 10e+10 -def f(x: Double): Double throws LimitExceeded = - if x < limit then x * x else throw LimitExceeded() -``` -The new `throws` clause expands into an implicit parameter that provides -a `CanThrow` capability. Hence, function `f` could equivalently be written -like this: -```scala -def f(x: Double)(using CanThrow[LimitExceeded]): Double = ... -``` -If the implicit parameter is missing, an error is reported. For instance, the function definition -```scala -def g(x: Double): Double = - if x < limit then x * x else throw LimitExceeded() -``` -is rejected with this error message: -``` - | if x < limit then x * x else throw LimitExceeded() - | ^^^^^^^^^^^^^^^^^^^^^ - |The capability to throw exception LimitExceeded is missing. - |The capability can be provided by one of the following: - | - Adding a using clause `(using CanThrow[LimitExceeded])` to the definition of the enclosing method - | - Adding `throws LimitExceeded` clause after the result type of the enclosing method - | - Wrapping this piece of code with a `try` block that catches LimitExceeded -``` -`CanThrow` capabilities are required by `throw` expressions and are created -by `try` expressions. For instance, the expression -```scala -try xs.map(f).sum -catch case ex: LimitExceeded => -1 -``` -would be expanded by the compiler to something like the following: -```scala -try - erased given ctl: CanThrow[LimitExceeded] = compiletime.erasedValue - xs.map(f).sum -catch case ex: LimitExceeded => -1 -``` -(The `ctl` capability is only used for type checking but need not show up in the generated code, so it can be declared as -erased.) - -As with other capability based schemes, one needs to guard against capabilities -that are captured in results. For instance, here is a problematic use case: -```scala -def escaped(xs: Double*): (() => Double) throws LimitExceeded = - try () => xs.map(f).sum - catch case ex: LimitExceeded => () => -1 -val crasher = escaped(1, 2, 10e+11) -crasher() -``` -This code needs to be rejected since otherwise the call to `crasher()` would cause -an unhandled `LimitExceeded` exception to be thrown. - -Under the language import `language.experimental.captureChecking`, the code is indeed rejected -``` -14 | try () => xs.map(f).sum - | ^ - |The expression's type () => Double is not allowed to capture the root capability `cap`. - |This usually means that a capability persists longer than its allowed lifetime. -15 | catch case ex: LimitExceeded => () => -1 -``` -To integrate exception and capture checking, only two changes are needed: - - - `CanThrow` is declared as a class extending `Capability`, so all references to `CanThrow` instances are tracked. - - Escape checking is extended to `try` expressions. The result type of a `try` is not allowed to - capture the universal capability. - -## A Larger Example - -As a larger example, we present an implementation of lazy lists and some use cases. For simplicity, -our lists are lazy only in their tail part. This corresponds to what the Scala-2 type `Stream` did, whereas Scala 3's `LazyList` type computes strictly less since it is also lazy in the first argument. - -Here is the base trait `LzyList` for our version of lazy lists: -```scala -trait LzyList[+A]: - def isEmpty: Boolean - def head: A - def tail: LzyList[A]^{this} -``` -Note that `tail` carries a capture annotation. It says that the tail of a lazy list can -potentially capture the same references as the lazy list as a whole. - -The empty case of a `LzyList` is written as usual: -```scala -object LzyNil extends LzyList[Nothing]: - def isEmpty = true - def head = ??? - def tail = ??? -``` -Here is a formulation of the class for lazy cons nodes: -```scala -import scala.compiletime.uninitialized - -final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: - private var forced = false - private var cache: LzyList[A]^{this} = uninitialized - private def force = - if !forced then { cache = tl(); forced = true } - cache - - def isEmpty = false - def head = hd - def tail: LzyList[A]^{this} = force -end LzyCons -``` -The `LzyCons` class takes two parameters: A head `hd` and a tail `tl`, which is a function -returning a `LzyList`. Both the function and its result can capture arbitrary capabilities. -The result of applying the function is memoized after the first dereference of `tail` in -the private mutable field `cache`. Note that the typing of the assignment `cache = tl()` relies on the monotonicity rule for `{this}` capture sets. - -Here is an extension method to define an infix cons operator `#:` for lazy lists. It is analogous -to `::` but instead of a strict list it produces a lazy list without evaluating its right operand. -```scala -extension [A](x: A) - def #:(xs1: => LzyList[A]^): LzyList[A]^{xs1} = - LzyCons(x, () => xs1) -``` -Note that `#:` takes an impure call-by-name parameter `xs1` as its right argument. The result -of `#:` is a lazy list that captures that argument. - -As an example usage of `#:`, here is a method `tabulate` that creates a lazy list -of given length with a generator function `gen`. The generator function is allowed -to have side effects. -```scala -def tabulate[A](n: Int)(gen: Int => A) = - def recur(i: Int): LzyList[A]^{gen} = - if i == n then LzyNil - else gen(i) #: recur(i + 1) - recur(0) -``` -Here is a use of `tabulate`: -```scala -class LimitExceeded extends Exception -def squares(n: Int)(using ct: CanThrow[LimitExceeded]) = - tabulate(10): i => - if i > 9 then throw LimitExceeded() - i * i -``` -The inferred result type of `squares` is `LzyList[Int]^{ct}`, i.e it is a lazy list of -`Int`s that can throw the `LimitExceeded` exception when it is elaborated by calling `tail` -one or more times. - -Here are some further extension methods for mapping, filtering, and concatenating lazy lists: -```scala -extension [A](xs: LzyList[A]^) - def map[B](f: A => B): LzyList[B]^{xs, f} = - if xs.isEmpty then LzyNil - else f(xs.head) #: xs.tail.map(f) - - def filter(p: A => Boolean): LzyList[A]^{xs, p} = - if xs.isEmpty then LzyNil - else if p(xs.head) then xs.head #: xs.tail.filter(p) - else xs.tail.filter(p) - - def concat(ys: LzyList[A]^): LzyList[A]^{xs, ys} = - if xs.isEmpty then ys - else xs.head #: xs.tail.concat(ys) - - def drop(n: Int): LzyList[A]^{xs} = - if n == 0 then xs else xs.tail.drop(n - 1) -``` -Their capture annotations are all as one would expect: - - - Mapping a lazy list produces a lazy list that captures the original list as well - as the (possibly impure) mapping function. - - Filtering a lazy list produces a lazy list that captures the original list as well - as the (possibly impure) filtering predicate. - - Concatenating two lazy lists produces a lazy list that captures both arguments. - - Dropping elements from a lazy list gives a safe approximation where the original list is captured in the result. In fact, it's only some suffix of the list that is retained at run time, but our modelling identifies lazy lists and their suffixes, so this additional knowledge would not be useful. - -Of course the function passed to `map` or `filter` could also be pure. After all, `A -> B` is a subtype of `(A -> B)^{cap}` which is the same as `A => B`. In that case, the pure function -argument will _not_ show up in the result type of `map` or `filter`. For instance: -```scala -val xs = squares(10) -val ys: LzyList[Int]^{xs} = xs.map(_ + 1) -``` -The type of the mapped list `ys` has only `xs` in its capture set. The actual function -argument does not show up since it is pure. Likewise, if the lazy list -`xs` was pure, it would not show up in any of the method results. -This demonstrates that capability-based -effect systems with capture checking are naturally _effect polymorphic_. - -This concludes our example. It's worth mentioning that an equivalent program defining and using standard, strict lists would require no capture annotations whatsoever. It would compile exactly as written now in standard Scala 3, yet one gets the capture checking for free. Essentially, `=>` already means "can capture anything" and since in a strict list side effecting operations are not retained in the result, there are no additional captures to record. A strict list could of course capture side-effecting closures in its elements but then tunnelling applies, since -these elements are represented by a type variable. This means we don't need to annotate anything there either. - -Another possibility would be a variant of lazy lists that requires all functions passed to `map`, `filter` and other operations like it to be pure. E.g. `map` on such a list would be defined like this: -```scala -extension [A](xs: LzyList[A]) - def map[B](f: A -> B): LzyList[B] = ... -``` -That variant would not require any capture annotations either. - -To summarize, there are two "sweet spots" of data structure design: strict lists in -side-effecting or resource-aware code and lazy lists in purely functional code. -Both are already correctly capture-typed without requiring any explicit annotations. Capture annotations only come into play where the semantics gets more complicated because we deal with delayed effects such as in impure lazy lists or side-effecting iterators over strict lists. This property is probably one of the greatest plus points of our approach to capture checking compared to previous techniques which tend to be more noisy. - -## Existential Capabilities - -In fact, what is written as the top type `cap` can mean different capabilities, depending on scope. For instance, consider the function type -`() -> Iterator[T]^`. This is taken to mean -```scala - () -> Exists x. Iterator[T]^x -``` -In other words, it means an unknown type bound `x` by an "existential" in the scope of the function result. A `cap` in a function result is therefore different from a `cap` at the top-level or in a function parameter. - -Internally, an existential type is represented as a kind of dependent function type. The type above would be modelled as -```scala - () -> (x: Exists) -> Iterator[T]^x -``` -Here, `Exists` is a sealed trait in the `caps` object that serves to mark -dependent functions as representations of existentials. It should be noted -that this is strictly an internal representation. It is explained here because it can show up in error messages. It is generally not recommended to use this syntax in source code. Instead one should rely on the automatic expansion of `^` and `cap` to existentials, which can be -influenced by introducing the right alias types. The rules for this expansion are as follows: - - - If a function result type contains covariant occurrences of `cap`, - we replace these occurrences with a fresh existential variable which - is bound by a quantifier scoping over the result type. - - We might want to do the same expansion in function arguments, but right now this is not done. - - Occurrences of `cap` elsewhere are not translated. They can be seen as representing an existential at the top-level scope. - -**Examples:** - - - `A => B` is an alias type that expands to `(A -> B)^`, therefore - `() -> A => B` expands to `() -> Exists c. A ->{c} B`. - - - `() -> Iterator[A => B]` expands to `() -> Exists c. Iterator[A ->{c} B]` - - - `A -> B^` expands to `A -> Exists c.B^{c}`. - - - If we define `type Fun[T] = A -> T`, then `() -> Fun[B^]` expands to `() -> Exists c.Fun[B^{c}]`, which dealiases to `() -> Exists c.A -> B^{c}`. This demonstrates how aliases can be used to force existential binders to be in some specific outer scope. - - - If we define - ```scala - type F = A -> Fun[B^] - ``` - then the type alias expands to - ```scala - type F = A -> Exists c.A -> B^{c} - ``` - -**Typing Rules:** - - - When we typecheck the body of a function or method, any covariant occurrences of `cap` in the result type are bound with a fresh existential. - - Conversely, when we typecheck the application of a function or method, - with an existential result type `Exists ex.T`, the result of the application is `T` where every occurrence of the existentially bound - variable `ex` is replaced by `cap`. - -## Reach Capabilities - -Say you have a method `f` that takes an impure function argument which gets stored in a `var`: -```scala -def f(op: A => B) - var x: A ->{op} B = op - ... -``` -This is legal even though `var`s cannot have types with `cap` or existential capabilities. The trick is that the type of the variable `x` -is not `A => B` (this would be rejected), but is the "narrowed" type -`A ->{op} B`. In other words, all capabilities retained by values of `x` -are all also referred to by `op`, which justifies the replacement of `cap` by `op`. - -A more complicated situation is if we want to store successive values -held in a list. Example: -```scala -def f(ops: List[A => B]) - var xs = ops - var x: ??? = xs.head - while xs.nonEmpty do - xs = xs.tail - x = xs.head - ... -``` -Here, `x` cannot be given a type with an `ops` capability. In fact, `ops` is pure, i.e. it's capture set is empty, so it cannot be used as the name of a capability. What we would like to express is that `x` refers to -any operation "reachable" through `ops`. This can be expressed using a -_reach capability_ `ops*`. -```scala -def f(ops: List[A => B]) - var xs = ops - var x: A ->{ops*} B = xs.head - ... -``` -Reach capabilities take the form `x*` where `x` is syntactically a regular capability. If `x: T` then `x*` stands for any capability that appears covariantly in `T` and that is accessed through `x`. The least supertype of this capability is the set of all capabilities appearing covariantly in `T`. - -## Capability Polymorphism - -It is sometimes convenient to write operations that are parameterized with a capture set of capabilities. For instance consider a type of event sources -`Source` on which `Listener`s can be registered. Listeners can hold certain capabilities, which show up as a parameter to `Source`: -```scala -class Source[X^]: - private var listeners: Set[Listener^{X}] = Set.empty - def register(x: Listener^{X}): Unit = - listeners += x - - def allListeners: Set[Listener^{X}] = listeners -``` -The type variable `X^` can be instantiated with a set of capabilities. It can occur in capture sets in its scope. For instance, in the example above -we see a variable `listeners` that has as type a `Set` of `Listeners` capturing `X`. The `register` method takes a listener of this type -and assigns it to the variable. - -Capture-set variables `X^` without user-annotated bounds by default range over the interval `>: {} <: {caps.cap}` which is the universe of capture sets instead of regular types. - -Under the hood, such capture-set variables are represented as regular type variables within the special interval - `>: CapSet <: CapSet^`. -For instance, `Source` from above could be equivalently -defined as follows: -```scala -class Source[X >: CapSet <: CapSet^]: - ... -``` -`CapSet` is a sealed trait in the `caps` object. It cannot be instantiated or inherited, so its only -purpose is to identify type variables which are capture sets. In non-capture-checked -usage contexts, the type system will treat `CapSet^{a}` and `CapSet^{a,b}` as the type `CapSet`, whereas -with capture checking enabled, it will take the annotated capture sets into account, -so that `CapSet^{a}` and `CapSet^{a,b}` are distinct. -This representation based on `CapSet` is subject to change and -its direct use is discouraged. - -Capture-set variables can be inferred like regular type variables. When they should be instantiated -explicitly one supplies a concrete capture set. For instance: -```scala -class Async extends caps.Capability - -def listener(async: Async): Listener^{async} = ??? - -def test1(async1: Async, others: List[Async]) = - val src = Source[{async1, others*}] - ... -``` -Here, `src` is created as a `Source` on which listeners can be registered that refer to the `async` capability or to any of the capabilities in list `others`. So we can continue the example code above as follows: -```scala - src.register(listener(async1)) - others.map(listener).foreach(src.register) - val ls: Set[Listener^{async, others*}] = src.allListeners -``` -A common use-case for explicit capture parameters is describing changes to the captures of mutable fields, such as concatenating -effectful iterators: -```scala -class ConcatIterator[A, C^](var iterators: mutable.List[IterableOnce[A]^{C}]): - def concat(it: IterableOnce[A]^): ConcatIterator[A, {C, it}]^{this, it} = - iterators ++= it // ^ - this // track contents of `it` in the result -``` -In such a scenario, we also should ensure that any pre-existing alias of a `ConcatIterator` object should become -inaccessible after invoking its `concat` method. This is achieved with mutation and separation tracking which are -currently in development. - - -## Capability Members - -Just as parametrization by types can be equally expressed with type members, we could -also define the `Source[X^]` class above could using a _capability member_: -```scala -class Source: - type X^ - private var listeners: Set[Listener^{this.X}] = Set.empty - ... // as before -``` -Here, we can refer to capability members using paths in capture sets (such as `{this.X}`). Similarly to type members, -capability members can be upper- and lower-bounded with capture sets: -```scala -trait Thread: - type Cap^ - def run(block: () ->{this.Cap} -> Unit): Unit - -trait GPUThread extends Thread: - type Cap^ >: {cudaMalloc, cudaFree} <: {caps.cap} -``` -Since `caps.cap` is the top element for subcapturing, we could have also left out the -upper bound: `type Cap^ >: {cudaMalloc, cudaFree}`. - - -[More Advanced Use Cases](cc-advanced.md) - -## Compilation Options - -The following options are relevant for capture checking. - - - **-Vprint:cc** Prints the program with capturing types as inferred by capture checking. - - **-Ycc-debug** Gives more detailed, implementation-oriented information about capture checking, as described in the next section. - - The implementation supporting capture checking with these options is currently in branch `cc-experiment` on dotty.epfl.ch. - -## Capture Checking Internals - -The capture checker is architected as a propagation constraint solver, which runs as a separate phase after type-checking and some initial transformations. - -Constraint variables stand for unknown capture sets. A constraint variable is introduced - - - for every part of a previously inferred type, - - for the accessed references of every method, class, anonymous function, or by-name argument, - - for the parameters passed in a class constructor call. - -Capture sets in explicitly written types are treated as constants (before capture checking, such sets are simply ignored). - -The capture checker essentially rechecks the program with the usual typing rules. Every time a subtype requirement between capturing types is checked, this translates to a subcapturing test on capture sets. If the two sets are constant, this is simply a yes/no question, where a no will produce an error message. - -If the lower set `C₁` of a comparison `C₁ <: C₂` is a variable, the set `C₂` is recorded -as a _superset_ of `C₁`. If the upper set `C₂` is a variable, the elements of `C₁` are _propagated_ to `C₂`. Propagation of an element `x` to a set `C` means that `x` is included as an element in `C`, and it is also propagated -to all known supersets of `C`. If such a superset is a constant, it is checked that `x` is included in it. If that's not the case, the original comparison `C₁ <: C₂` has no solution and an error is reported. - -The type checker also performs various maps on types, for instance when substituting actual argument types for formal parameter types in dependent functions, or mapping -member types with "as-seen-from" in a selection. Maps keep track of the variance -of positions in a type. The variance is initially covariant, it flips to -contravariant in function parameter positions, and can be either covariant, -contravariant, or nonvariant in type arguments, depending on the variance of -the type parameter. - -When capture checking, the same maps are also performed on capture sets. If a capture set is a constant, its elements (which are capabilities) are mapped as regular types. If the result of such a map is not a capability, the result is approximated according to the variance of the type. A covariant approximation replaces a type by its capture set. -A contravariant approximation replaces it with the empty capture set. A nonvariant -approximation replaces the enclosing capturing type with a range of possible types -that gets propagated and resolved further out. - -When a mapping `m` is performed on a capture set variable `C`, a new variable `Cm` is created that contains the mapped elements and that is linked with `C`. If `C` subsequently acquires further elements through propagation, these are also propagated to `Cm` after being transformed by the `m` mapping. `Cm` also gets the same supersets as `C`, mapped again using `m`. - -One interesting aspect of the capture checker concerns the implementation of capture tunnelling. The [foundational theory](https://infoscience.epfl.ch/record/290885) on which capture checking is based makes tunnelling explicit through so-called _box_ and -_unbox_ operations. Boxing hides a capture set and unboxing recovers it. The capture checker inserts virtual box and unbox operations based on actual and expected types similar to the way the type checker inserts implicit conversions. When capture set variables are first introduced, any capture set in a capturing type that is an instance of a type parameter instance is marked as "boxed". A boxing operation is -inserted if the expected type of an expression is a capturing type with -a boxed capture set variable. The effect of the insertion is that any references -to capabilities in the boxed expression are forgotten, which means that capture -propagation is stopped. Dually, if the actual type of an expression has -a boxed variable as capture set, an unbox operation is inserted, which adds all -elements of the capture set to the environment. - -Boxing and unboxing has no runtime effect, so the insertion of these operations is only simulated; the only visible effect is the retraction and insertion -of variables in the capture sets representing the environment of the currently checked expression. - -The `-Ycc-debug` option provides some insight into the workings of the capture checker. -When it is turned on, boxed sets are marked explicitly and capture set variables are printed with an ID and some information about their provenance. For instance, the string `{f, xs}33M5V` indicates a capture set -variable that is known to hold elements `f` and `xs`. The variable's ID is `33`. The `M` -indicates that the variable was created through a mapping from a variable with ID `5`. The latter is a regular variable, as indicated - by `V`. - -Generally, the string following the capture set consists of alternating numbers and letters where each number gives a variable ID and each letter gives the provenance of the variable. Possible letters are - - - `V` : a regular variable, - - `M` : a variable resulting from a _mapping_ of the variable indicated by the string to the right, - - `B` : similar to `M` but where the mapping is a _bijection_, - - `F` : a variable resulting from _filtering_ the elements of the variable indicated by the string to the right, - - `I` : a variable resulting from an _intersection_ of two capture sets, - - `D` : a variable resulting from the set _difference_ of two capture sets. - - `R` : a regular variable that _refines_ a class parameter, so that the capture - set of a constructor argument is known in the class instance type. - -At the end of a compilation run, `-Ycc-debug` will print all variable dependencies of variables referred to in previous output. Here is an example: -``` -Capture set dependencies: - {}2V :: - {}3V :: - {}4V :: - {f, xs}5V :: {f, xs}31M5V, {f, xs}32M5V - {f, xs}31M5V :: {xs, f} - {f, xs}32M5V :: -``` -This section lists all variables that appeared in previous diagnostics and their dependencies, recursively. For instance, we learn that - - - variables 2, 3, 4 are empty and have no dependencies, - - variable `5` has two dependencies: variables `31` and `32` which both result from mapping variable `5`, - - variable `31` has a constant fixed superset `{xs, f}` - - variable `32` has no dependencies. - - - diff --git a/docs/_docs/reference/experimental/overview.md b/docs/_docs/reference/experimental/overview.md index f70cf32b9c24..9242056d8405 100644 --- a/docs/_docs/reference/experimental/overview.md +++ b/docs/_docs/reference/experimental/overview.md @@ -32,4 +32,4 @@ Hence, dependent projects also have to be experimental. Some experimental language features that are still in research and development can be enabled with special compiler options. These include * [`-Yexplicit-nulls`](./explicit-nulls.md). Enable support for tracking null references in the type system. -* [`-Ycc`](./cc.md). Enable support for capture checking. +* [`-Ycc`](./capture-checking/cc.md). Enable support for capture checking. diff --git a/docs/sidebar.yml b/docs/sidebar.yml index 440cfa450849..144ad293eaea 100644 --- a/docs/sidebar.yml +++ b/docs/sidebar.yml @@ -162,9 +162,20 @@ subsection: - page: reference/experimental/explicit-nulls.md - page: reference/experimental/main-annotation.md - page: reference/experimental/into.md - - page: reference/experimental/cc.md - - page: reference/experimental/cc-advanced.md - hidden: true + - title: Capture Checking + index: reference/experimental/capture-checking/cc.md + subsection: + - page: reference/experimental/capture-checking/basics.md + - page: reference/experimental/capture-checking/classes.md + - page: reference/experimental/capture-checking/polymorphism.md + - page: reference/experimental/capture-checking/advanced.md + hidden: true + - page: reference/experimental/capture-checking/scoped-caps.md + - page: reference/experimental/capture-checking/classifiers.md + - page: reference/experimental/capture-checking/checked-exceptions.md + - page: reference/experimental/capture-checking/separation-checking.md + - page: reference/experimental/capture-checking/how-to-use.md + - page: reference/experimental/capture-checking/internals.md - page: reference/experimental/purefuns.md - page: reference/experimental/tupled-function.md - page: reference/experimental/modularity.md diff --git a/library/src/scala/caps/package.scala b/library/src/scala/caps/package.scala index ff029fbbae9c..45d1e18e741a 100644 --- a/library/src/scala/caps/package.scala +++ b/library/src/scala/caps/package.scala @@ -123,16 +123,6 @@ final class reserve extends annotation.StaticAnnotation @experimental final class use extends annotation.StaticAnnotation -/** An annotations on parameters and update methods. - * On a parameter it states that any capabilties passed in the argument - * are no longer available afterwards, unless they are of class `SharableCapabilitty`. - * On an update method, it states that the `this` of the enclosing class is - * consumed, which means that any capabilities of the method prefix are - * no longer available afterwards. - */ -@experimental -final class consume extends annotation.StaticAnnotation - /** A trait that used to allow expressing existential types. Replaced by * root.Result instances. */ @@ -143,6 +133,11 @@ sealed trait Exists extends Capability @experimental object internal: + /** An annotation to reflect that a parameter or method carries the `consume` + * soft modifier. + */ + final class consume extends annotation.StaticAnnotation + /** An internal annotation placed on a refinement created by capture checking. * Refinements with this annotation unconditionally override any * info from the parent type, so no intersection needs to be formed. diff --git a/project/resources/referenceReplacements/sidebar.yml b/project/resources/referenceReplacements/sidebar.yml index 4e40642858c9..2f766e17e715 100644 --- a/project/resources/referenceReplacements/sidebar.yml +++ b/project/resources/referenceReplacements/sidebar.yml @@ -149,9 +149,20 @@ subsection: - page: reference/experimental/numeric-literals.md - page: reference/experimental/explicit-nulls.md - page: reference/experimental/main-annotation.md - - page: reference/experimental/cc.md - - page: reference/experimental/cc-advanced.md - hidden: true + - title: Capture Checking + index: reference/experimental/capture-checking/cc.md + subsection: + - page: reference/experimental/capture-checking/basics.md + - page: reference/experimental/capture-checking/classes.md + - page: reference/experimental/capture-checking/polymorphism.md + - page: reference/experimental/capture-checking/advanced.md + hidden: true + - page: reference/experimental/capture-checking/scoped-caps.md + - page: reference/experimental/capture-checking/classifiers.md + - page: reference/experimental/capture-checking/checked-exceptions.md + - page: reference/experimental/capture-checking/separation-checking.md + - page: reference/experimental/capture-checking/how-to-use.md + - page: reference/experimental/capture-checking/internals.md - page: reference/experimental/tupled-function.md - page: reference/syntax.md - title: Language Versions diff --git a/scaladoc/src/dotty/tools/scaladoc/cc/CaptureOps.scala b/scaladoc/src/dotty/tools/scaladoc/cc/CaptureOps.scala index 626162db55ec..3867e1e37ac7 100644 --- a/scaladoc/src/dotty/tools/scaladoc/cc/CaptureOps.scala +++ b/scaladoc/src/dotty/tools/scaladoc/cc/CaptureOps.scala @@ -27,7 +27,7 @@ object CaptureDefs: def UseAnnot(using qctx: Quotes) = qctx.reflect.Symbol.requiredClass("scala.caps.use") def ConsumeAnnot(using qctx: Quotes) = - qctx.reflect.Symbol.requiredClass("scala.caps.consume") + qctx.reflect.Symbol.requiredClass("scala.caps.internal.consume") def ReachCapabilityAnnot(using qctx: Quotes) = qctx.reflect.Symbol.requiredClass("scala.annotation.internal.reachCapability") def RootCapabilityAnnot(using qctx: Quotes) = diff --git a/tests/neg-custom-args/captures/bad-uses-2.scala b/tests/neg-custom-args/captures/bad-uses-2.scala index d8bc3eca93e6..7a4f26b506a9 100644 --- a/tests/neg-custom-args/captures/bad-uses-2.scala +++ b/tests/neg-custom-args/captures/bad-uses-2.scala @@ -1,13 +1,12 @@ -import caps.{use, consume} +import caps.{use, Mutable} class TestUse: @use def F = ??? // error @use val x = ??? // error @use type T // error def foo[@use T](@use c: T): Unit = ??? // error // error -class TestConsume: - @consume def F = ??? // ok - @consume val x = ??? // error - @consume type T // error - def foo[@consume T](@use c: T): Unit = ??? // error // error +class TestConsume extends Mutable: + consume def F = ??? // ok + consume val x = ??? // error + consume type T // error diff --git a/tests/neg-custom-args/captures/box-adapt-contra.scala b/tests/neg-custom-args/captures/box-adapt-contra.scala index 9c18a9a2c50a..660c82ac8410 100644 --- a/tests/neg-custom-args/captures/box-adapt-contra.scala +++ b/tests/neg-custom-args/captures/box-adapt-contra.scala @@ -1,5 +1,5 @@ -import caps.consume + trait Cap @@ -8,7 +8,7 @@ def useCap[X](x: X): (X -> Unit) -> Unit = ??? def test1(c: Cap^): Unit = val f: (Cap^{c} -> Unit) -> Unit = useCap[Cap^{c}](c) // error -def test2(@consume c: Cap^, d: Cap^): Unit = +def test2(consume c: Cap^, d: Cap^): Unit = def useCap1[X](x: X): (X => Unit) -> Unit = ??? val f1: (Cap^{c} => Unit) ->{c} Unit = useCap1[Cap^{c}](c) // error, was ok when cap was a root diff --git a/tests/neg-custom-args/captures/cc-annot-value-classes2.scala b/tests/neg-custom-args/captures/cc-annot-value-classes2.scala index 5821f9664f6b..f8449b49a444 100644 --- a/tests/neg-custom-args/captures/cc-annot-value-classes2.scala +++ b/tests/neg-custom-args/captures/cc-annot-value-classes2.scala @@ -1,13 +1,13 @@ import language.experimental.captureChecking import caps.* trait Ref extends Mutable -def kill(@consume x: Ref^): Unit = () +def kill(consume x: Ref^): Unit = () class C1: - def myKill(@consume x: Ref^): Unit = kill(x) // ok + def myKill(consume x: Ref^): Unit = kill(x) // ok class C2(val dummy: Int) extends AnyVal: - def myKill(@consume x: Ref^): Unit = kill(x) // ok, too + def myKill(consume x: Ref^): Unit = kill(x) // ok, too class C3: def myKill(x: Ref^): Unit = kill(x) // error diff --git a/tests/neg-custom-args/captures/cc-this-shared.scala b/tests/neg-custom-args/captures/cc-this-shared.scala index 769bae9b5ee6..cd4b6f93af07 100644 --- a/tests/neg-custom-args/captures/cc-this-shared.scala +++ b/tests/neg-custom-args/captures/cc-this-shared.scala @@ -1,4 +1,4 @@ -import caps.consume + class Cap extends caps.SharedCapability @@ -19,7 +19,7 @@ def test(using Cap) = class C4(val f: () => Int) extends C3 // error // The following is a variation of pos/cc-this.scala -def test2(using @consume cc: Cap) = +def test2(using consume cc: Cap) = class C(val x: () => Int): val y: C^ = this diff --git a/tests/neg-custom-args/captures/cc-this.scala b/tests/neg-custom-args/captures/cc-this.scala index d90c0084a14f..3d9f8ca5cf53 100644 --- a/tests/neg-custom-args/captures/cc-this.scala +++ b/tests/neg-custom-args/captures/cc-this.scala @@ -1,4 +1,4 @@ -import caps.consume + class Cap extends caps.ExclusiveCapability @@ -19,7 +19,7 @@ def test(using Cap) = class C4(val f: () => Int) extends C3 // error // The following is a variation of pos/cc-this.scala -def test2(using @consume cc: Cap) = +def test2(using consume cc: Cap) = class C(val x: () => Int): val y: C^ = this diff --git a/tests/neg-custom-args/captures/consume-overrides.scala b/tests/neg-custom-args/captures/consume-overrides.scala index 78f013349a31..f3cd371b0cd7 100644 --- a/tests/neg-custom-args/captures/consume-overrides.scala +++ b/tests/neg-custom-args/captures/consume-overrides.scala @@ -1,15 +1,15 @@ -import caps.consume + trait A[X]: - def foo(@consume x: X): X + def foo(consume x: X): X def bar(x: X): X trait B extends A[C]: def foo(x: C): C // error - def bar(@consume x: C): C // error + def bar(consume x: C): C // error trait B2: def foo(x: C): C - def bar(@consume x: C): C + def bar(consume x: C): C abstract class C extends A[C], B2 // error diff --git a/tests/neg-custom-args/captures/delayedRunops.check b/tests/neg-custom-args/captures/delayedRunops.check index df578f4c6146..05d02af6b5a7 100644 --- a/tests/neg-custom-args/captures/delayedRunops.check +++ b/tests/neg-custom-args/captures/delayedRunops.check @@ -1,31 +1,31 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:14:4 --------------------------------- -14 | () => // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:12:4 --------------------------------- +12 | () => // error | ^ | Found: () ->{ops*} Unit | Required: () -> Unit | | Note that capability ops* is not included in capture set {}. -15 | val ops1 = ops -16 | runOps(ops1) +13 | val ops1 = ops +14 | runOps(ops1) | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:26:4 --------------------------------- -26 | () => // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/delayedRunops.scala:24:4 --------------------------------- +24 | () => // error | ^ | Found: () ->{ops*} Unit | Required: () -> Unit | | Note that capability ops* is not included in capture set {}. -27 | val ops1: List[() ->{ops*} Unit] = ops -28 | runOps(ops1) +25 | val ops1: List[() ->{ops*} Unit] = ops +26 | runOps(ops1) | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/delayedRunops.scala:22:6 ------------------------------------------------------ -22 | runOps(ops1) // error +-- Error: tests/neg-custom-args/captures/delayedRunops.scala:20:6 ------------------------------------------------------ +20 | runOps(ops1) // error | ^^^^^^ | Local reach capability ops* leaks into capture scope of method delayedRunOps2. | You could try to abstract the capabilities referred to by ops* in a capset variable. --- Error: tests/neg-custom-args/captures/delayedRunops.scala:21:16 ----------------------------------------------------- -21 | val ops1: List[() => Unit] = ops // error +-- Error: tests/neg-custom-args/captures/delayedRunops.scala:19:16 ----------------------------------------------------- +19 | val ops1: List[() => Unit] = ops // error | ^^^^^^^^^^^^^^^^ | Separation failure: value ops1's type List[() => Unit] hides non-local parameter ops diff --git a/tests/neg-custom-args/captures/delayedRunops.scala b/tests/neg-custom-args/captures/delayedRunops.scala index a9ad226d4da1..4b89a14537c5 100644 --- a/tests/neg-custom-args/captures/delayedRunops.scala +++ b/tests/neg-custom-args/captures/delayedRunops.scala @@ -1,7 +1,5 @@ import language.experimental.captureChecking -import caps.{use, consume} - def runOps[C^](ops: List[() ->{C} Unit]): Unit = ops.foreach(op => op()) @@ -16,7 +14,7 @@ import caps.{use, consume} runOps(ops1) // unsound: impure operation pretended pure - def delayedRunOps2(@consume ops: List[() => Unit]): () ->{} Unit = + def delayedRunOps2(consume ops: List[() => Unit]): () ->{} Unit = () => val ops1: List[() => Unit] = ops // error runOps(ops1) // error diff --git a/tests/neg-custom-args/captures/i19330.check b/tests/neg-custom-args/captures/i19330.check index e142d6dbddb0..72947fb1bcf6 100644 --- a/tests/neg-custom-args/captures/i19330.check +++ b/tests/neg-custom-args/captures/i19330.check @@ -31,4 +31,4 @@ 16 | val t: () => Logger^ = () => l // error | ^^^^^^^^^^^^^ | Separation failure: value t's type () => Logger^ hides parameter l. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/i21442.check b/tests/neg-custom-args/captures/i21442.check index aa0a8e53ff7f..0f64325fad98 100644 --- a/tests/neg-custom-args/captures/i21442.check +++ b/tests/neg-custom-args/captures/i21442.check @@ -12,4 +12,4 @@ 17 | val x1: Boxed[IO^] = x // error | ^^^^^^^^^^ | Separation failure: value x1's type Boxed[IO^] hides parameter x. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/i22005.scala b/tests/neg-custom-args/captures/i22005.scala index fc7d4183f8c3..8bf17661fc82 100644 --- a/tests/neg-custom-args/captures/i22005.scala +++ b/tests/neg-custom-args/captures/i22005.scala @@ -7,4 +7,4 @@ class File(io: IO^) class Handler[C^]: def f(file: File^): File^{C} = file // error - def g(@consume file: File^{C}): File^ = file // ok + def g(consume file: File^{C}): File^ = file // ok diff --git a/tests/neg-custom-args/captures/i23431.check b/tests/neg-custom-args/captures/i23431.check index 624a3b63cb09..722fd6d6e313 100644 --- a/tests/neg-custom-args/captures/i23431.check +++ b/tests/neg-custom-args/captures/i23431.check @@ -48,4 +48,4 @@ 6 | var myIO: IO^ = io1 // error: separation | ^^^ | Separation failure: variable myIO's type IO^ hides parameter io1. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/linear-buffer-2.check b/tests/neg-custom-args/captures/linear-buffer-2.check index be8f0623418e..6d9493bddb02 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.check +++ b/tests/neg-custom-args/captures/linear-buffer-2.check @@ -10,7 +10,7 @@ 20 | val buf3 = buf1.append(4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 18 + | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -18,7 +18,7 @@ 28 | val buf3 = buf1.append(4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 25 + | consume parameter or was used as a prefix to a consume method on line 25 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -26,7 +26,7 @@ 38 | val buf3 = buf1.append(4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 33 + | consume parameter or was used as a prefix to a consume method on line 33 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -34,6 +34,6 @@ 42 | buf.append(1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot - | be passed to a @consume parameter or be used as a prefix of a @consume method call. + | be passed to a consume parameter or be used as a prefix of a consume method call. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer-2.scala b/tests/neg-custom-args/captures/linear-buffer-2.scala index 78561351838b..d2ed1544fadf 100644 --- a/tests/neg-custom-args/captures/linear-buffer-2.scala +++ b/tests/neg-custom-args/captures/linear-buffer-2.scala @@ -1,25 +1,25 @@ -import caps.{cap, consume, Mutable} +import caps.{cap, Mutable} import language.experimental.captureChecking class Buffer[T] extends Mutable: - @consume update def append(x: T): Buffer[T]^ = this // ok + consume def append(x: T): Buffer[T]^ = this // ok -def app[T](@consume buf: Buffer[T]^, elem: T): Buffer[T]^ = +def app[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ = buf.append(elem) -def Test(@consume buf: Buffer[Int]^) = +def Test(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = buf.append(1) val buf2 = buf1.append(2) // OK val buf3 = buf.append(3) // error -def Test2(@consume buf: Buffer[Int]^) = +def Test2(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = buf.append(1) val buf2 = if ??? then buf1.append(2) // OK else buf1.append(3) // OK val buf3 = buf1.append(4) // error -def Test3(@consume buf: Buffer[Int]^) = +def Test3(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = buf.append(1) val buf2 = (??? : Int) match case 1 => buf1.append(2) // OK @@ -27,7 +27,7 @@ def Test3(@consume buf: Buffer[Int]^) = case _ => buf1.append(3) val buf3 = buf1.append(4) // error -def Test4(@consume buf: Buffer[Int]^) = +def Test4(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = buf.append(1) val buf2 = (??? : Int) match case 1 => buf1.append(2) // OK @@ -37,6 +37,6 @@ def Test4(@consume buf: Buffer[Int]^) = case 5 => buf1.append(5) val buf3 = buf1.append(4) // error -def Test5(@consume buf: Buffer[Int]^) = +def Test5(consume buf: Buffer[Int]^) = while true do buf.append(1) // error diff --git a/tests/neg-custom-args/captures/linear-buffer.check b/tests/neg-custom-args/captures/linear-buffer.check index 4aaf1794aac1..78ddb54b5535 100644 --- a/tests/neg-custom-args/captures/linear-buffer.check +++ b/tests/neg-custom-args/captures/linear-buffer.check @@ -2,17 +2,17 @@ 5 | update def append(x: T): BadBuffer[T]^ = this // error | ^^^^^^^^^^^^^ | Separation failure: method append's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. - | The access must be in a @consume method to allow this. + | The access must be in a consume method to allow this. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:7:13 ------------------------------------------------------ 7 | def bar: BadBuffer[T]^ = this // error | ^^^^^^^^^^^^^ | Separation failure: method bar's result type BadBuffer[T]^ hides non-local this of class class BadBuffer. - | The access must be in a @consume method to allow this. + | The access must be in a consume method to allow this. -- Error: tests/neg-custom-args/captures/linear-buffer.scala:19:17 ----------------------------------------------------- 19 | val buf3 = app(buf, 3) // error | ^^^ | Separation failure: Illegal access to (buf : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 17 + | consume parameter or was used as a prefix to a consume method on line 17 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf @@ -20,7 +20,7 @@ 26 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 24 + | consume parameter or was used as a prefix to a consume method on line 24 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -28,7 +28,7 @@ 34 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 31 + | consume parameter or was used as a prefix to a consume method on line 31 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -36,7 +36,7 @@ 44 | val buf3 = app(buf1, 4) // error | ^^^^ | Separation failure: Illegal access to (buf1 : Buffer[Int]^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 39 + | consume parameter or was used as a prefix to a consume method on line 39 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of value buf1 @@ -44,6 +44,6 @@ 48 | app(buf, 1) // error | ^^^ | Separation failure: (buf : Buffer[Int]^) appears in a loop, therefore it cannot - | be passed to a @consume parameter or be used as a prefix of a @consume method call. + | be passed to a consume parameter or be used as a prefix of a consume method call. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter buf diff --git a/tests/neg-custom-args/captures/linear-buffer.scala b/tests/neg-custom-args/captures/linear-buffer.scala index 5c6d991579aa..27e2efeeed1f 100644 --- a/tests/neg-custom-args/captures/linear-buffer.scala +++ b/tests/neg-custom-args/captures/linear-buffer.scala @@ -1,4 +1,4 @@ -import caps.{cap, consume, Mutable} +import caps.{cap, Mutable} import language.experimental.captureChecking class BadBuffer[T] extends Mutable: @@ -8,24 +8,24 @@ class BadBuffer[T] extends Mutable: bar class Buffer[T] extends Mutable: - @consume update def append(x: T): Buffer[T]^ = this // ok + consume def append(x: T): Buffer[T]^ = this // ok -def app[T](@consume buf: Buffer[T]^, elem: T): Buffer[T]^ = +def app[T](consume buf: Buffer[T]^, elem: T): Buffer[T]^ = buf.append(elem) -def Test(@consume buf: Buffer[Int]^) = +def Test(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = app(buf, 1) val buf2 = app(buf1, 2) // OK val buf3 = app(buf, 3) // error -def Test2(@consume buf: Buffer[Int]^) = +def Test2(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = app(buf, 1) val buf2 = if ??? then app(buf1, 2) // OK else app(buf1, 3) // OK val buf3 = app(buf1, 4) // error -def Test3(@consume buf: Buffer[Int]^) = +def Test3(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = app(buf, 1) val buf2 = (??? : Int) match case 1 => app(buf1, 2) // OK @@ -33,7 +33,7 @@ def Test3(@consume buf: Buffer[Int]^) = case _ => app(buf1, 3) val buf3 = app(buf1, 4) // error -def Test4(@consume buf: Buffer[Int]^) = +def Test4(consume buf: Buffer[Int]^) = val buf1: Buffer[Int]^ = app(buf, 1) val buf2 = (??? : Int) match case 1 => app(buf1, 2) // OK @@ -43,6 +43,6 @@ def Test4(@consume buf: Buffer[Int]^) = case 5 => app(buf1, 5) val buf3 = app(buf1, 4) // error -def Test5(@consume buf: Buffer[Int]^) = +def Test5(consume buf: Buffer[Int]^) = while true do app(buf, 1) // error diff --git a/tests/neg-custom-args/captures/localReaches.check b/tests/neg-custom-args/captures/localReaches.check index 1df4886e61d5..5acb12457323 100644 --- a/tests/neg-custom-args/captures/localReaches.check +++ b/tests/neg-custom-args/captures/localReaches.check @@ -12,9 +12,9 @@ 14 | val xs: List[() => Unit] = op :: Nil // error | ^^^^^^^^^^^^^^^^ | Separation failure: value xs's type List[() => Unit] hides parameter op. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/localReaches.scala:22:10 ------------------------------------------------------ 22 | val xs: List[() => Unit] = ops // error | ^^^^^^^^^^^^^^^^ | Separation failure: value xs's type List[() => Unit] hides parameter ops. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/localReaches.scala b/tests/neg-custom-args/captures/localReaches.scala index 9795a6dd099c..d88e3f4bb992 100644 --- a/tests/neg-custom-args/captures/localReaches.scala +++ b/tests/neg-custom-args/captures/localReaches.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking // no separation checking -import caps.consume + def localReach() = val xs: List[() => Unit] = ??? diff --git a/tests/neg-custom-args/captures/non-local-consume.scala b/tests/neg-custom-args/captures/non-local-consume.scala index 0e46146eb7e8..81915a54246f 100644 --- a/tests/neg-custom-args/captures/non-local-consume.scala +++ b/tests/neg-custom-args/captures/non-local-consume.scala @@ -1,29 +1,29 @@ -import caps.{cap, consume, Mutable} +import caps.{cap, Mutable} import language.experimental.captureChecking class Buffer extends Mutable -def f1(@consume buf: Buffer^): Buffer^ = +def f1(consume buf: Buffer^): Buffer^ = val buf1: Buffer^ = buf // OK buf1 -def f2(@consume buf: Buffer^): Buffer^ = +def f2(consume buf: Buffer^): Buffer^ = def g(): Buffer^ = buf // error g() -def f3(@consume buf: Buffer^): Buffer^ = +def f3(consume buf: Buffer^): Buffer^ = val buf1 = buf def g(): Buffer^ = buf1 // error g() -def f4(@consume buf: Buffer^): Buffer^ = +def f4(consume buf: Buffer^): Buffer^ = val buf1: Buffer^ = buf def g(): Buffer^ = buf1 // error g() -def f5(@consume buf: Buffer^): Unit = +def f5(consume buf: Buffer^): Unit = val buf1: Buffer^ = buf def g(): Unit = cc(buf1) // error g() -def cc(@consume buf: Buffer^): Unit = () +def cc(consume buf: Buffer^): Unit = () diff --git a/tests/neg-custom-args/captures/reaches.check b/tests/neg-custom-args/captures/reaches.check index bcfbc33c8a9f..70896596593e 100644 --- a/tests/neg-custom-args/captures/reaches.check +++ b/tests/neg-custom-args/captures/reaches.check @@ -1,5 +1,5 @@ --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:22:13 -------------------------------------- -22 | usingFile: f => // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:20:13 -------------------------------------- +20 | usingFile: f => // error | ^ |Found: (f: File^'s1) ->'s2 Unit |Required: File^ => Unit @@ -9,11 +9,11 @@ |where: => refers to a fresh root capability created in method runAll0 when checking argument to parameter f of method usingFile | ^ refers to the universal root capability | cap is a fresh root capability created in anonymous function of type (f: File^'s1): Unit of parameter parameter f² of method $anonfun -23 | cur = (() => f.write()) :: Nil +21 | cur = (() => f.write()) :: Nil | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:32:13 -------------------------------------- -32 | usingFile: f => // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:30:13 -------------------------------------- +30 | usingFile: f => // error | ^ |Found: (f: File^'s3) ->'s4 Unit |Required: File^ => Unit @@ -23,19 +23,19 @@ |where: => refers to a fresh root capability created in method runAll1 when checking argument to parameter f of method usingFile | ^ refers to the universal root capability | cap is a fresh root capability created in anonymous function of type (f: File^'s3): Unit of parameter parameter f² of method $anonfun -33 | cur.set: -34 | (() => f.write()) :: Nil +31 | cur.set: +32 | (() => f.write()) :: Nil | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:44:16 ----------------------------------------------------------- -44 | val cur = Ref[List[Proc]](xs) // error +-- Error: tests/neg-custom-args/captures/reaches.scala:42:16 ----------------------------------------------------------- +42 | val cur = Ref[List[Proc]](xs) // error | ^^^^^^^^^^ | Type variable T of constructor Ref cannot be instantiated to List[() => Unit] since | the part () => Unit of that type captures the root capability `cap`. | | where: => refers to the universal root capability --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:46:35 -------------------------------------- -46 | val next: () => Unit = cur.get.head // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:44:35 -------------------------------------- +44 | val next: () => Unit = cur.get.head // error | ^^^^^^^^^^^^ | Found: () => Unit | Required: () =>² Unit @@ -49,8 +49,8 @@ | cap² is a fresh root capability in the type of value next | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:48:20 -------------------------------------- -48 | cur.set(cur.get.tail: List[Proc]) // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:46:20 -------------------------------------- +46 | cur.set(cur.get.tail: List[Proc]) // error | ^^^^^^^^^^^^ | Found: List[() => Unit] | Required: List[() =>² Unit] @@ -64,15 +64,15 @@ | cap² is a fresh root capability created in method runAll3 | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:54:51 ----------------------------------------------------------- -54 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error +-- Error: tests/neg-custom-args/captures/reaches.scala:52:51 ----------------------------------------------------------- +52 | val id: Id[Proc, Proc] = new Id[Proc, () -> Unit] // error | ^ | Type variable A of constructor Id cannot be instantiated to () => Unit since | that type captures the root capability `cap`. | | where: => refers to the universal root capability --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:59:27 -------------------------------------- -59 | val id: File^ -> File^ = x => x // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:57:27 -------------------------------------- +57 | val id: File^ -> File^ = x => x // error | ^^^^^^ | Found: (x: File^) ->'s5 File^² | Required: File^ -> File^³ @@ -87,8 +87,8 @@ | cap² is a fresh root capability in the type of value id | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:69:38 -------------------------------------- -69 | val leaked = usingFile[File^{id*}]: f => // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:67:38 -------------------------------------- +67 | val leaked = usingFile[File^{id*}]: f => // error | ^ |Found: (f: File^'s6) ->'s7 File^{id*} |Required: File^ => File^{id*} @@ -98,12 +98,12 @@ |where: => refers to a fresh root capability created in value leaked when checking argument to parameter f of method usingFile | ^ refers to the universal root capability | cap is a fresh root capability created in anonymous function of type (f: File^'s6): File^{id*} of parameter parameter f² of method $anonfun -70 | val f1: File^{id*} = id(f) -71 | f1 +68 | val f1: File^{id*} = id(f) +69 | f1 | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:87:10 -------------------------------------- -87 | ps.map((x, y) => compose1(x, y)) // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:85:10 -------------------------------------- +85 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ |Found: (x$1: (A^ ->'s8 A^'s9, A^ ->'s10 A^'s11)^'s12) ->'s13 A^'s14 ->'s15 A^'s16 |Required: ((A ->{ps*} A, A ->{ps*} A)) => A^'s17 ->'s18 A^'s19 @@ -114,8 +114,8 @@ | ^ refers to the universal root capability | | longer explanation available when compiling with `-explain` --- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:90:10 -------------------------------------- -90 | ps.map((x, y) => compose1(x, y)) // error +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reaches.scala:88:10 -------------------------------------- +88 | ps.map((x, y) => compose1(x, y)) // error | ^^^^^^^^^^^^^^^^^^^^^^^ |Found: (x$1: (A^ ->'s20 A^'s21, A^ ->'s22 A^'s23)^'s24) ->'s25 A^'s26 ->'s27 A^'s28 |Required: ((A ->{C} A, A ->{C} A)) => A^'s29 ->'s30 A^'s31 @@ -126,16 +126,16 @@ | ^ refers to the universal root capability | | longer explanation available when compiling with `-explain` --- Error: tests/neg-custom-args/captures/reaches.scala:39:31 ----------------------------------------------------------- -39 | val next: () => Unit = cur.head // error, use +-- Error: tests/neg-custom-args/captures/reaches.scala:37:31 ----------------------------------------------------------- +37 | val next: () => Unit = cur.head // error, use | ^^^^^^^^ | Local reach capability xs* leaks into capture scope of method runAll2. | You could try to abstract the capabilities referred to by xs* in a capset variable. --- Error: tests/neg-custom-args/captures/reaches.scala:62:36 ----------------------------------------------------------- -62 | val leaked = usingFile[File^{id*}]: f => // error: separation +-- Error: tests/neg-custom-args/captures/reaches.scala:60:36 ----------------------------------------------------------- +60 | val leaked = usingFile[File^{id*}]: f => // error: separation | ^ | Local cap created in type of parameter x leaks into capture scope of enclosing function | | where: cap is a fresh root capability created in value id of parameter parameter x of method $anonfun -63 | val f1: File^{id*} = id(f) -64 | f1 +61 | val f1: File^{id*} = id(f) +62 | f1 diff --git a/tests/neg-custom-args/captures/reaches.scala b/tests/neg-custom-args/captures/reaches.scala index d59bc4a7994b..daf326f17f98 100644 --- a/tests/neg-custom-args/captures/reaches.scala +++ b/tests/neg-custom-args/captures/reaches.scala @@ -1,5 +1,3 @@ -import caps.use; -import caps.consume class File: def write(): Unit = ??? @@ -33,7 +31,7 @@ def runAll1[C^](xs: List[() ->{C} Unit]): Unit = cur.set: (() => f.write()) :: Nil -def runAll2(@consume xs: List[Proc]): Unit = +def runAll2(consume xs: List[Proc]): Unit = var cur: List[Proc] = xs while cur.nonEmpty do val next: () => Unit = cur.head // error, use diff --git a/tests/neg-custom-args/captures/reference-cc.check b/tests/neg-custom-args/captures/reference-cc.check new file mode 100644 index 000000000000..dea3e1a5b5e1 --- /dev/null +++ b/tests/neg-custom-args/captures/reference-cc.check @@ -0,0 +1,45 @@ +-- Error: tests/neg-custom-args/captures/reference-cc.scala:42:20 ------------------------------------------------------ +42 | def f = println(c) // error + | ^ + | reference (c : Cap) is not included in the allowed capture set {} + | of the enclosing class A +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:44:27 --------------------------------- +44 | val later = usingLogFile { file => () => file.write(0) } // error + | ^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^ + |Found: (file: java.io.FileOutputStream^'s1) ->'s2 () ->{file} Unit + |Required: java.io.FileOutputStream^ => () ->'s3 Unit + | + |Note that capability file cannot be included in outer capture set 's3. + | + |where: => refers to a fresh root capability created in value later when checking argument to parameter op of method usingLogFile + | ^ refers to the universal root capability + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:47:25 --------------------------------- +47 | val xs = usingLogFile: f => // error + | ^ + |Found: (f: java.io.FileOutputStream^'s4) ->'s5 LzyList[Int]^{f} + |Required: java.io.FileOutputStream^ => LzyList[Int]^'s6 + | + |Note that capability f cannot be included in outer capture set 's6. + | + |where: => refers to a fresh root capability created in value xs when checking argument to parameter op of method usingLogFile + | ^ refers to the universal root capability +48 | LzyList(1, 2, 3).map { x => f.write(x); x * x } + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/reference-cc.scala:58:8 ---------------------------------- +58 | try () => xs.map(f).sum // error TODO improve error message + | ^^^^^^^^^^^^^^^^^^^ + |Found: () => Double + |Required: () =>² Double + | + |Note that capability cap is not included in capture set {cap²} + |because cap in method try$1 is not visible from cap² in enclosing function. + | + |where: => refers to a fresh root capability classified as Control in the type of given instance canThrow$1 + | =>² refers to a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap³} Double of function literal + | cap is a fresh root capability classified as Control in the type of given instance canThrow$1 + | cap² is a fresh root capability created in anonymous function of type (using erased x$1: CanThrow[LimitExceeded]): () => Double when instantiating expected result type () ->{cap³} Double of function literal + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/reference-cc.scala b/tests/neg-custom-args/captures/reference-cc.scala new file mode 100644 index 000000000000..c94ad207bb04 --- /dev/null +++ b/tests/neg-custom-args/captures/reference-cc.scala @@ -0,0 +1,59 @@ +import language.experimental.captureChecking +import scala.compiletime.uninitialized +import java.io.* +import language.experimental.saferExceptions + + +def usingLogFile[T](op: FileOutputStream^ => T): T = + val logFile = FileOutputStream("log") + val result = op(logFile) + logFile.close() + result + +trait LzyList[+A]: + def isEmpty: Boolean + def head: A + def tail: LzyList[A]^{this} + def map[B](f: A => B): LzyList[B]^{f, this} = ??? +object LzyList: + def apply[A](xs: A*): LzyList[A] = ??? + +object LzyNil extends LzyList[Nothing]: + def isEmpty = true + def head = ??? + def tail = ??? + +final class LzyCons[+A](hd: A, tl: () => LzyList[A]^) extends LzyList[A]: + private var forced = false + private var cache: LzyList[A]^{this} = uninitialized + private def force = + if !forced then { cache = tl(); forced = true } + cache + + def isEmpty = false + def head = hd + def tail: LzyList[A]^{this} = force +end LzyCons + +class Cap extends caps.SharedCapability +def test(c: Cap) = + class A: + val x: A = this + def f = println(c) // error + + val later = usingLogFile { file => () => file.write(0) } // error + later() // crash + + val xs = usingLogFile: f => // error + LzyList(1, 2, 3).map { x => f.write(x); x * x } + +class LimitExceeded extends Exception + +def testException = + val limit = 10e+10 + def f(x: Double): Double throws LimitExceeded = + if x < limit then x * x else throw LimitExceeded() + + def escaped(xs: Double*): (() => Double) throws LimitExceeded = + try () => xs.map(f).sum // error TODO improve error message + catch case ex: LimitExceeded => () => -1 diff --git a/tests/neg-custom-args/captures/scoped-caps2.check b/tests/neg-custom-args/captures/scoped-caps2.check new file mode 100644 index 000000000000..1a885b4689d3 --- /dev/null +++ b/tests/neg-custom-args/captures/scoped-caps2.check @@ -0,0 +1,93 @@ +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:5:23 ---------------------------------- +5 | val _: (x: C) => C = b // error + | ^ + | Found: (b : C => C) + | Required: (x: C^) =>² C^² + | + | Note that the existential capture root in C^ + | cannot subsume the capability cap.. + | + | Note that capability cap is not included in capture set {cap²}. + | + | where: => refers to a fresh root capability in the type of value b + | =>² refers to a fresh root capability in the type of value _$1 + | ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² + | cap is a fresh root capability classified as SharedCapability in the type of value b + | cap² is a fresh root capability in the type of value b + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:6:18 ---------------------------------- +6 | val _: C => C = a // error + | ^ + | Found: (a : (x: C) => C) + | Required: C^ =>² C^² + | + | Note that capability cap is not included in capture set {cap²}. + | + | where: => refers to a fresh root capability in the type of value a + | =>² refers to a fresh root capability in the type of value _$2 + | ^ refers to the universal root capability + | ^² refers to a fresh root capability classified as SharedCapability in the type of value _$2 + | cap is a fresh root capability in the type of value a + | cap² is a fresh root capability in the type of value _$2 + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:8:18 ---------------------------------- +8 | val _: C => C = (x: C) => a(x) // error + | ^^^^^^^^^^^^^^ + | Found: (x: C^) ->{a} C^² + | Required: C^ => C^³ + | + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$4. + | + | where: => refers to a fresh root capability in the type of value _$4 + | ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² + | ^³ refers to a fresh root capability classified as SharedCapability in the type of value _$4 + | cap is a root capability associated with the result type of (x: C^): C^² + | cap² is a fresh root capability classified as SharedCapability in the type of value _$4 + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:14:18 --------------------------------- +14 | val _: C -> C = a // error + | ^ + | Found: (a : (x: C) -> C) + | Required: C^ -> C^² + | + | Note that capability cap is not included in capture set {cap²} + | because cap is not visible from cap² in value _$6. + | + | where: ^ refers to the universal root capability + | ^² refers to a fresh root capability classified as SharedCapability in the type of value _$6 + | cap is a root capability associated with the result type of (x: C^): C^³ + | cap² is a fresh root capability classified as SharedCapability in the type of value _$6 + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:15:23 --------------------------------- +15 | val _: (x: C) -> C = (x: C) => b(x) // error + | ^^^^^^^^^^^^^^ + | Found: (x: C^) ->{b} C^² + | Required: (x: C^) -> C^³ + | + | Note that capability b is not included in capture set {}. + | + | where: ^ refers to the universal root capability + | ^² refers to a root capability associated with the result type of (x: C^): C^² + | ^³ refers to a root capability associated with the result type of (x: C^): C^³ + | + | longer explanation available when compiling with `-explain` +-- [E007] Type Mismatch Error: tests/neg-custom-args/captures/scoped-caps2.scala:16:29 --------------------------------- +16 | val _: C -> C = (x: C) => a(x) // error + | ^^^^ + | Found: C^{x} + | Required: C^ + | + | Note that capability x is not included in capture set {cap} + | because (x : C) in enclosing function is not visible from cap in value _$8. + | + | where: ^ refers to a fresh root capability classified as SharedCapability in the type of value _$8 + | cap is a fresh root capability classified as SharedCapability in the type of value _$8 + | + | longer explanation available when compiling with `-explain` diff --git a/tests/neg-custom-args/captures/scoped-caps2.scala b/tests/neg-custom-args/captures/scoped-caps2.scala new file mode 100644 index 000000000000..527debb57378 --- /dev/null +++ b/tests/neg-custom-args/captures/scoped-caps2.scala @@ -0,0 +1,17 @@ +class C extends caps.SharedCapability +def test1(c: C) = + val a: (x: C) => C = ??? + val b: C => C = ??? + val _: (x: C) => C = b // error + val _: C => C = a // error + val _: (x: C) => C = (x: C) => b(x) // OK + val _: C => C = (x: C) => a(x) // error + +def test2(c: C) = + val a: (x: C) -> C = ??? + val b: C -> C = ??? + val _: (x: C) -> C = b // OK + val _: C -> C = a // error + val _: (x: C) -> C = (x: C) => b(x) // error + val _: C -> C = (x: C) => a(x) // error + diff --git a/tests/neg-custom-args/captures/sep-consume.check b/tests/neg-custom-args/captures/sep-consume.check index e44d3235afd6..5967947783ae 100644 --- a/tests/neg-custom-args/captures/sep-consume.check +++ b/tests/neg-custom-args/captures/sep-consume.check @@ -2,7 +2,7 @@ 19 | x.put(42) // error | ^ | Separation failure: Illegal access to (x : Ref^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 18 + | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x @@ -10,11 +10,11 @@ 21 | par(rx, () => x.put(42)) // error | ^ | Separation failure: Illegal access to (x : Ref^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 18 + | consume parameter or was used as a prefix to a consume method on line 18 | and therefore is no longer available. | | where: ^ refers to a fresh root capability classified as Mutable in the type of parameter x -- Error: tests/neg-custom-args/captures/sep-consume.scala:26:16 ------------------------------------------------------- 26 | def foo = bad(f) // error | ^ - | Separation failure: argument to @consume parameter with type (f : () ->{x.rd} Unit) refers to non-local value f + | Separation failure: argument to consume parameter with type (f : () ->{x.rd} Unit) refers to non-local value f diff --git a/tests/neg-custom-args/captures/sep-consume.scala b/tests/neg-custom-args/captures/sep-consume.scala index 7b633b814e88..3caa2713dd95 100644 --- a/tests/neg-custom-args/captures/sep-consume.scala +++ b/tests/neg-custom-args/captures/sep-consume.scala @@ -11,9 +11,9 @@ case class Pair[+A, +B](fst: A, snd: B) // require f and g to be non-interfering def par(f: () => Unit, g: () => Unit): Unit = ??? -def bad(@consume op: () ->{cap.rd} Unit): () => Unit = op +def bad(consume op: () ->{cap.rd} Unit): () => Unit = op -def test2(@consume x: Ref^): Unit = +def test2(consume x: Ref^): Unit = val f: () ->{x.rd} Unit = () => x.get val rx: () => Unit = bad(f) // hides x.rd in the resulting `cap` x.put(42) // error @@ -21,22 +21,22 @@ def test2(@consume x: Ref^): Unit = par(rx, () => x.put(42)) // error par(rx, () => x.get) // ok rd/rd -def test3(@consume x: Ref^): Unit = +def test3(consume x: Ref^): Unit = val f: () ->{x.rd} Unit = () => x.get def foo = bad(f) // error foo() foo() /* -def test4(@consume @use p: Pair[Ref^, Ref^]): Unit = +def test4(consume @use p: Pair[Ref^, Ref^]): Unit = val x: Ref^{p.fst*} = p.fst val y: Ref^{p.snd*} = p.snd badp(Pair(x, y)) println(p.fst.get) -def badp(@consume p: Pair[Ref^, Ref^]): Unit = () +def badp(consume p: Pair[Ref^, Ref^]): Unit = () -def test5(@consume @use p: Pair[Ref^, Ref^]): Unit = +def test5(consume @use p: Pair[Ref^, Ref^]): Unit = badp(p) // ok println(p.fst.get) */ diff --git a/tests/neg-custom-args/captures/sep-lazyListState.check b/tests/neg-custom-args/captures/sep-lazyListState.check index 519d143983bf..5806f9082d58 100644 --- a/tests/neg-custom-args/captures/sep-lazyListState.check +++ b/tests/neg-custom-args/captures/sep-lazyListState.check @@ -2,4 +2,4 @@ 13 | def tail: LazyListIterable[A]^ = tl // error | ^^^^^^^^^^^^^^^^^^^^ | Separation failure: method tail's result type LazyListIterable[A]^ hides non-local this of class class Cons. - | The access must be in a @consume method to allow this. + | The access must be in a consume method to allow this. diff --git a/tests/neg-custom-args/captures/sep-use.scala b/tests/neg-custom-args/captures/sep-use.scala index e89adb0f060e..ec661b15fedc 100644 --- a/tests/neg-custom-args/captures/sep-use.scala +++ b/tests/neg-custom-args/captures/sep-use.scala @@ -1,25 +1,25 @@ -import caps.{cap, consume} +import caps.cap -def test1(@consume io: Object^): Unit = +def test1(consume io: Object^): Unit = val x: () => Unit = () => println(io) println(io) // error println(x) // ok -def test2(@consume io: Object^): Unit = +def test2(consume io: Object^): Unit = def x: () => Unit = () => println(io) // error println(io) // error println(x) // ok -def test3(@consume io: Object^): Unit = +def test3(consume io: Object^): Unit = def xx: (y: Int) => Unit = _ => println(io) // error println(io) // error println(xx(2)) // ok -def test4(@consume io: Object^): Unit = +def test4(consume io: Object^): Unit = def xxx(y: Int): Object^ = io // error println(io) // error diff --git a/tests/neg-custom-args/captures/sep-use2.check b/tests/neg-custom-args/captures/sep-use2.check index d6379639f0bc..8fec0e3bdd83 100644 --- a/tests/neg-custom-args/captures/sep-use2.check +++ b/tests/neg-custom-args/captures/sep-use2.check @@ -14,7 +14,7 @@ 12 | val x4: Object^ = // error | ^^^^^^^ | Separation failure: value x4's type Object^ hides parameter f. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sep-use2.scala:16:10 ---------------------------------------------------------- 16 | def cc: Object^ = c // error | ^^^^^^^ @@ -61,10 +61,10 @@ |where: ^ refers to a fresh root capability in the type of parameter c | ^² refers to a fresh root capability created in value x4 when checking argument to parameter v1 of method apply -- Error: tests/neg-custom-args/captures/sep-use2.scala:23:10 ---------------------------------------------------------- -23 | val x4: Object^ = // error: ^ hides f*, needs @consume +23 | val x4: Object^ = // error: ^ hides f*, needs consume | ^^^^^^^ | Separation failure: value x4's type Object^ hides parameter f. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sep-use2.scala:28:8 ----------------------------------------------------------- 28 | { f(c) } // error | ^ @@ -83,7 +83,7 @@ |where: ^ refers to a fresh root capability in the type of parameter c | ^² refers to a fresh root capability created in value x4 when checking argument to parameter v1 of method apply -- Error: tests/neg-custom-args/captures/sep-use2.scala:27:10 ---------------------------------------------------------- -27 | val x4: Object^ = // error: ^ hides f* which refers to c, so c needs @consume +27 | val x4: Object^ = // error: ^ hides f* which refers to c, so c needs consume | ^^^^^^^ | Separation failure: value x4's type Object^ hides parameter c. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/sep-use2.scala b/tests/neg-custom-args/captures/sep-use2.scala index 088984fab0c6..9ce8a1ade72f 100644 --- a/tests/neg-custom-args/captures/sep-use2.scala +++ b/tests/neg-custom-args/captures/sep-use2.scala @@ -1,7 +1,7 @@ -import caps.consume -def test1(@consume c: Object^, f: (x: Object^) => Object^) = + +def test1(consume c: Object^, f: (x: Object^) => Object^) = def cc: Object^ = c // error val x1 = { f(cc) } // ok @@ -12,19 +12,19 @@ def test1(@consume c: Object^, f: (x: Object^) => Object^) = val x4: Object^ = // error { f(c) } // error -def test2(@consume c: Object^, f: (x: Object^) ->{c} Object^) = +def test2(consume c: Object^, f: (x: Object^) ->{c} Object^) = def cc: Object^ = c // error val x1 = { f(cc) } // error val x4: Object^ = // ^ hides just c, since the Object^ in the result of `f` is existential { f(c) } // error // error -def test3(@consume c: Object^, f: Object^ ->{c} Object^) = - val x4: Object^ = // error: ^ hides f*, needs @consume +def test3(consume c: Object^, f: Object^ ->{c} Object^) = + val x4: Object^ = // error: ^ hides f*, needs consume { f(c) } // error -def test4(c: Object^, @consume f: Object^ ->{c} Object^) = - val x4: Object^ = // error: ^ hides f* which refers to c, so c needs @consume +def test4(c: Object^, consume f: Object^ ->{c} Object^) = + val x4: Object^ = // error: ^ hides f* which refers to c, so c needs consume { f(c) } // error diff --git a/tests/neg-custom-args/captures/sepchecks2.check b/tests/neg-custom-args/captures/sepchecks2.check index e7b8dcbf038f..5529c2a6d1c8 100644 --- a/tests/neg-custom-args/captures/sepchecks2.check +++ b/tests/neg-custom-args/captures/sepchecks2.check @@ -55,9 +55,9 @@ 30 | val x: (Object^, Object^{c}) = (d, c) // error | ^^^^^^^^^^^^^^^^^^^^^ | Separation failure: value x's type (Object^, Object^{c}) hides parameter d. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks2.scala:33:9 --------------------------------------------------------- 33 | val x: (Object^, Object^) = (c, d) // error | ^^^^^^^^^^^^^^^^^^ | Separation failure: value x's type (Object^, Object^) hides parameters c and d. - | The parameters need to be annotated with @consume to allow this. + | The parameters need to be annotated with consume to allow this. diff --git a/tests/neg-custom-args/captures/sepchecks2.scala b/tests/neg-custom-args/captures/sepchecks2.scala index 34ca3a56a243..d3310fc8b3ca 100644 --- a/tests/neg-custom-args/captures/sepchecks2.scala +++ b/tests/neg-custom-args/captures/sepchecks2.scala @@ -1,11 +1,11 @@ -import caps.consume + def foo(xs: List[() => Unit], y: Object^) = ??? def bar(x: (Object^, Object^)): Unit = ??? -def Test(@consume c: Object^) = +def Test(consume c: Object^) = val xs: List[() => Unit] = (() => println(c)) :: Nil println(c) // error @@ -14,10 +14,10 @@ def Test2(c: Object^, d: Object^): Unit = val x1: (Object^, Object^) = (c, c) // error val x2: (Object^, Object^{d}) = (d, d) // error -def Test3(@consume c: Object^, @consume d: Object^) = +def Test3(consume c: Object^, consume d: Object^) = val x: (Object^, Object^) = (c, d) // ok -def Test4(@consume c: Object^, @consume d: Object^) = +def Test4(consume c: Object^, consume d: Object^) = val x: (Object^, Object^{c}) = (d, c) // ok def Test5(c: Object^, d: Object^): Unit = diff --git a/tests/neg-custom-args/captures/sepchecks3.scala b/tests/neg-custom-args/captures/sepchecks3.scala index 8cc7d705b42b..abfd263b0ff8 100644 --- a/tests/neg-custom-args/captures/sepchecks3.scala +++ b/tests/neg-custom-args/captures/sepchecks3.scala @@ -1,5 +1,5 @@ -import caps.consume + def foo(xs: List[() => Unit], y: Object^) = ??? @@ -7,6 +7,6 @@ def bar(x: (Object^, Object^)): Unit = ??? def Test(c: Object^): Object^ = c // error -def Test2(@consume c: Object^): Object^ = c // ok +def Test2(consume c: Object^): Object^ = c // ok def Test3(c: Object^): List[Object^] = c :: Nil // error diff --git a/tests/neg-custom-args/captures/sepchecks4.check b/tests/neg-custom-args/captures/sepchecks4.check index 7b587363d1cd..64ebb04239d5 100644 --- a/tests/neg-custom-args/captures/sepchecks4.check +++ b/tests/neg-custom-args/captures/sepchecks4.check @@ -2,12 +2,12 @@ 8 | val x: () => Unit = () => println(io) // error | ^^^^^^^^^^ | Separation failure: value x's type () => Unit hides parameter io. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks4.scala:7:25 --------------------------------------------------------- 7 |def bad(io: Object^): () => Unit = // error | ^^^^^^^^^^ | Separation failure: method bad's result type () => Unit hides parameter io. - | The parameter needs to be annotated with @consume to allow this. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks4.scala:12:6 --------------------------------------------------------- 12 | par(() => println(io))(() => println(io)) // error // (1) | ^^^^^^^^^^^^^^^^^ diff --git a/tests/neg-custom-args/captures/sepchecks4.scala b/tests/neg-custom-args/captures/sepchecks4.scala index d44b31ca02dc..285c5405e215 100644 --- a/tests/neg-custom-args/captures/sepchecks4.scala +++ b/tests/neg-custom-args/captures/sepchecks4.scala @@ -12,5 +12,5 @@ def test(io: Object^): Unit = par(() => println(io))(() => println(io)) // error // (1) val f = bad(io) - par(f)(() => println(io)) // no error, but it is equivalent to (1) and should failimport caps.consume + par(f)(() => println(io)) // no error, but it is equivalent to (1) and should fail diff --git a/tests/neg-custom-args/captures/sepchecks5.check b/tests/neg-custom-args/captures/sepchecks5.check index 63ec3bc73431..9f76ef21f46d 100644 --- a/tests/neg-custom-args/captures/sepchecks5.check +++ b/tests/neg-custom-args/captures/sepchecks5.check @@ -1,18 +1,18 @@ -- Error: tests/neg-custom-args/captures/sepchecks5.scala:12:37 -------------------------------------------------------- 12 |def bad(io: Object^): () => Unit = f(io) // error | ^^ - | Separation failure: argument to @consume parameter with type (io : Object^) refers to parameter io. - | The parameter needs to be annotated with @consume to allow this. + | Separation failure: argument to consume parameter with type (io : Object^) refers to parameter io. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks5.scala:19:13 -------------------------------------------------------- 19 | val f2 = g(io) // error | ^^ - | Separation failure: argument to @consume parameter with type (io : Object^) refers to parameter io. - | The parameter needs to be annotated with @consume to allow this. + | Separation failure: argument to consume parameter with type (io : Object^) refers to parameter io. + | The parameter needs to be annotated with consume to allow this. -- Error: tests/neg-custom-args/captures/sepchecks5.scala:20:24 -------------------------------------------------------- 20 | par(f2)(() => println(io)) // error | ^^ | Separation failure: Illegal access to (io : Object^), which was passed to a - | @consume parameter or was used as a prefix to a @consume method on line 19 + | consume parameter or was used as a prefix to a consume method on line 19 | and therefore is no longer available. | | where: ^ refers to a fresh root capability in the type of parameter io diff --git a/tests/neg-custom-args/captures/sepchecks5.scala b/tests/neg-custom-args/captures/sepchecks5.scala index 9a16051e64bd..82b7f17108f0 100644 --- a/tests/neg-custom-args/captures/sepchecks5.scala +++ b/tests/neg-custom-args/captures/sepchecks5.scala @@ -1,13 +1,13 @@ -import caps.{cap, consume} +import caps.cap import language.future import language.experimental.captureChecking def par(op1: () => Unit)(op2: () => Unit): Unit = () -def f(@consume io: Object^): () => Unit = +def f(consume io: Object^): () => Unit = () => println(io) -def g(@consume io: Object^): () => Unit = f(io) // ok +def g(consume io: Object^): () => Unit = f(io) // ok def bad(io: Object^): () => Unit = f(io) // error diff --git a/tests/neg-custom-args/captures/unsound-reach-3.scala b/tests/neg-custom-args/captures/unsound-reach-3.scala index 46ed469a308e..56b39097b1ca 100644 --- a/tests/neg-custom-args/captures/unsound-reach-3.scala +++ b/tests/neg-custom-args/captures/unsound-reach-3.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking -import caps.consume + trait File: def close(): Unit @@ -8,9 +8,9 @@ trait File: def withFile[R](path: String)(op: File^ => R): R = ??? trait Foo[+X]: - def use(@consume x: File^): X + def use(consume x: File^): X class Bar extends Foo[File^]: // error - def use(@consume x: File^): File^ = x // error override + def use(consume x: File^): File^ = x // error override def bad(): Unit = val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). diff --git a/tests/neg-custom-args/captures/unsound-reach-4.check b/tests/neg-custom-args/captures/unsound-reach-4.check index 56e1a0cc1548..573e9a31d068 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.check +++ b/tests/neg-custom-args/captures/unsound-reach-4.check @@ -20,7 +20,7 @@ | | longer explanation available when compiling with `-explain` -- [E164] Declaration Error: tests/neg-custom-args/captures/unsound-reach-4.scala:17:6 --------------------------------- -17 | def use(@consume x: F): File^ = x // error @consume override +17 | def use(consume x: F): File^ = x // error consume override | ^ | error overriding method use in trait Foo of type (x: File^): File^; | method use of type (@consume x: File^): File^² has incompatible type diff --git a/tests/neg-custom-args/captures/unsound-reach-4.scala b/tests/neg-custom-args/captures/unsound-reach-4.scala index 715dfcc90ef8..c6ad721213c2 100644 --- a/tests/neg-custom-args/captures/unsound-reach-4.scala +++ b/tests/neg-custom-args/captures/unsound-reach-4.scala @@ -2,7 +2,7 @@ import language.experimental.captureChecking; -import caps.consume + trait File: def close(): Unit @@ -14,7 +14,7 @@ type F = File^ trait Foo[+X]: def use(x: F): X class Bar extends Foo[File^]: // error - def use(@consume x: F): File^ = x // error @consume override + def use(consume x: F): File^ = x // error consume override def bad(): Unit = val backdoor: Foo[File^] = new Bar // error (follow-on, since the parent Foo[File^] of bar is illegal). diff --git a/tests/neg-custom-args/captures/unsound-reach-6.check b/tests/neg-custom-args/captures/unsound-reach-6.check index c6f45c15e62b..b9e9b287dace 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.check +++ b/tests/neg-custom-args/captures/unsound-reach-6.check @@ -22,11 +22,11 @@ | Local reach capability xs* leaks into capture scope of method f. | You could try to abstract the capabilities referred to by xs* in a capset variable. -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:11:14 --------------------------------------------------- -11 | val z = f(ys) // error @consume failure +11 | val z = f(ys) // error consume failure | ^^ | Local reach capability ys* leaks into capture scope of method test. | You could try to abstract the capabilities referred to by ys* in a capset variable. -- Error: tests/neg-custom-args/captures/unsound-reach-6.scala:19:14 --------------------------------------------------- -19 | val z = f(ys) // error @consume failure +19 | val z = f(ys) // error consume failure | ^^ - |Separation failure: argument to @consume parameter with type List[() ->{io} Unit] refers to non-local parameter io + |Separation failure: argument to consume parameter with type List[() ->{io} Unit] refers to non-local parameter io diff --git a/tests/neg-custom-args/captures/unsound-reach-6.scala b/tests/neg-custom-args/captures/unsound-reach-6.scala index 4643950d78d0..0d737828d466 100644 --- a/tests/neg-custom-args/captures/unsound-reach-6.scala +++ b/tests/neg-custom-args/captures/unsound-reach-6.scala @@ -1,14 +1,14 @@ -import caps.consume + class IO -def f(@consume xs: List[() => Unit]): () => Unit = () => +def f(consume xs: List[() => Unit]): () => Unit = () => println(xs.head) // error def test(io: IO^)(ys: List[() ->{io} Unit]) = val x = () => - val z = f(ys) // error @consume failure + val z = f(ys) // error consume failure z() val _: () -> Unit = x // error () @@ -16,7 +16,7 @@ def test(io: IO^)(ys: List[() ->{io} Unit]) = def test(io: IO^) = def ys: List[() ->{io} Unit] = ??? val x = () => - val z = f(ys) // error @consume failure + val z = f(ys) // error consume failure z() val _: () -> Unit = x // error () diff --git a/tests/neg/localReaches.scala b/tests/neg/localReaches.scala index d0935e2d491f..5bf1b9a26303 100644 --- a/tests/neg/localReaches.scala +++ b/tests/neg/localReaches.scala @@ -1,6 +1,6 @@ import language.experimental.captureChecking // no separation checking -import caps.consume + def localReach() = val xs: List[() => Unit] = ??? diff --git a/tests/new/test.scala b/tests/new/test.scala index 2904592cc6b2..23ac0de47b6f 100644 --- a/tests/new/test.scala +++ b/tests/new/test.scala @@ -1 +1,5 @@ -def test[T] = println(T) +class Cap extends caps.ExclusiveCapability + +def test(consume x: Cap) = ??? + +def impl(using consume x: Cap) = ??? diff --git a/tests/pos-custom-args/captures/capt-depfun.scala b/tests/pos-custom-args/captures/capt-depfun.scala index fb6866459aba..359c49e9110f 100644 --- a/tests/pos-custom-args/captures/capt-depfun.scala +++ b/tests/pos-custom-args/captures/capt-depfun.scala @@ -1,5 +1,5 @@ import annotation.retains -import caps.consume + class C type Cap = C @retains[caps.cap.type] @@ -11,7 +11,7 @@ class STR(s: String) val aa: ((x: Cap) -> STR @retains[x.type]) = (x: Cap) => STR("") -def f(@consume y: Cap, z: Cap): STR @retains[caps.cap.type] = +def f(consume y: Cap, z: Cap): STR @retains[caps.cap.type] = val a: ((x: Cap) -> STR @retains[x.type]) = (x: Cap) => STR("") val b = a(y) val c: STR @retains[y.type] = b diff --git a/tests/pos-custom-args/captures/capt-depfun2.scala b/tests/pos-custom-args/captures/capt-depfun2.scala index 101ea6bb94e1..4451deb27c76 100644 --- a/tests/pos-custom-args/captures/capt-depfun2.scala +++ b/tests/pos-custom-args/captures/capt-depfun2.scala @@ -1,10 +1,10 @@ import annotation.retains -import caps.consume + class C type Cap = C @retains[caps.cap.type] class STR -def f(@consume y: Cap, @consume z: Cap) = +def f(consume y: Cap, consume z: Cap) = def g(): C @retains[y.type | z.type] = ??? val ac: ((x: Cap) -> Array[STR @retains[x.type]]) = ??? val dc: Array[? >: STR <: STR^]^{y, z} = ac(g()) // needs to be inferred diff --git a/tests/pos-custom-args/captures/cc-this.scala b/tests/pos-custom-args/captures/cc-this.scala index 6aa21a7a6c70..719a48130c6c 100644 --- a/tests/pos-custom-args/captures/cc-this.scala +++ b/tests/pos-custom-args/captures/cc-this.scala @@ -1,12 +1,12 @@ -import caps.consume + import caps.unsafe.unsafeAssumeSeparate class Cap extends caps.SharedCapability def eff(using Cap): Unit = () -def test(using @consume cc: Cap) = +def test(using consume cc: Cap) = class C(val x: () => Int): val y: C^ = this diff --git a/tests/pos-custom-args/captures/lazyref.scala b/tests/pos-custom-args/captures/lazyref.scala index 6b5d62c743b6..0723aef95271 100644 --- a/tests/pos-custom-args/captures/lazyref.scala +++ b/tests/pos-custom-args/captures/lazyref.scala @@ -1,5 +1,5 @@ -import caps.consume + class Cap extends caps.SharedCapability @@ -14,7 +14,7 @@ def map[A, B](ref: LazyRef[A]^, f: A => B): LazyRef[B]^{f, ref} = def mapc[A, B]: (ref: LazyRef[A]^, f: A => B) => LazyRef[B]^{f, ref} = (ref1, f1) => map[A, B](ref1, f1) -def test(@consume cap1: Cap, @consume cap2: Cap) = +def test(consume cap1: Cap, consume cap2: Cap) = def f(x: Int) = if cap1 == cap1 then x else 0 def g(x: Int) = if cap2 == cap2 then x else 0 val ref1 = LazyRef(() => f(0)) diff --git a/tests/pos-custom-args/captures/reaches.scala b/tests/pos-custom-args/captures/reaches.scala index eae4c3e8a73c..348346ad1c3f 100644 --- a/tests/pos-custom-args/captures/reaches.scala +++ b/tests/pos-custom-args/captures/reaches.scala @@ -1,6 +1,3 @@ - -import caps.{use, consume} - class C def f(xs: List[C^]) = val y = xs @@ -37,7 +34,7 @@ def cons(x: Proc, xs: List[Proc]): List[() ->{x, xs*} Unit] = val y = x :: xs y -def addOneProc(@consume xs: List[Proc]): List[Proc] = +def addOneProc(consume xs: List[Proc]): List[Proc] = val x: Proc = () => println("hello") val result: List[() ->{x, xs*} Unit] = x :: xs result // OK, we can widen () ->{x, xs*} Unit to cap here. @@ -45,7 +42,7 @@ def addOneProc(@consume xs: List[Proc]): List[Proc] = def compose1[A, B, C](f: A => B, g: B => C): A ->{f, g} C = z => g(f(z)) -def compose2[A, B, C](@consume f: A => B, @consume g: B => C): A => C = +def compose2[A, B, C](consume f: A => B, consume g: B => C): A => C = z => g(f(z)) //def mapCompose[A](ps: List[(A => A, A => A)]): List[A ->{ps*} A] = diff --git a/tests/pos-custom-args/captures/reference-cc.scala b/tests/pos-custom-args/captures/reference-cc.scala new file mode 100644 index 000000000000..ea0dbf6860aa --- /dev/null +++ b/tests/pos-custom-args/captures/reference-cc.scala @@ -0,0 +1,8 @@ +import language.experimental.captureChecking +import java.io.* + +def usingLogFile[T](op: FileOutputStream^ => T): T = + val logFile = FileOutputStream("log") + val result = op(logFile) + logFile.close() + result \ No newline at end of file diff --git a/tests/pos-custom-args/captures/sep-pairs.scala b/tests/pos-custom-args/captures/sep-pairs.scala index 17cb8eb9aa6c..ad22df412e0d 100644 --- a/tests/pos-custom-args/captures/sep-pairs.scala +++ b/tests/pos-custom-args/captures/sep-pairs.scala @@ -1,5 +1,5 @@ import caps.Mutable -import caps.{cap, consume, use} +import caps.cap class Ref extends Mutable: var x = 0 @@ -14,19 +14,19 @@ def mkPair: Pair[Ref^, Ref^] = val p_exact: Pair[Ref^{r1}, Ref^{r2}] = Pair(r1, r2) p_exact -def copyPair[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] = +def copyPair[C^, D^](consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] = val x: Ref^{C} = p.fst val y: Ref^{D} = p.snd Pair[Ref^{C}, Ref^{D}](x, y) /* TODO: The following variants don't work -def copyPair1[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] = +def copyPair1[C^, D^](consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^{C}, Ref^{D}] = val x: Ref^{C} = p.fst val y: Ref^{D} = p.snd Pair(x, y) -def copyPair2[C^, D^](@consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^, Ref^] = +def copyPair2[C^, D^](consume p: Pair[Ref^{C}, Ref^{D}]): Pair[Ref^, Ref^] = val x: Ref^{C} = p.fst val y: Ref^{D} = p.snd Pair(x, y) diff --git a/tests/pos-custom-args/captures/skolems2.scala b/tests/pos-custom-args/captures/skolems2.scala index 53fbe935e362..754f80b9a36f 100644 --- a/tests/pos-custom-args/captures/skolems2.scala +++ b/tests/pos-custom-args/captures/skolems2.scala @@ -1,8 +1,8 @@ -import caps.consume + import caps.unsafe.unsafeAssumeSeparate -def Test(@consume c: Object^, @consume f: Object^ => Object^) = +def Test(consume c: Object^, consume f: Object^ => Object^) = def cc: Object^ = unsafeAssumeSeparate(c) val x1 = { f(cc) } @@ -13,7 +13,7 @@ def Test(@consume c: Object^, @consume f: Object^ => Object^) = val x4: Object^ = { unsafeAssumeSeparate(f)(cc) } -def Test2(@consume c: Object^, @consume f: Object^ => Object^) = +def Test2(consume c: Object^, consume f: Object^ => Object^) = def cc(): Object^ = unsafeAssumeSeparate(c) val x1 = { f(cc()) } diff --git a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala index 9effb37d5278..a546d5def0d9 100644 --- a/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala +++ b/tests/run-tasty-inspector/stdlibExperimentalDefinitions.scala @@ -39,7 +39,6 @@ val experimentalDefinitionInLibrary = Set( "scala.caps.ExclusiveCapability", "scala.caps.Mutable", "scala.caps.Read", - "scala.caps.consume", "scala.caps.internal", "scala.caps.internal$", "scala.caps.cap",