Singly typed actors in Agda - An approach to distributed programming with dependent types
Ladda ner
Typ
Examensarbete för masterexamen
Master Thesis
Master Thesis
Program
Computer science – algorithms, languages and logic (MPALG), MSc
Publicerad
2018
Författare
Kraft, Pierre
Modellbyggare
Tidskriftstitel
ISSN
Volymtitel
Utgivare
Sammanfattning
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.
Beskrivning
Ämne/nyckelord
Data- och informationsvetenskap , Computer and Information Science