Abstract
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.
Supplemental Material
Available for Download
- J. Armstrong. Getting Erlang to talk to the outside world. In Proc. 2002 ACM SIGPLAN workshop on Erlang, pages 64--72. ACM Press, 2002. Google ScholarDigital Library
- K. Asai and Y. Kameyama. Polymorphic delimited continuations. In Programming Languages and Systems, volume 4807 of Lecture Notes in Computer Science, pages 239--254. Springer-Verlag, 2007. Google ScholarDigital Library
- R. Atkey. Parameterized notions of computation. In Proc. Workshop on Mathematically Structured Functional Programming (MSFP'06). BCS, 2006. Google ScholarDigital Library
- E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579--612, 1996.Google ScholarCross Ref
- M. M. T. Chakravarty, G. Keller, S. Peyton Jones, and S. Marlow. Associated types with class. In Proc. 32nd Annual ACM Symposium on Principles of Programming Languages (POPL'05), pages 1--13. ACM Press, 2005. Google ScholarDigital Library
- R. DeLine and M. Fähndrich. Enforcing high-level protocols in low-level software. In Proc. 2001 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'01). ACM Press, 2001. Google ScholarDigital Library
- M. Dezani-Ciancaglini, N. Yoshida, A. Ahern, and S. Drossopolou. A distributed object-oriented language with session types. In Proc. Symposium on Trustworthy Global Computing, volume 3706 of Lecture Notes in Computer Science. Springer-Verlag, 2005. Google ScholarDigital Library
- M. Dezani-Ciancaglini, D. Mostrous, N. Yoshida, and S. Drossopolou. Session types for object-oriented languages. In Proc. European Conference on Object-Oriented Programming (ECOOP'06). Springer-Verlag, 2006. Google ScholarDigital Library
- M. Fähndrich, M. Aiken, C. Hawblitzel, O. Hodson, G. Hunt, J. R. Larus, and S. Levi. Language support for fast and reliable message-based communication in Singularity OS. In Proc. 1st ACM SIGOPS/EuroSys European Conference on Computer Systems (EuroSys'2006), pages 177--190. ACM Press, 2006. Google ScholarDigital Library
- S. J. Gay and M. J. Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2/3):191--225, 2005.Google ScholarCross Ref
- S. J. Gay and M. J. Hole. Types and subtypes for client-server interactions. In Proc. 8th European Symposium on Programming (ESOP'99), volume 1576 of Lecture Notes in Computer Science, pages 74--90. Springer-Verlag, 1999. Google ScholarDigital Library
- S. J. Gay and V. T. Vasconcelos. Asynchronous functional session types. Technical Report 2007--251, Department of Computing, University of Glasgow, May 2007.Google Scholar
- J.-Y. Girard. Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination des coupures dans l'analyse et la théorie des types. In J. E. Fenstad, editor, Proc. Second Scandinavian Logic Symposium, pages 63--92. North-Holland, 1971.Google ScholarCross Ref
- J.-Y. Girard. Interprétation fonctionelle et élimination des coupures de l'arithmétique d'ordre supérieur. PhD thesis, Université Paris VI, 1972.Google Scholar
- J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java(TM) Language Specification. Addison Wesley, 3rd edition, 2005. Google ScholarDigital Library
- T. Harris, S. Marlow, S. Peyton Jones, and M. Herlihy. Composable memory transactions. In Proc. ACM SIGPLAN Symposium on on Principles and Practice of Parallel Programming (PPoPP'05). ACM Press, 2005. Google ScholarDigital Library
- K. Honda, V. Vasconcelos, and M. Kubo. Language primitives and type discipline for structured communication-based programming. In Proc. European Symposium on Programming Languages and Systems, volume 1381 of Lecture Notes in Computer Science, pages 122--138. Springer-Verlag, 1998. Google ScholarDigital Library
- M. P. Jones. Type classes with functional dependencies. In Programming Languages and Systems, volume 1782 of Lecture Notes in Computer Science, pages 230--244. Springer-Verlag, 2000. Google ScholarDigital Library
- O. Kiselyov. Simple variable-state 'monad'. Mailing list message, December 2006. URL http://www.haskell.org/pipermail/haskell/2006-December/018917.html.Google Scholar
- O. Kiselyov. Genuine shift/reset in Haskell98. Mailing list message, December 2007. URL http://www.haskell.org/pipermail/haskell/2007-December/020034.html.Google Scholar
- O. Kiselyov, R. Lammel, and K. Schupke. Strongly typed heterogeneous collections. In Proc. ACM SIGPLAN Workshop on Haskell (Haskell'04), pages 96--107. ACM Press, 2004. Google ScholarDigital Library
- M. Neubauer and P. Thiemann. An implementation of session types. In Proc. 7th International Symposium on Practical Aspects of Declarative Languages (PADL'04), volume 3057 of Lecture Notes in Computer Science, pages 56--70, 2004.Google ScholarCross Ref
- S. Peyton Jones, A. Gordon, and S. Finne. Concurrent Haskell. In Proc. 23rd Annual ACM Symposium on Principles of Programming Languages (POPL'96), pages 295--308. ACM Press, 1996. Google ScholarDigital Library
- S. Peyton Jones, M. P. Jones, and E. Meijer. Type classes: An exploration of the design space, 1997.Google Scholar
- R. Pucella and A. Heller. Capability-based calculi for session types. Unpublished manuscript, 2008.Google Scholar
- D. Rémy and J. Vouillon. Objective ML: An effective object-oriented extension to ML. Theory and Practice of Object Systems, 4(1):27--50, 1998. Google ScholarDigital Library
- J. H. Reppy. CML: A higher concurrent language. In Proc. 1991 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'91), volume 26, pages 293--305. ACM Press, 1991. Google ScholarDigital Library
- J. C. Reynolds. Towards a theory of type structure. In Proc. Colloque sur la Programmation, volume 19 of Lecture Notes in Computer Science, pages 408--425. Springer-Verlag, 1974. Google ScholarDigital Library
- O. Shivers and M. Might. Continuations and transducer composition. In Proc. 2006 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI'06), pages 295--307. ACM Press, 2006. Google ScholarDigital Library
- I. E. Sutherland and G. W. Hodgman. Reentrant polygon clipping. Communications of the ACM, 17(1):32--42, January 1974. Google ScholarDigital Library
- A. Vallecillo, V. T. Vasconcelos, and A. Ravara. Typing the behavior of objects and components using session types. In Proc. International Workshop on Foundations of Coordination Languages and Software Architectures, volume 68(3) of Electronic Notes in Theoretical Computer Science. Elsevier Science Publishers, 2003.Google Scholar
- V. T. Vasconcelos, S. J. Gay, and A. Ravara. Typechecking a multithreaded functional language with session types. Theoretical Computer Science, 368(1-2): 64--87, 2006. Google ScholarDigital Library
- A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994. Google ScholarDigital Library
Index Terms
Haskell session types with (almost) no class
Recommendations
Haskell session types with (almost) no class
Haskell '08: Proceedings of the first ACM SIGPLAN symposium on HaskellWe 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 ...
Type classes in Haskell
This article defines a set of type inference rules for resolving overloading introduced by type classes, as used in the functional programming language Haskell. Programs including type classes are transformed into ones which may be typed by standard ...
Polymorphic variants in Haskell
Haskell '06: Proceedings of the 2006 ACM SIGPLAN workshop on HaskellIn languages that support polymorphic variants, a single variant value can be passed to many contexts that accept different sets of constructors. Polymorphic variants can be used in order to introduce extensible algebraic datatypes into functional ...
Comments