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

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.