Haskell session types with (almost) no class

Riccardo Pucella*, Jesse A. Tov

*Corresponding author for this work

Research output: Chapter in Book/Report/Conference proceedingConference contribution

60 Scopus citations


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)
Title of host publicationHaskell'08 - Proceedings of the ACM SIGPLAN 2008 Haskell Symposium
Number of pages12
StatePublished - 2008
Event1st ACM SIGPLAN Haskell Symposium, Haskell'08 - Victoria, BC, Canada
Duration: Sep 25 2008Sep 25 2008

Publication series

NameHaskell'08 - Proceedings of the ACM SIGPLAN 2008 Haskell Symposium


Other1st ACM SIGPLAN Haskell Symposium, Haskell'08
CityVictoria, BC


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

ASJC Scopus subject areas

  • Computer Science Applications
  • Software
  • Electrical and Electronic Engineering


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

Cite this