Skip to content
Open
Changes from all commits
Commits
File filter

Filter by extension

Filter by extension

Conversations
Failed to load comments.
Loading
Jump to
Jump to file
Failed to load files.
Loading
Diff view
Diff view
10 changes: 8 additions & 2 deletions examples/tour/captures.effekt.md
Original file line number Diff line number Diff line change
Expand Up @@ -5,8 +5,10 @@ permalink: tour/captures

# Captures

Functions are second-class in Effekt, but for a good reason. Functions closing over capabilities must not be returned, otherwise it can not be guaranteed that these capabilities are still in scope.
Thus, we have to keep track of these captures and ensure they are in scope upon invoking.
[Computations](/tour/computation), such as functions and objects, are second-class _by default_ in Effekt, but for a good reason.
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Does the "but for a good reason" add anything? 🤔

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it is fine, since it leads over to the next sentence.

Since computations can capture capabilities, they can only be used where those capabilities remain in scope.
For statically preventing capabilities from escaping their valid scope, Effekt tracks captured capabilities on the type level and verifies they're still in scope upon usage.
We call this mechanism _boxing_ and will discuss in greater details in the next [section](/tour/captures#boxing).
Copy link
Collaborator

@b-studios b-studios Nov 30, 2025

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a bit misleading IMO. I would rather say something like

Suggested change
We call this mechanism _boxing_ and will discuss in greater details in the next [section](/tour/captures#boxing).
Functions and capabilities can still be treated as first-class values by means of _boxing_, which we discuss in greater details in the next [section](/tour/captures#boxing).


Consider the following example where `divide` is being passed an explicit capability:

Expand All @@ -19,7 +21,9 @@ def divide(n: Int, m: Int) {exc: Exception}: Int =
if (m == 0) { exc.throw("uhoh") }
else { n / m }
```

Handlers (implicitly or explicitly) introduce capabilities that are then passed to the position where an effect is used.

```effekt:repl
try {
val res = divide(10, 0) {exc} // here we pass it explicitly
Expand All @@ -28,11 +32,13 @@ try {
def throw(msg) = println("ERROR: " ++ show(msg))
}
```

What happens if we try to return the capability?

```effekt:repl
try { exc } with exc: Exception { def throw(msg) = panic(msg) }
```

By directly returning `exc` from the `try` expression, we break the lexical effect handling reasoning since `exc` is only defined within the `try` body.
For the same reason, we must not return a function that closes over such a capability.

Expand Down
Loading