Typed Interaction with Session Types (using Scala and Libretto) by Tomas Mikula

Tomas Mikula demonstrates how to use session types and linearity in Scala with the Libretto library to make illegal states unrepresentable.

"Typed Interaction with Session Types (using Scala and Libretto)" at Functional Scala 2022. As the interaction between two stateful components unfolds, the set of acceptable messages changes at each step. Session types change with the progressing interaction, thus providing type-safety at each step. Conventional approaches to typed interaction fail to keep track of the ever-changing state of types where any message can be received at any stage. That leads to code handling a lot of illegal state, as he will demonstrate with an example. To make the illegal state unrepresentable, Tomas will arrive at an encoding of session types and discover that they require linearity, i.e., the property that each resource is consumed exactly once. However, linearity checking is not widely supported in mainstream programming languages. Finally, Tomas will present Libretto, an experimental Scala library/DSL with an encoding of session types that checks linearity before program execution. Grab Your Early Bird Tickets for the Functional Scala 2023! ➡️ eventbrite.com/e/functional-scala-2023-tickets-481896564597 Contents in the video: 00:58 - First Sketch (Approach I: Naive Objects and Methods, The Interface) 03:45 - Let's take a step up! (Approach II: Linearity by Convention, The Idea) 06:51 - Linearity Helps, Can We Enforce It Before Execution? Meet Libretto! 10:41 - Code Is Cheap. Show Me The Types! Libretto: Types Of Interaction 13:31 - Approach III: Libretto. Canteen: Protocol 19:18 - There's more in Libretto #FunScala2022 #scala #zio #ziverge #functionalprogramming #functionalscala #scalaconference #scaladeveloper