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.
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.
- Ensure you have GHC (Glasgow Haskell Compiler) of at least version 7.8.1.
The latest version of GHC (7.10.2) can be downloaded as part of the Haskell Platform for Windows, Linux, or Mac OS X.
To upgrade an existing Haskell Platform for Linux, there are good instructions here (tested for Ubuntu).
- Install the stm package:
cabal install stm
- Download and unzip the library sources
The library also relies on the effect-monad and type-level-sets libraries. The relevant files from these are included with the download here for ease of use. The files comprising the contribution of the artifact are:
Control/Effect/Sessions.hs Control/Effect/Sessions/Process.lhs Control/Effect/Sessions/Operations.lhs Data/Type/FiniteMap.lhs examples.lhs effect-sessions.cabal
- The examples.lhs file in the top-level directory
provides a tutorial-like set of examples showing how to use
the library. Open this in GHC interactive mode via:
$ ghci examples.lhs ... Main*>
- The library has full Haddock documentation here. Most useful is the documentation for Control.Effect.Sessions.Operations which explains each combinator provided by the library for concurrency.
- The main examples.lhs provides tutorial.
TroubleshootingIf 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.
- A common cause of errors is not naming channels. Channels should be named whenever there is more than one channel being used in a computation block. If two endpoints of a channel are being bound in new then only one needs to be named.
- Occasionally, extra type annotations are needed on primitive types to restrict them from polymorphic to monomorphic instances. e.g., write (x :: Int) <- recv c instead of just x <- recv c.
- Check that the error isn't an expected error: e.g., the types of the process don't match up, or a balancing check fails, e.g. NotBal (Bal s).
- effect-sessions has been tested on the following architectures/versions:
- Mac OS X 10.9.5: GHC 7.8.2 and GHC 7.10.1
- Windows 7, GHC 7.10.2
- Ubuntu 15.04, GHC 7.10.2
- effect-sessions relies on the effect-monad and type-level-sets libraries. These are included with the download here for ease of use. These can also be installed via cabal (cabal install effect-monad, cabal install type-level-sets).
- effect-sessions itself can be installed
(though this isn't necessary for experimenting with the examples) via:
cabal configure cabal build cabal install
AcknowledgmentsThanks 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