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
This work is licensed under a Creative Commons Attribution-NonCommercial 4.0 International License.
|
|
Download this file (PDF/162kB) |
|
Request a format suitable for use with assistive technology e.g. a screenreader | |
PDF
Language: English |
|
Download this file (PDF/162kB) |
Preview |
Request a format suitable for use with assistive technology e.g. a screenreader | |
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: | 05 Nov 2024 11:05 UTC |
Resource URI: | https://kar.kent.ac.uk/id/eprint/66632 (The current URI for this page, for reference purposes) |
- Link to SensusAccess
- Export to:
- RefWorks
- EPrints3 XML
- BibTeX
- CSV
- Depositors only (login required):