Haskell Session Types with (Almost) No Class

Riccardo Pucella and Jesse A. Tov

In Proc. ACM SIGPLAN 2008 Haskell Symposium (Haskell’08), September 2008.

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.

Available:

• US Letter PDF (237 KiB)
• Slides from talk (688 KiB)
• Library page (on Hackage)
• Preprocessor for ixdo notation (on Hackage)
• See Keigo IMAI’s full-session package for a library that updates and extends our work

• Prototypes in other languages:

  cs/SessionTypes.cs

  Requires C# 3.0 for lambda; known to work with VS2008 and known to crash Mono gmcs 1.2.2.1’s type checker

  java/SessionTypes.java

  Requires Java >=1.5 for generics; known to work with Sun JDK 1.5.0_13

  ocaml/session.mli and ocaml/session.ml

  Known to work with OCaml 3.10.1, but should work with older versions

  scala/SessionTypes.scala

  Known to work with Scala 2.7.0-final

  sml/session.sml

  Some portions use SML/NJ-specific feature, indicated with a comment; the rest should be SML’97; known to work with SML/NJ v110.67 and Moscow ML 2.00.

“Haskell Session Types with (Almost) No Class” paper © 2008 ACM. This is the author's version of the work. It is posted here by permission of ACM for your personal use. Not for redistribution. The definitive version was published in Proc. ACM SIGPLAN 2008 Haskell Symposium, 13:25-36, 2008. http://doi.acm.org/10.1145/1411286.1411290

---

Publications list | Home