skip to main content
research-article

Haskell session types with (almost) no class

Published:25 September 2008Publication History
Skip Abstract Section

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.

Skip Supplemental Material Section

Supplemental Material

Video

References

  1. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  2. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  3. R. Atkey. Parameterized notions of computation. In Proc. Workshop on Mathematically Structured Functional Programming (MSFP'06). BCS, 2006. Google ScholarGoogle ScholarDigital LibraryDigital Library
  4. E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579--612, 1996.Google ScholarGoogle ScholarCross RefCross Ref
  5. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  6. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  7. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  8. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  9. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  10. S. J. Gay and M. J. Hole. Subtyping for session types in the pi calculus. Acta Informatica, 42(2/3):191--225, 2005.Google ScholarGoogle ScholarCross RefCross Ref
  11. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  12. S. J. Gay and V. T. Vasconcelos. Asynchronous functional session types. Technical Report 2007--251, Department of Computing, University of Glasgow, May 2007.Google ScholarGoogle Scholar
  13. 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 ScholarGoogle ScholarCross RefCross Ref
  14. 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 ScholarGoogle Scholar
  15. J. Gosling, B. Joy, G. Steele, and G. Bracha. The Java(TM) Language Specification. Addison Wesley, 3rd edition, 2005. Google ScholarGoogle ScholarDigital LibraryDigital Library
  16. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  17. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  18. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  19. O. Kiselyov. Simple variable-state 'monad'. Mailing list message, December 2006. URL http://www.haskell.org/pipermail/haskell/2006-December/018917.html.Google ScholarGoogle Scholar
  20. O. Kiselyov. Genuine shift/reset in Haskell98. Mailing list message, December 2007. URL http://www.haskell.org/pipermail/haskell/2007-December/020034.html.Google ScholarGoogle Scholar
  21. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  22. 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 ScholarGoogle ScholarCross RefCross Ref
  23. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  24. S. Peyton Jones, M. P. Jones, and E. Meijer. Type classes: An exploration of the design space, 1997.Google ScholarGoogle Scholar
  25. R. Pucella and A. Heller. Capability-based calculi for session types. Unpublished manuscript, 2008.Google ScholarGoogle Scholar
  26. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  27. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  28. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  29. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  30. I. E. Sutherland and G. W. Hodgman. Reentrant polygon clipping. Communications of the ACM, 17(1):32--42, January 1974. Google ScholarGoogle ScholarDigital LibraryDigital Library
  31. 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 ScholarGoogle Scholar
  32. 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 ScholarGoogle ScholarDigital LibraryDigital Library
  33. A. K. Wright and M. Felleisen. A syntactic approach to type soundness. Information and Computation, 115(1):38--94, 1994. Google ScholarGoogle ScholarDigital LibraryDigital Library

Index Terms

  1. Haskell session types with (almost) no class

      Recommendations

      Comments

      Login options

      Check if you have access through your login credentials or your institution to get full access on this article.

      Sign in

      Full Access

      • Published in

        cover image ACM SIGPLAN Notices
        ACM SIGPLAN Notices  Volume 44, Issue 2
        HASKELL '08
        February 2009
        126 pages
        ISSN:0362-1340
        EISSN:1558-1160
        DOI:10.1145/1543134
        Issue’s Table of Contents
        • cover image ACM Conferences
          Haskell '08: Proceedings of the first ACM SIGPLAN symposium on Haskell
          September 2008
          134 pages
          ISBN:9781605580647
          DOI:10.1145/1411286
          • Program Chair:
          • Andy Gill

        Copyright © 2008 ACM

        Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

        Publisher

        Association for Computing Machinery

        New York, NY, United States

        Publication History

        • Published: 25 September 2008

        Check for updates

        Qualifiers

        • research-article

      PDF Format

      View or Download as a PDF file.

      PDF

      eReader

      View online with eReader.

      eReader