A possible type-based model for scope restrictions on ~Escapable types

Hello, folks.

For the last few months, I've been thinking about where we're going with ~Escapable types and lifetime dependencies. My conclusion is that we need a somewhat radical shift in the basic language model of the feature, away from the system of value dependencies that we currently use towards a world in which scope restrictions are encoded in the types of values.

This is a rather large and complicated question, so I've written it up as a rather long and obscure design document. I'm afraid the document has undergone several incomplete rounds of drafting and redrafting, so it might not hang together as well as I'd like. Still, I hope it'll give people a better understanding of where we stand today and where I think we ought to be going, and I'd love to hear feedback on the ideas in it.

The document uses a somewhat intentionally less-than-great syntax for the type-based restrictions. Nothing about this is set in stone, that most of all, so please don't fret too much about it.

John.

30 Likes

Interesting work!

I've just skimmed through the document and I promise will read it properly later, but it already have a question: are these proposed scopes basically just Rust-style lifetimes, Swift-flavored? Or am I missing something significant?

Just a thought: I remember when I first seen ~Escapable being added to the language, I hoped that It will be able to buy Swift some of the benefits of Rusts's lifetimes without the added complexity. I wonder how and why the language departed from that idea, or was that the idea in the first place.

2 Likes

Rust does use a type-based model for lifetimes. The proposal isn't to blindly copy their language rules, but yes, we would have a lot of similarities that emerge from that.

Ultimately, I don't think the complexity you're concerned about is avoidable if you want to allow things like abstractions over non-escapable values. I also think Swift does need to allow those things in order to let programmers achieve the highest level of performance without sacrificing memory safety. But I also think we can continue to not make programmers think about this stuff unless they specifically want to write that kind of code, whereas I think Rust encourages people to worry about it proactively.

10 Likes

I'm super excited by this direction. Lifetimes in the type system have motivated an incredible type system in Rust, including generic associated types, which I am missing dearly in Swift. I also find this model much easier to reason about than the value-based one, because I can reuse the reasoning about the type system that I have already built up over the years.

I also like scope as a keyword in generic signatures. There is precedent for distinguishing different kinds of generic parameters with keywords like each for parameter packs and let for value generics. And while I can see @scoped working as a spelling for applying a concrete scope restriction, the document is much more tentative about @unscoped, and notes that unbound types really have a whole expected scope signature rather than a boolean property. That made me wonder whether this model would be more naturally expressed by fully embracing existing generic syntax. It would leave the door open to generalizing some of this syntax to regular type parameters in the future, and I have the feeling it would also offer better progressive disclosure than introducing new attributes that nevertheless participate deeply in the type system.

One idea for this would be to introduce a separate implicit generic argument section:

struct Span<Element; scope storage>

It would always come last and be introduced using a semicolon (for example). The key is that this section could be omitted in ordinary source, preserving the existing spelling:

Span<Int>
// understood as:
Span<Int; scope _> // where the scope is inferred

The semicolon is just one possible way to separate the implicit scope section from the type's existing visible generic arguments. I mainly like that it preserves the idea of Span<Element> at the declaration instead of making its scope look like an ordinary generic argument.

This implicit scope section would not exist on every type. It would belong to types that are unconditionally ~Escapable because their values retain some scoped capability, such as Span, Ref, or MutableRef. A generic wrapper that becomes nonescapable only because one of its arguments is nonescapable (like Optional) can propagate the scopes already bound into that argument through ordinary type substitution.

Ordinary escapable types such as Int also have no scope argument of their own. However, every borrow or exclusive access has a scope parameter attached to the ownership convention:

borrowing T
// conceptually:
borrowing<scope _> T

inout T
// conceptually:
inout<scope _> T

And now that Swift has Ref and MutableRef, there's a type level analogy:

borrowing<scope s> T
// conceptually:
Ref<T; scope s>

inout<scope s> T
// conceptually:
MutableRef<T; scope s>

borrowing and inout describe the exclusivity of the access, while the scope parameter describes how long that access remains valid.

More complex examples from the document could then look like this[1]:

struct SMR<T; scope r, s> {
  let ref: MutableRef<Span<T; scope s>; scope r>
}
struct SpanPair<T; scope left, right>: ~Escapable {
  let left: Span<T; scope left>
  let right: Span<T; scope right>
}
func returnEither<scope a, b>(
  spanOne: Span<Int; scope a>,
  spanTwo: Span<Int; scope b>
) -> Span<Int; scope a & b>

Scopes do not necessarily need to be projected back out of values. As with ordinary generic arguments, a function that needs to express a relationship between scopes can introduce names for them in its generic signature:

func returnFirst<scope first>(
  spanOne: Span<Int; scope first>,
  spanTwo: Span<Int>
) -> Span<Int; scope first>

The explicit scope parameters are only needed when inference is insufficient or the programmer wants to document a particular relationship. This is one more way in which this syntax sticks to patterns familiar to existing Swift users (versus the decltype-like syntax @scoped(spanOne) from the document).

Borrowing and inout accesses also introduce scopes, but these scopes do not come from generic arguments in the parameter's nominal type. They come from the ownership convention itself. I see two ways of spelling this, I'm not entirely sure which one is better long term.

Because Swift's self parameter is implicit and its ownership convention is written before the declaration keyword, one option would be to let that convention introduce a name for its access scope:

borrowing<scope access> func visit(
  visitor: (borrowing<scope access> Element) -> Void
)

Here access names the borrow of self performed for the call, and the annotation on Element says that its borrow remains valid for the same scope.

This syntax is somewhat special because borrowing<scope access> both introduces the scope parameter and binds it to the implicit self access. Another option would be to make the implicit parameter explicit:

func visit<scope access>(
  self: borrowing<scope access> Self,
  visitor: (borrowing<scope access> Element) -> Void
)

In this form, access is introduced in the ordinary generic signature and then applied to the ownership convention of self, just like any other generic argument.

The first spelling is probably more swifty today. But the explicit form may ultimately be more principled as ownership, isolation, and lifetime properties of the hidden self parameter become increasingly important (and complex).

Also: if Self is itself nonescapable, its concrete scope arguments remain part of the Self type and are separate from access, which names this particular call's temporary borrow.

Generic associated types

The document introduces the distinction between bound and unbound types. This seems like the strongest motivation for using generic syntax. Consider:

typealias ISpan = Span<UInt32>

This could be explained as implicitly abstracting over the omitted scope:

typealias ISpan<scope s> = Span<UInt32; scope s>

When ISpan is used as the type of a value, the scope argument is inferred and bound at that use.

The same reasoning applies to an unbound associated type. An attribute such as:

@unscoped associatedtype BorrowingIterator

looks like it switches on one special property. But as the document points out, an unbound type actually has an expected scope signature.

Embracing GATs, an adaptation of Iterable could look something like this:

protocol Iterable: ~Copyable, ~Escapable {
  associatedtype Element: ~Copyable
  associatedtype Failure: Error = Never

  associatedtype BorrowingIterator<scope access>:
    BorrowingIteratorProtocol<Element, Failure>
      & ~Copyable
      & ~Escapable
    where Self: access

  borrowing<scope access> func makeBorrowingIterator()
    -> BorrowingIterator<scope access>
}

(The exact syntax of where Self: access is again illustrative.)

The associated type declaration says that BorrowingIterator is a family of types indexed by an access scope. The where clause says that the family only needs to be defined for access scopes contained within the scope in which Self is valid.

I think this is pleasantly intuitive if you already understand generic syntax. Instead of one associated type, the conformance provides a family of associated types indexed by a scope parameter.

More importantly, it gives us ordinary generic operations for composing these families. An implementation could write:

typealias BorrowingIterator<scope access> =
  PrefixIterator<Base.BorrowingIterator<scope access>>

The scope-indexed associated type is explicitly instantiated before being composed in an ordinary generic wrapper. With only a @unscoped attribute, the language would still eventually need some way to instantiate/project/equate/compose such unbound associated types. At that point it seems like we would be reconstructing a parallel GAT system with special purpose rules.

To be clear, I do not want to predicate lifetime features on the existence of fully fledged GATs or other type system features. We could start with a very limited form that permits only a single scope parameter on an otherwise non generic associated type.

I also don't want to seriously suggest any particular concrete syntax here. My argument is more about the direction:

  • By basing scope abstraction on existing generic syntax we can reuse a mental model Swift programmers already have and offer better progressive disclosure than either @scoped or the current @lifetime.
  • Treating "unbound" as an implicit generic signature leaves the door open to more powerful scope abstractions and potentially broader improvements to Swift's generics system in the future.

Even if none of that broader generalization happens in the short term, I think it would be valuable for the lifetime model to be built on concepts that can naturally grow in that direction. That could also help justify the scale of this refactor, as the machinery would not only improve Swift's ability to abstract over scopes, but could eventually provide the foundation for stronger abstraction capabilities over ordinary types as well.


  1. In the case of SMR, I think the type is only valid when s contains r because the stored span must remain valid whenever the mutable reference can be used. Rust can infer this, so I expect Swift would too, but an explicit syntax is always possible. ↩︎

7 Likes

Thanks for writing this up. I have worked with a lot of ~Escapable types over the past year as part of the new prototype HTTP APIs and Async Streaming APIs. While the value based model worked for most of the APIs so far there were a few things we weren't able to do yet that you covered in the document. In particular, I wanted to express a "span of spans" to model vector reads and writes, and transformation methods such as map/filter/first on the reader and writers. I really like the type-based model outlined in the document. In my opinion, It makes it both more powerful and understandable at the same time.

In the beginning of the document, it is mentioned that this is applicable for both low-level and high-level resources. However, the rest of the document is then only showing examples of low-level resources (mostly memory in the form of buffers and spans). I think high-level resources are very different from low-level resources. In particular, they often have different clean-up patterns such as throwing and asynchronous clean-ups which require with-style closure approaches to correctly model. I'm curious to see how the type-level based approach would translate to something like a File or HTTPClient example:

struct File: ~Copyable, ~Escapable {
    static func openAt(
        path: FilePath,
        options: OpenOptions,
        body: (@scoped(?) inout File) async throws -> Void 
    ) {
      ...
    }
}

What would be the scope of File here? It is not tied to any parameter but it is also not immortal.

While this is somewhat orthogonal to document and I don't want to derail this thread but I was wondering how this relates to ownership. The document outlines making lifetimes/scope part of a type which enables lifetime effect polymorphism for types and closures. Assuming we go this route we will still have a similar problem when it comes to polymorphism over the ownership as we can see with Span/MutableSpan and Ref/MutableRef. While for concrete types that's less of a problem I have faced a lot of problems when it comes to generic algorithms and protocols where they often want to be generic over the ownership of parameters or return values. Similarly, this applies to sendable effects such as @Sendable or sending. I'm curious to understand your thinking here.

3 Likes
Slight aside re: File API

Why would you want to define a File type like that instead of letting it be used like a normal variable? My understanding was that one of the main goals of ~Escapable was to replace closure scopes like withUnsafePointer with normal function calls that just return a lifetime-scoped value. A non-copyable struct can already perform cleanup, and a need for async cleanup feels like an unrelated language feature and not really something that should be bolted on to ~Escapable.

struct File: ~Copyable[, ~Escapable] {
    init(
        opening path: FilePath,
        options: OpenOptions,
    )
}
3 Likes

This is a great question. Putting aside whether File should really be a non-escapable type, a with-function callback that receives a temporary value as a parameter is obviously a key use case to support. The way you should think about this in the type-based world is that the callback must be prepared to accept a span of any scope, which is to say, it must be polymorphic over the scope of the span.

This example makes a strong case that first-class scope polymorphism is a necessary part of this feature and cannot be deferred for long. I'll update the document.

6 Likes

I’m curious about the relationship between flow-sensitive refinement and handling Optional and Result. According to SE-0465, Optional.init(_: T) and Optional.take() are defined as follows for non-escapable Wrapped types:

extension Optional: ExpressibleByNilLiteral
where Wrapped: ~Copyable & ~Escapable {
  @_lifetime(immortal) // Illustrative syntax
  init(nilLiteral: ())
}

extension Optional where Wrapped: ~Copyable & ~Escapable {
  @_lifetime(copying some) // Illustrative syntax
  init(_ some: consuming Wrapped)
}

extension Optional where Wrapped: ~Copyable & ~Escapable {
  @_lifetime(copying self) // Illustrative syntax
  mutating func take() -> Self
}

Since take() only states a lifetime dependency on self, does this mean that an Optional’s scope is currently defined at initialization and never changes, even after being reassigned? Does that imply an Optional initialized with nil could effectively “launder” scopes through the immortal scope.

That seems at odds with the section on flow-sensitive refinement, which describes a local Array variable’s scope tracking the union of its values’ lifetimes at various points throughout the abstract execution of the function in which it is declared. The section strongly suggests that this is the behavior in shipping Swift, so I must be misinterpreting the design of Optional, yes?

I agree that first-class scope polymorphism is necessary. Thinking about this more I like what @Val outlined with making scopes part of the generic signature since it allows types with stored closures to become generic over the scope of the stored closure e.g.:

struct Holder<A, scope S> {
  var closure: @scope(S) () -> A
}
4 Likes

Would it be possible to include a comparison to Rust's current model? I personally would find that helpful in understanding the expressivity differences.

1 Like

There's no laundering problem here in any of the models. Consider code like this, where NE is a non-escapable type:

var x: [NE]? = nil
x = []
x!.append(elt)
let y = x.take()

x has different abstract values at different points in its lifetime; let's make those explicit:

var x: [NE]? = nil
// x here is %x0 = .none
x = []
// x here is %x1 = .some([])
x!.append(elt)
// x here is %x2, the post-value of self for the call to append
let y = x.take()
// x here is %x3, the post-value of self for the call to take
// y here is %y1, the return value of the call to take

In the value-dependency model, %x0 is produced by constructing a fresh Optional.none value from nothing, so it has no dependencies.
%x1 is produced by constructing a fresh Optional.some value from an array value, so it has the dependencies of that array value, which is constructed by calling an initializer with no arguments, so it also has no dependencies.
%x2 is the post-value of self for append. If Array supported non-escapable elements, append would say that the post-value of self has the dependencies of both the pre-value of self (%x1) and the appended argument (elt). Since the dependencies of %x1 are empty, x2's dependencies are therefore just those of elt.
%y1 is the return value of take. The signature of take above says that the return value has the dependencies of the pre-value of self, which is %x2. %y1's dependencies are therefore those of elt.
%x3 is the post-value of self for take. The signature of take above says that the post-value just has the dependencies of the pre-value, so %x3's dependencies are those of %x2, which is to say, those of elt. This is sub-optimal: since take actually leaves the optional empty, a more precise signature would reset the dependencies on the post-value.

The simple type-based model does not consider abstract values. Instead, we see that the type of x is [NE]?, and we begin by filling in the missing scope specifiers to make it a properly bound type. Assume that NE is a type like Span with a single scope parameter, so the type of x is now:

_x := [@scoped(_4) NE]?

Phase 1 checking then proceeds as follows:

  • nil has type _nil := [@scoped(_5) NE]?. Because of the initialization, this must be a subtype of _x. Recursively decomposing using the variance rules, _1 must a subscope of _5.
  • Optional.some([]) has type _lit := [@scoped(_5) NE]?. Because of the assignment, _lit must be a subtype of _x. Recursively decomposing using the variance rules, _4 must a subscope of _5.
  • elt has type _elt := @scoped(_6) NE.
  • x! has type [@scoped(_4) NE].
  • Array.append has type <Element> (inout [Element]) -> (Element) -> Void. Applying this to x!, Element must be @scoped(_4) NE, so _elt must be a subtype of that. Recursively decomposing using the variance rules, _4 must a subscope of _6.
  • Optional.take has type <Wrapped> (inout Wrapped?) -> () -> Wrapped. Applying this to x, Wrapped must be [@scoped(_4) NE], and this is the return type of the call.
  • y has type _y := [@scoped(_7) NE]. Because of the initialization, the return type of the call to take, [@scoped(_4) NE], must be a subtype of this.

Phase 2 checking would then find a valid solution to these constraints, most likely that _4 = _5 = _6 = _7. That is to say, the scope restriction of the element type of the array stored in x is inferred from the type of elt.

Flow-sensitive refinement would allow different abstract values of x to have different scope restrictions, so instead of having a global _x that's bound to [@scoped(_4) NE]?, %x1 would have type [@scoped(_1) NE]?, %x2 would have type [@scoped(_2) NE]?, and so on. The data flow rules for inout arguments would then require the type of %x3 to be a subtype of the type of %x2, which in turn would have to be a subtype of %x1.

In both type-based models, the type of x is derived from its use pattern. In the non-flow-sensitive model, it's the entire use pattern; in the flow-sensitive model, it's just the use pattern that might have happened prior to this point. This function doesn't require flow-sensitive refinement to pass checking, so both models accept it.

But even if x's type was naively derived from the type of its initializer, that wouldn't be a soundness hole in the checking, it would just be an overly-conservative rule. We would decide that x had type [@scoped(immortal) NE]?, and then we would see the call to append and presumably reject it because there is no subscope relationship between _6 (the scope restriction of elt) and immortal.

6 Likes

I've updated the document to address Franz's point about first-class scope polymorphism and to correct a few misunderstandings, most importantly my own misunderstanding of a request from the SIL optimizer team.

I still owe Val a reply to their message, which is long enough that I need to break it down a bit.

4 Likes