This talk provides an overview of our ongoing research on the relationship between type systems and placement systems in programming languages for distributed systems. While the different approaches for programming multiparty systems share the common objective of static reasoning across distributed parties, integrating such reasoning techniques into general-purpose programming languages remains challenging.

Traditionally, placement features, such as polymorphic and dynamic placements, are retrofitted onto existing type systems. Yet this integration lacks a principled approach that is independent of type systems. In this talk, we argue that static semantics of the language is orthogonal to the idea of placements by demonstrating how a placement system (for checking placements) can be separated completely from a type system (for conventional type-checking) and how both can be composed and reasoned about modularly.

Our key insight is that the structure of a placement system is identical to the structure of a type system, enabling ideas from one to be applied to the other. Practically, this correspondence allows us to repurpose Haskell’s type checker to become a placement checker. Theoretically, we use this correspondence to build a placement algebra on places akin to algebraic data types in conventional type systems.