Dominic Orchard - Imperial College London

Artifact for Effects as sessions, sessions as effects (preprint PDF), POPL 2016

Dominic Orchard, Nobuko Yoshida (Imperial College London)

Effect and session type systems are two expressive behavioural type systems. The former is usually developed in the context of the lambda-calculus and its variants, the latter for the pi-calculus. In our paper we explored their relative expressive power. Firstly, we gave an embedding from PCF, augmented with a parameterised effect system, into a session-typed pi-calculus (session calculus), showing that session types are powerful enough to express effects. Secondly, we gave a reverse embedding, from the session calculus back into PCF, by instantiating PCF with concurrency primitives and its effect system with a session-like effect algebra (Section 6). The embedding of session types into an effect system is leveraged to give an implementation of session types in Haskell, via an effect system encoding (Section 7). This is the artifact of this paper, provided as the effect-sessions library.

Section 6 and 7 are the relevant parts of the paper for the artifact. As explained in Section 7, the implementation is not explicitly designed to be a user-friendly interface for programming with sessions. Instead, it is a fairly direct rendering in Haskell of the encoding of Section 6. Its aim is to give credance to embedding of Section 6 and to provide a new basis for working with session types in Haskell-- but is not a full "end product" in terms of user programming.

Limitations. There are a number of limitations in the implementation due to the limits of Haskell compared with the variant of PCF in Section 6. Mainly, Haskell has no subtyping or equirecursive types. The former is solved via explicit subtyping combinators in Haskell. The latter (equirecursive types) is solved via restricted forms of recursion, with fixed-points computed at the type-level only for affine effect equations. In practice, this covers a multitude of examples.




If experiencing problems running the examples.lhs, try running cabal configure in the top-level directory which should explain more clearly any missing dependencies in your Haskell setup.

Whilst experimenting the library, the programmer may encounter some harder to read errors. This is a shortcoming of GHC type-level programming: it is hard to get good domain-specific errors. The following provides some hints.



Thanks to Julien Lange and Bernardo Toninho for their comments and testing. Any remaining issues are my own.
Last modified: Tue Oct 13 12:28:40 BST 2015