Swift Sessions: a binary sessions library for Swift

Hello, everyone!

I recently wrote my bachelor degree thesis about designing and implementing a binary sessions library for Swift. The final outcome is Swift Sessions, a Swift package that developers can use to make concurrent processes communicate safely with compile-time correctness check.

The library is based on the session types formalism, and currently supports the following features:

  • session type inference (only with closures)
  • session types with binary branches
  • dynamic linearity checking
  • duality constraints on session types
  • session initialization with client/server architecture

Programming Styles

The library offers two distinct styles.

Continuation with Closures

Protocol continuations are passed as closures. This approach makes the flow of logic explicit and easy to follow within the closure context. It's particularly useful for straightforward communication sequences.

await Session.create { e in
    // One side of the communication channel
    await Session.recv(from: e) { num, e in
        await Session.send(num % 2 == 0, on: e) { e in
            Session.close(e)
        }
    }
} _: { c in
    // Another side of the communication channel
    await Session.send(42, on: e) { e in
        await Session.recv(from: e) { isEven, e in
            Session.close(e)
        }
    }   
}
  • Pros: Complete type inference of the communication protocol.
  • Cons: Nested code structure.

Continuations with endpoint passing

This style involves returning continuation endpoints from communication primitives. It offers greater flexibility, enabling more modular and reusable code, particularly for complex communication sequences.

typealias Protocol = Endpoint<Empty, (Int, Endpoint<(Bool, Endpoint<Empty, Empty>), Empty>)>

// One side of the communication channel
let e = await Session.create { (e: Protocol) in
    let (num, e1) = await Session.recv(from: e)
    let e2 = await Session.send(num % 2 == 0, on: e1)
    Session.close(e2)
}
    
// Another side of the communication channel
let e1 = await Session.send(42, on: e)
let (isEven, e2) = await Session.recv(from: e1)
Session.close(e2)
  • Pros: Simplicity, particularly for avoiding deep indentation.
  • Cons: Incomplete type inference support.

Client/Server architecture

Instead of creating disposable sessions as seen in the previous examples, you can also initialize sessions using a client/server architectural style.

A server is responsible for creating and managing multiple sessions that can handle a specific protocol. Many clients can be spawned and used with the same server to interact dually according to that defined protocol. This allows to define a protocol's side only once, and use it as many times as we want.

// Server side
let server = await Server { e in
    await Session.recv(from: e) { num, e in
        await Session.send(num % 2 == 0, on: e) { e in
            Session.close(e)
        }
    }
}

// Client side
let c1 = await Client(for: server) { e in
    await Session.send(42, on: e) { e in
        await Session.recv(from: e) { isEven, e in
            Session.close(e)
        }
    }
}

// You can spawn more clients here...

This architecture is useful for scenarios where multiple clients need to interact with a single server. It's also useful to implement complex protocols that involve loops and recursion.

Future directions

Swift 6.0 will introduce new features such as non-copyable generics, which will significantly enhance the capabilities of this library allowing static linearity checking.

I couldn't wait to share this little contribution of mine with the Swift community. You can find more details about this project inside this Medium article I wrote. Any contributions and comments are welcome!

7 Likes

This is awesome thx for sharing!

1 Like