Singly typed actors in Agda - An approach to distributed programming with dependent types

Abstract

By requiring communication to take place using explicit message passing, the actor model has been shown to be an effective tool for building distributed systems. However, communication in the actor model has traditionally been untyped, i. e. any message can be sent to an actor, even though it most probably only handles specific ones. Singly typed actors have a single static type assigned to each actor, limiting messages to those that can be handled by the actor. We present Mact, a formal model of singly typed actors, implemented as a shallow embedding in Agda. The shallow embedding allows for a minimal calculus that does not sacrifice usability, since programs are expressed using the full power of Agda— a deep embedding would not have allowed for the same experimental investigation without significantly more effort. We use this advantage to demonstrate how several common communication patterns can be expressed as abstractions inside the model. We implement and compare implementation strategies for out of order communication—the foundation of the abstractions we build. With out of order communication we are able to emulate local channels, which we use to implement synchronous calls and active objects. Like He (2014), we find that subtyping solves the problem of wide actor types when sending messages. However, the use of a single inbox per actor remains problematic when receiving messages, especially in the context of call-response patterns. Our emulation of local channels alleviates the problem of wide actor types, but we still propose extending the model with native support for multiple inboxes per actor as a better solution.