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) (KAR id:66632)

PDF Publisher pdf
Language: English


Download (162kB)
[thumbnail of RP_9788793519817C10.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
PDF
Language: English
Download (162kB) Preview
[thumbnail of RP_9788793519817C10.pdf]
Preview
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:
http://dx.doi.org/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: CamFort
Uncontrolled keywords: behavioural types, linearity, Haskell, verification
Subjects: Q Science > QA Mathematics (inc Computing science) > QA 76 Software, computer programming,
Divisions: Divisions > Division of Computing, Engineering and Mathematical Sciences > School of Computing
Funders: Organisations -1 not found.
Depositing User: Dominic Orchard
Date Deposited: 05 Apr 2018 15:43 UTC
Last Modified: 08 Dec 2022 22:19 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