Session types in Cloud Haskell

Abstract

The implemention of a communication protocol is susceptible to human errors. Two processes engaging in such a protocol can deadlock or crash if their implementation of the protocol is faulty. In the context of Cloud Haskell, a distributed programming library for Haskell, we address this problem by providing a library for annotating Cloud Haskell programs with session types. A session type describes a protocol and by annotating a program with a session type we produce a static guarantee that the program correctly implements the protocol. We demonstrate how we use a deep-embedded domain-specific language for writing session typed programs to define several interpreters that can evaluate session typed programs. The most important interpreter is the one that evaluates a session typed program to Cloud Haskell semantics. Other interpreters can purely evaluate a session typed program, interactively step through a session typed program, visualize a session type using a diagram and normalize session typed programs to normal form. We introduce an optimization that reduces the amount of administrative communication required for n-ary nested branching session types. Further, we also introduce an optimization that turns the quadratic complexity of any session typed program, caused by left-associatively nested binds, into linear complexity using the codensity monad. To conclude, we measured the performance overhead that our library introduces compared to that of the Cloud Haskell library.