Skip to content

Commit f5b8125

Browse files
committed
Go back to "capability"
... instead of "ability". Two reasons: - it's more standard - it's also more correct. According to https://writingexplained.org/capability-vs-ability-difference#When_to_Use_Capability a capability is a yes or no proposition, whereas an ability is a matter of degree.
1 parent 6e50277 commit f5b8125

File tree

4 files changed

+35
-37
lines changed

4 files changed

+35
-37
lines changed

compiler/src/dotty/tools/dotc/transform/TypeUtils.scala

Lines changed: 1 addition & 1 deletion
Original file line numberDiff line numberDiff line change
@@ -28,7 +28,7 @@ object TypeUtils {
2828
* derives from Exception but not from RuntimeException. According to
2929
* that definition Throwable is unchecked. That makes sense since you should
3030
* neither throw nor catch `Throwable` anyway, so we should not define
31-
* an ability to do so.
31+
* a capability to do so.
3232
*/
3333
def isCheckedException(using Context): Boolean =
3434
self.derivesFrom(defn.ExceptionClass)

docs/docs/reference/experimental/canthrow.md

Lines changed: 28 additions & 30 deletions
Original file line numberDiff line numberDiff line change
@@ -1,6 +1,6 @@
11
---
22
layout: doc-page
3-
title: CanThrow Abilities
3+
title: CanThrow Capabilities
44
author: Martin Odersky
55
---
66

@@ -42,7 +42,7 @@ So the dilemma is that exceptions are easy to use only as long as we forgo stati
4242

4343
However, a programming language is not a framework; it has to cater also for those applications that do not fit the framework's use cases. So there's still a strong motivation for getting exception checking right.
4444

45-
## From Effects To Abilities
45+
## From Effects To Capabilities
4646

4747
Why does `map` work so poorly with Java's checked exception model? It's because
4848
`map`'s signature limits function arguments to not throw checked exceptions. We could try to come up with a more polymorphic formulation of `map`. For instance, it could look like this:
@@ -53,22 +53,20 @@ This assumes a type `A throws E` to indicate computations of type `A` that can t
5353

5454
But there is a way to avoid the ceremony. Instead of concentrating on possible _effects_ such as "this code might throw an exception", concentrate on _capabilities_ such as "this code needs the capability to throw an exception". From a standpoint of expressiveness this is quite similar. But capabilities can be expressed as parameters whereas traditionally effects are expressed as some addition to result values. It turns out that this can make a big difference!
5555

56-
Going to the root of the word _capability_, it means "being _able_ to do something", so the "cap" prefix is really just a filler. Following Conor McBride, we will use the name _ability_ from now on.
56+
## The CanThrow Cabability
5757

58-
## The CanThrow Ability
59-
60-
In the _effects as abilities_ model, an effect is expressed as an (implicit) parameter of a certain type. For exceptions we would expect parameters of type
58+
In the _effects as capabilities_ model, an effect is expressed as an (implicit) parameter of a certain type. For exceptions we would expect parameters of type
6159
`CanThrow[E]` where `E` stands for the exception that can be thrown. Here is the definition of `CanThrow`:
6260
```scala
6361
erased class CanThrow[-E <: Exception]
6462
```
65-
This shows another experimental Scala feature: [erased definitions](./erased-defs). Roughly speaking, values of an erased class do not generate runtime code; they are erased before code generation. This means that all `CanThrow` abilities are compile-time only artifacts; they do not have a runtime footprint.
63+
This shows another experimental Scala feature: [erased definitions](./erased-defs). Roughly speaking, values of an erased class do not generate runtime code; they are erased before code generation. This means that all `CanThrow` capabilities are compile-time only artifacts; they do not have a runtime footprint.
6664

67-
Now, if the compiler sees a `throw Exc()` construct where `Exc` is a checked exception, it will check that there is an ability of type `CanThrow[Exc]` that can be summoned as a given. It's a compile-time error if that's not the case.
65+
Now, if the compiler sees a `throw Exc()` construct where `Exc` is a checked exception, it will check that there is a capability of type `CanThrow[Exc]` that can be summoned as a given. It's a compile-time error if that's not the case.
6866

69-
How can the ability be produced? There are several possibilities:
67+
How can the capability be produced? There are several possibilities:
7068

71-
Most often, the ability is produced by having a using clause `(using CanThrow[Exc])` in some enclosing scope. This roughly corresponds to a `throws` clause
69+
Most often, the capability is produced by having a using clause `(using CanThrow[Exc])` in some enclosing scope. This roughly corresponds to a `throws` clause
7270
in Java. The analogy is even stronger since alongside `CanThrow` there is also the following type alias defined in the `scala` package:
7371
```scala
7472
infix type $throws[R, +E <: Exception] = CanThrow[E] ?=> R
@@ -96,7 +94,7 @@ can alternatively be expressed like this:
9694
```scala
9795
def m(x: T): U throws E1 | E2
9896
```
99-
The `CanThrow`/`throws` combo essentially propagates the `CanThrow` requirement outwards. But where are these abilities created in the first place? That's in the `try` expression. Given a `try` like this:
97+
The `CanThrow`/`throws` combo essentially propagates the `CanThrow` requirement outwards. But where are these capabilities created in the first place? That's in the `try` expression. Given a `try` like this:
10098

10199
```scala
102100
try
@@ -106,7 +104,7 @@ catch
106104
...
107105
case exN: ExN => handlerN
108106
```
109-
the compiler generates abilities for `CanThrow[Ex1]`, ..., `CanThrow[ExN]` that are in scope as givens in `body`. It does this by augmenting the `try` roughly as follows:
107+
the compiler generates capabilities for `CanThrow[Ex1]`, ..., `CanThrow[ExN]` that are in scope as givens in `body`. It does this by augmenting the `try` roughly as follows:
110108
```scala
111109
try
112110
erased given CanThrow[Ex1] = ???
@@ -136,8 +134,8 @@ You'll get this error message:
136134
```
137135
9 | if x < limit then x * x else throw LimitExceeded()
138136
| ^^^^^^^^^^^^^^^^^^^^^
139-
|The ability to throw exception LimitExceeded is missing.
140-
|The ability can be provided by one of the following:
137+
|The capability to throw exception LimitExceeded is missing.
138+
|The capability can be provided by one of the following:
141139
| - A using clause `(using CanThrow[LimitExceeded])`
142140
| - A `throws` clause in a result type such as `X throws LimitExceeded`
143141
| - an enclosing `try` that catches LimitExceeded
@@ -146,7 +144,7 @@ You'll get this error message:
146144
|
147145
| import unsafeExceptions.canThrowAny
148146
```
149-
As the error message implies, you have to declare that `f` needs the ability to throw a `LimitExceeded` exception. The most concise way to do so is to add a `throws` clause:
147+
As the error message implies, you have to declare that `f` needs the capability to throw a `LimitExceeded` exception. The most concise way to do so is to add a `throws` clause:
150148
```scala
151149
def f(x: Double): Double throws LimitExceeded =
152150
if x < limit then x * x else throw LimitExceeded()
@@ -175,26 +173,26 @@ Everything typechecks and works as expected. But wait - we have called `map` wit
175173
println(xs.map(x => f(x)(using ctl)).sum)
176174
catch case ex: LimitExceeded => println("too large")
177175
```
178-
The `CanThrow[LimitExceeded]` ability is passed in a synthesized `using` clause to `f`, since `f` requires it. Then the resulting closure is passed to `map`. The signature of `map` does not have to account for effects. It takes a closure as always, but that
179-
closure may refer to abilities in its free variables. This means that `map` is
176+
The `CanThrow[LimitExceeded]` capability is passed in a synthesized `using` clause to `f`, since `f` requires it. Then the resulting closure is passed to `map`. The signature of `map` does not have to account for effects. It takes a closure as always, but that
177+
closure may refer to capabilities in its free variables. This means that `map` is
180178
already effect polymorphic even though we did not change its signature at all.
181-
So the takeaway is that the effects as abilities model naturally provides for effect polymorphism whereas this is something that other approaches struggle with.
179+
So the takeaway is that the effects as capabilities model naturally provides for effect polymorphism whereas this is something that other approaches struggle with.
182180

183181
## Gradual Typing Via Imports
184182

185183
Another advantage is that the model allows a gradual migration from current unchecked exceptions to safer exceptions. Imagine for a moment that `experimental.saferExceptions` is turned on everywhere. There would be lots of code that breaks since functions have not yet been properly annotated with `throws`. But it's easy to create an escape hatch that lets us ignore the breakages for a while: simply add the import
186184
```scala
187185
import scala.unsafeExceptions.canThrowAny
188186
```
189-
This will provide the `CanThrow` ability for any exception, and thereby allow
187+
This will provide the `CanThrow` capability for any exception, and thereby allow
190188
all throws and all other calls, no matter what the current state of `throws` declarations is. Here's the
191189
definition of `canThrowAny`:
192190
```scala
193191
package scala
194192
object unsafeExceptions:
195193
given canThrowAny: CanThrow[Exception] = ???
196194
```
197-
Of course, defining a global ability like this amounts to cheating. But the cheating is useful for gradual typing. The import could be used to migrate existing code, or to
195+
Of course, defining a global capability like this amounts to cheating. But the cheating is useful for gradual typing. The import could be used to migrate existing code, or to
198196
enable more fluid explorations of code without regard for complete exception safety. At the end of these migrations or explorations the import should be removed.
199197

200198
## Scope Of the Extension
@@ -203,24 +201,24 @@ To summarize, the extension for safer exception checking consists of the followi
203201

204202
- It adds to the standard library the class `scala.CanThrow`, the type `scala.$throws`, and the `scala.unsafeExceptions` object, as they were described above.
205203
- It adds some desugaring rules ro rewrite `throws` types to cascaded `$throws` types.
206-
- It augments the type checking of `throw` by _demanding_ a `CanThrow` ability or the thrown exception.
207-
- It augments the type checking of `try` by _providing_ `CanThrow` abilities for every caught exception.
204+
- It augments the type checking of `throw` by _demanding_ a `CanThrow` capability or the thrown exception.
205+
- It augments the type checking of `try` by _providing_ `CanThrow` capabilities for every caught exception.
208206

209207
That's all. It's quite remarkable that one can do exception checking in this way without any special additions to the type system. We just need regular givens and context functions. Any runtime overhead is eliminated using `erased`.
210208

211209
## Caveats
212210

213-
Our ability model allows to declare and check the thrown exceptions of first-order code. But as it stands, it does not give us enough mechanism to enforce the _absence_ of
214-
abilities for arguments to higher-order functions. Consider a variant `pureMap`
211+
Our capability model allows to declare and check the thrown exceptions of first-order code. But as it stands, it does not give us enough mechanism to enforce the _absence_ of
212+
capabilities for arguments to higher-order functions. Consider a variant `pureMap`
215213
of `map` that should enforce that its argument does not throw exceptions or have any other effects (maybe because wants to reorder computations transparently). Right now
216214
we cannot enforce that since the function argument to `pureMap` can capture arbitrary
217-
abilities in its free variables without them showing up in its type. One possible way to
218-
address this would be to introduce a pure function type (maybe written `A -> B`). Pure functions are not allowed to close over abilities. Then `pureMap` could be written
215+
capabilities in its free variables without them showing up in its type. One possible way to
216+
address this would be to introduce a pure function type (maybe written `A -> B`). Pure functions are not allowed to close over capabilities. Then `pureMap` could be written
219217
like this:
220218
```
221219
def pureMap(f: A -> B): List[B]
222220
```
223-
Another area where the lack of purity requirements shows up is when abilities escape from bounded scopes. Consider the following function
221+
Another area where the lack of purity requirements shows up is when capabilities escape from bounded scopes. Consider the following function
224222
```scala
225223
def escaped(xs: Double*): () => Int =
226224
try () => xs.map(f).sum
@@ -240,16 +238,16 @@ But if you try to call `escaped` like this
240238
val g = escaped(1, 2, 1000000000)
241239
g()
242240
```
243-
the result will be a `LimitExceeded` exception thrown at the second line where `g` is called. What's missing is that `try` should enforce that the abilities it generates do not escape as free variables in the result of its body. It makes sense to describe such scoped effects as _ephemeral abilities_ - they have lifetimes that cannot be extended to delayed code in a lambda.
241+
the result will be a `LimitExceeded` exception thrown at the second line where `g` is called. What's missing is that `try` should enforce that the capabilities it generates do not escape as free variables in the result of its body. It makes sense to describe such scoped effects as _ephemeral capabilities_ - they have lifetimes that cannot be extended to delayed code in a lambda.
244242

245243

246244
# Outlook
247245

248-
We are working on a new class of type system that supports ephemeral abilities by tracking the free variables of values. Once that research matures, it will hopefully be possible to augment the language so that we can enforce the missing properties.
246+
We are working on a new class of type system that supports ephemeral capabilities by tracking the free variables of values. Once that research matures, it will hopefully be possible to augment the language so that we can enforce the missing properties.
249247

250248
And it would have many other applications besides: Exceptions are a special case of _algebraic effects_, which has been a very active research area over the last 20 years and is finding its way into programming languages (e.g. Koka, Eff, Multicore OCaml, Unison). In fact, algebraic effects have been characterized as being equivalent to exceptions with an additional _resume_ operation. The techniques developed here for exceptions can probably be generalized to other classes of algebraic effects.
251249

252-
But even without these additional mechanisms, exception checking is already useful as it is. It gives a clear path forward to make code that uses exceptions safer, better documented, and easier to refactor. The only loophole arises for scoped abilities - here we have to verify manually that these abilities do not escape. Specifically, a `try` always has to be placed in the same computation stage as the throws that it enables.
250+
But even without these additional mechanisms, exception checking is already useful as it is. It gives a clear path forward to make code that uses exceptions safer, better documented, and easier to refactor. The only loophole arises for scoped capabilities - here we have to verify manually that these capabilities do not escape. Specifically, a `try` always has to be placed in the same computation stage as the throws that it enables.
253251

254252
Put another way: If the status quo is 0% static checking since 100% is too painful, then an alternative that gives you 95% static checking with great ergonomics looks like a win. And we might still get to 100% in the future.
255253

library/src-bootstrapped/scala/CanThrow.scala

Lines changed: 2 additions & 2 deletions
Original file line numberDiff line numberDiff line change
@@ -2,12 +2,12 @@ package scala
22
import language.experimental.erasedDefinitions
33
import annotation.{implicitNotFound, experimental}
44

5-
/** An ability class that allows to throw exception `E`. When used with the
5+
/** A capability class that allows to throw exception `E`. When used with the
66
* experimental.saferExceptions feature, a `throw Ex()` expression will require
77
* a given of class `CanThrow[Ex]` to be available.
88
*/
99
@experimental
10-
@implicitNotFound("The ability to throw exception ${E} is missing.\nThe ability can be provided by one of the following:\n - A using clause `(using CanThrow[${E}])`\n - A `throws` clause in a result type such as `X throws ${E}`\n - an enclosing `try` that catches ${E}")
10+
@implicitNotFound("The capability to throw exception ${E} is missing.\nThe capability can be provided by one of the following:\n - A using clause `(using CanThrow[${E}])`\n - A `throws` clause in a result type such as `X throws ${E}`\n - an enclosing `try` that catches ${E}")
1111
erased class CanThrow[-E <: Exception]
1212

1313
/** A helper type to allow syntax like

tests/neg/saferExceptions.check

Lines changed: 4 additions & 4 deletions
Original file line numberDiff line numberDiff line change
@@ -1,8 +1,8 @@
11
-- Error: tests/neg/saferExceptions.scala:12:16 ------------------------------------------------------------------------
22
12 | case 4 => throw Exception() // error
33
| ^^^^^^^^^^^^^^^^^
4-
| The ability to throw exception Exception is missing.
5-
| The ability can be provided by one of the following:
4+
| The capability to throw exception Exception is missing.
5+
| The capability can be provided by one of the following:
66
| - A using clause `(using CanThrow[Exception])`
77
| - A `throws` clause in a result type such as `X throws Exception`
88
| - an enclosing `try` that catches Exception
@@ -14,8 +14,8 @@
1414
-- Error: tests/neg/saferExceptions.scala:17:46 ------------------------------------------------------------------------
1515
17 | def baz(x: Int): Int throws Failure = bar(x) // error
1616
| ^
17-
| The ability to throw exception java.io.IOException is missing.
18-
| The ability can be provided by one of the following:
17+
| The capability to throw exception java.io.IOException is missing.
18+
| The capability can be provided by one of the following:
1919
| - A using clause `(using CanThrow[java.io.IOException])`
2020
| - A `throws` clause in a result type such as `X throws java.io.IOException`
2121
| - an enclosing `try` that catches java.io.IOException

0 commit comments

Comments
 (0)