Polymorphic Typestate for Session Types
summary
Claims that a typestate-based model, using PolyVGR with higher-order polymorphism and existential types, matches the expressivity of functional and linear session-type approaches. Defines shapes/domains to quantify over fragments of the typestate so sent values carry an existential package describing their channel resources, unifying data/channel send/receive rules. Proves type preservation and progress and ships a prototype type checker that handles the complex polymorphic signatures and large types.
AI-written summary · about
chapters (11)
- 0:00Introduction
- 2:50Functional vs imperative styles
- 5:38Early system limitations
- 8:06Polymorphic typestate intro
- 11:13Unifying send/receive rules
- 13:00Sending with channel refs
- 15:14Example: multi-channel send
- 16:38Channel creation
- 17:43Advantages over prior calculi
- 18:26Future work
- 19:32Questions and discussion
related talks
31mSo what's the difference between a session type and an ordinary type anyway?
21mPolymorphic Type Inference for Dynamic Languages
22mProbabilistic Refinement Session Types
14mThe Simple Essence of Monomorphization
21mSeamless Scope-Safe Metaprogramming Through Polymorphic Subtype Inference (Short Paper)
32mIntrinsically Typed Sessions with Callbacks
20mMessage-Observing Sessions
42mPolymorphic Function Types in Scala 3