Channel- and actor-based programming languages are both used inpractice, but the two are often confused. Languages such as Goprovide 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 abouttranslations that exist in the folklore. We define a calculuslambda-ch for typed asynchronous channels, and a calculus lambda-act fortyped actors. We define translations from lambda-act into lambda-ch andlambda-ch into lambda-act and prove that both are type- andsemantics-preserving.We show that our approach accounts for synchronisation and selectivereceive in actor systems and discuss future extensions to support guardedchoice and behavioural types.
展开▼
