This demonstrates that capability-based effect systems with capture checking are naturally effect polymorphic. Likewise, if the lazy list xs was pure, it would not show up in any of the method results. The actual function argument does not show up since it is pure. The type of the mapped list ys has only xs in its capture set. We can now reconstruct how this principle produced the error in the introductory example, where usingLogFile was declared like this: But * is not itself available as a global entity in the environment. The capture set of a type has to be present in the environment when a type is instantiated from a type variable. Capabilities and Capturing TypesĬapture checking is done in terms of capturing types of the form. The capture checker extension introduces a new kind of types and it enforces some rules for working with these types.

The following sections explain in detail how capture checking works in Scala 3. How to reason about capabilities associated with memory locations.How to do region-based allocation, safely,.How to solve the 'what color is your function?' problem of mixing synchronous and asynchronous computations.How to address the problem of effect polymorphism in general.We show later how capture checking enables a clean and fully safe system for checked exceptions in Scala. How to have a simple and flexible system for checked exceptions.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. It turns out that capture checking has very broad applications. An error would be issued in the second case, but not the first one (this assumes a capture-aware formulation of LazyList which we will present later in this page).

Fs capture