MobilityReadingGroup

Session Types with Linearity in Haskell

Dominic ORCHARD, Nobuko YOSHIDA

Type systems with parametric polymorphism can encode a significant proportion 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.

@article{OY2017,
  author = {Dominic Orchard and Nobuko Yoshida},
  title = {{Session Types with Linearity in Haskell}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {219--242},
  publisher = {River Publishers},
  year = 2017
}

@article{OY2017,
  author = {Dominic Orchard and Nobuko Yoshida},
  title = {{Session Types with Linearity in Haskell}},
  journal = {Behavioural Types: from Theory to Tools},
  pages = {219--242},
  publisher = {River Publishers},
  doi = "10.13052/rp-9788793519817",
  year = 2017
}