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 caps in method and function parameters and results. For example, take this method:

  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:

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:

makeLogger: ∀cap₁.(fs: FileSystem^{cap₁}): ∃cap₂. Logger^{cap₂}

There's a connection with capture polymorphism here. caps 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

  (x: T) -> U^

is interpreted as having an existentially bound cap in the result, like this

  (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

  (x: A) -> B -> C^

is interpreted as

  (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]