TY - GEN
T1 - Haskell session types with (almost) no class
AU - Pucella, Riccardo
AU - Tov, Jesse A.
PY - 2008
Y1 - 2008
N2 - 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.
AB - 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.
KW - Concurrency
KW - Embedded type systems
KW - Functional programming
KW - Haskell
KW - Phantom types
KW - Session types
KW - Type classes
UR - http://www.scopus.com/inward/record.url?scp=78650422920&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=78650422920&partnerID=8YFLogxK
U2 - 10.1145/1411286.1411290
DO - 10.1145/1411286.1411290
M3 - Conference contribution
AN - SCOPUS:78650422920
SN - 9781605580647
T3 - Haskell'08 - Proceedings of the ACM SIGPLAN 2008 Haskell Symposium
SP - 25
EP - 36
BT - Haskell'08 - Proceedings of the ACM SIGPLAN 2008 Haskell Symposium
T2 - 1st ACM SIGPLAN Haskell Symposium, Haskell'08
Y2 - 25 September 2008 through 25 September 2008
ER -