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

Click to download this file (162kB)
[thumbnail of RP_9788793519817C10.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Language: English
Click to download this file (162kB) Preview
[thumbnail of RP_9788793519817C10.pdf]
This file may not be suitable for users of assistive technology.
Request an accessible format
Official URL:


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: (The current URI for this page, for reference purposes)
Orchard, Dominic A.:
  • Depositors only (login required):

Total unique views for this document in KAR since July 2020. For more details click on the image.