Haskell session types with (almost) no class

Riccardo Pucella*, Jesse A. Tov

*Corresponding author for this work

Research output: Contribution to journalArticlepeer-review

3 Scopus citations

Abstract

We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types are available. Our embedding takes advantage of Haskell where appropriate, but we rely on no exotic features. Thus our approach translates with minimal modification to other polymorphic, typed languages such as ML and Java. Our implementation works with existing Haskell concurrency mechanisms, handles multiple communication channels and recursive session types, and infers protocols automatically. While our implementation uses unsafe operations in Haskell, it does not violate Haskell's safety guarantees. We formalize this claim in a concurrent calculus with unsafe communication primitives over which we layer our implementation of session types, and we prove that the session types layer is safe. In particular, it enforces that channel-based communication follows consistent protocols.

Original languageEnglish (US)
Pages (from-to)25-36
Number of pages12
JournalACM SIGPLAN Notices
Volume44
Issue number2
StatePublished - Feb 1 2009

Keywords

  • Concurrency
  • Embedded type systems
  • Functional programming
  • Haskell
  • Phantom types
  • Session types
  • Type classes

ASJC Scopus subject areas

  • Computer Science(all)

Fingerprint Dive into the research topics of 'Haskell session types with (almost) no class'. Together they form a unique fingerprint.

Cite this