Mixing Metaphors: Actors as Channels and Channels as Actors (Extended Version)

TL;DR

This paper introduces formal calculi for typed channels and actors, providing translations between them that preserve type and semantics, clarifying their relationship and enabling better reasoning about concurrent programming models.

Contribution

It defines typed calculi for channels and actors, and proves type- and semantics-preserving translations between them, unifying their conceptual understanding.

Findings

Translations preserve types and semantics

Accounts for synchronization and selective receive

Framework supports future extensions like guarded choice

Abstract

Channel- and actor-based programming languages are both used in practice, but the two are often confused. Languages such as Go provide anonymous processes which communicate using buffers or rendezvous points---known as channels---while languages such as Erlang provide addressable processes---known as actors---each with a single incoming message queue. The lack of a common representation makes it difficult to reason about translations that exist in the folklore. We define a calculus $\lambda_{\textrm{ch}}$ for typed asynchronous channels, and a calculus $\lambda_{\textrm{act}}$ for typed actors. We define translations from $\lambda_{\textrm{act}}$ into $\lambda_{\textrm{ch}}$ and $\lambda_{\textrm{ch}}$ into $\lambda_{\textrm{act}}$ and prove that both are type- and semantics-preserving. We show that our approach accounts for synchronisation and selective receive in actor systems and discuss future extensions to support guarded choice and behavioural types.