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

Examensarbete för masterexamen

Please use this identifier to cite or link to this item:
Download file(s):
File Description SizeFormat 
256251.pdfFulltext701.06 kBAdobe PDFView/Open
Type: Examensarbete för masterexamen
Master Thesis
Title: Singly typed actors in Agda - An approach to distributed programming with dependent types
Authors: Kraft, Pierre
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.
Keywords: Data- och informationsvetenskap;Computer and Information Science
Issue Date: 2018
Publisher: Chalmers tekniska högskola / Institutionen för data- och informationsteknik (Chalmers)
Chalmers University of Technology / Department of Computer Science and Engineering (Chalmers)
Collection:Examensarbeten för masterexamen // Master Theses

Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.