Skip to main content

Session Types with Linearity in Haskell

Orchard, Dominic A. and Yoshida, Nobuko (2017) Session Types with Linearity in Haskell. In: Gay, S. and Ravara, A., eds. Behavioural Types: from Theory to Tools. River Publishers Series in Automation, Control and Robotics . River Publishers, pp. 219-241. ISBN 978-87-93519-82-4. E-ISBN 978-87-93519-81-7. (doi:10.13052/rp-9788793519817)

Abstract

Type systems with parametric polymorphism can encode a significant pro- portion of the information contained in session types. This allows concurrent programming with session-type-like guarantees in languages like ML and Java. However, statically enforcing the linearity properties of session types, in a way that is also natural to program with, is more challenging. Haskell provides various language features that can capture concurrent programming with session types, with full linearity invariants and in a mostly idiomatic style. This chapter overviews various approaches in the literature for session typed programming in Haskell. As a starting point, we use polymorphic types and simple type-level functions to provide session-typed communication in Haskell without linearity. We then overview and compare the varying approaches to implementing session types with static linearity checks. We conclude with a discussion of the remaining open problems. The code associated with this chapter can be found at http://github. com/dorchard/betty-book-haskell-sessions.

Item Type: Book section
DOI/Identification number: 10.13052/rp-9788793519817
Projects: Projects 0 not found.
Uncontrolled keywords: behavioural types, linearity, Haskell, verification
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Faculties > Sciences > School of Computing
Depositing User: Dominic Orchard
Date Deposited: 05 Apr 2018 15:43 UTC
Last Modified: 29 May 2019 20:26 UTC
Resource URI: https://kar.kent.ac.uk/id/eprint/66632 (The current URI for this page, for reference purposes)
Orchard, Dominic A.: https://orcid.org/0000-0002-7058-7842
  • Depositors only (login required):

Downloads

Downloads per month over past year