Exploring Algebraic Placement in Multiparty Languages
summary
Claims that placement systems mirror type-system structure and that a type-checker can be repurposed into a placement checker, demonstrated by a Scala prototype that encodes polymorphic peer modules (mix-in composition and macros hooked into the compiler), implements placed union types for dynamic placement and intersection placements for replication, and derives an explicit placement algebra (union/intersection distributive laws). The prototype compiles realistic examples, requires nontrivial Scala encoding and compiler hooks, and suggests algebraic optimizations though some runtime checks remain.
AI-written summary · about
chapters (12)
- 0:00Algebraic placement intro
- 1:47Choreography vs multitier
- 4:55Static placement in Scala Loci
- 6:39Polymorphism for multitier modules
- 8:44Distributed algorithm with modules
- 10:09Dynamic placement limitations
- 10:52First-class placed union types
- 12:18Products as sharing
- 13:00Placement type laws
- 14:47Future work and compiler optimizations
- 15:09Conclusion and open questions
- 15:34Q&A
related talks
16mType-Safe Dynamic Placement with First-Class Placed Values
32mMulticompatibility for Multiparty-Session Composition
23mA Synthetic Reconstruction of Multiparty Session Types
35mEvent-Driven Multiparty Session Actors
18mHybrid Multiparty Session Types: Compositionality for Protocol Specification th...
41mTowards language support for distributed systems
15mStatically Verified Refinements for Multiparty Protocols
22mCompositional Programming and Testing of Dynamic Distributed Systems