Haskell session types with (almost) no class

Subscribe (Full Service)


	Search: The ACM Digital Library The Guide

	Feedback

Haskell session types with (almost) no class

Full text

Pdf (278 KB)

Source

Haskell archive
Proceedings of the first ACM SIGPLAN symposium on Haskell table of contents

Victoria, BC, Canada

SESSION: Session 1 table of contents

Pages 25-36

Year of Publication: 2008

ISBN:978-1-60558-064-7

Also published in ...

Authors

Riccardo Pucella	Northeastern University, Boston, MA, USA
Jesse A. Tov	Northeastern University, Boston, MA, USA

Sponsors

SIGPLAN: ACM Special Interest Group on Programming Languages
ACM: Association for Computing Machinery

Publisher

ACM New York, NY, USA

Bibliometrics

Downloads (6 Weeks): 9, Downloads (12 Months): 99, Citation Count: 0

Additional Information:

abstract references index terms collaborative colleagues

Tools and Actions:	Request Permissions Review this Article Save this Article to a Binder Display Formats: BibTeX EndNote ACM Ref

DOI Bookmark:	Use this link to bookmark this Article: http://doi.acm.org/10.1145/1411286.1411290 What is a DOI?

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.

REFERENCES

Note: OCR errors may be found in this Reference List extracted from the full text article. ACM has opted to expose the complete List rather than only correct and linked references.

	1	Joe Armstrong, Getting Erlang to talk to the outside world, Proceedings of the 2002 ACM SIGPLAN workshop on Erlang, p.64-72, October 07-07, 2002, Pittsburgh, Pennsylvania [doi>10.1145/592849.592858]
	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.
	3	R. Atkey. Parameterized notions of computation. In Proc. Workshop on Mathematically Structured Functional Programming (MSFP'06). BCS, 2006.
	4	E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. Mathematical Structures in Computer Science, 6:579--612, 1996.
	5	Manuel M. T. Chakravarty , Gabriele Keller , Simon Peyton Jones , Simon Marlow, Associated types with class, Proceedings of the 32nd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.1-13, January 12-14, 2005, Long Beach, California, USA
	6	Robert DeLine , Manuel Fähndrich, Enforcing high-level protocols in low-level software, Proceedings of the ACM SIGPLAN 2001 conference on Programming language design and implementation, p.59-69, June 2001, Snowbird, Utah, United States
	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.
	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.
	9	Manuel Fähndrich , Mark Aiken , Chris Hawblitzel , Orion Hodson , Galen Hunt , James R. Larus , Steven Levi, Language support for fast and reliable message-based communication in singularity OS, Proceedings of the 1st ACM SIGOPS/EuroSys European Conference on Computer Systems 2006, April 18-21, 2006, Leuven, Belgium
	10	Simon Gay , Malcolm Hole, Subtyping for session types in the pi calculus, Acta Informatica, v.42 n.2, p.191-225, November 2005 [doi>10.1007/s00236-005-0177-z]
	11	Simon J. Gay , Malcolm Hole, Types and Subtypes for Client-Server Interactions, Proceedings of the 8th European Symposium on Programming Languages and Systems, p.74-90, March 22-28, 1999
	12	S. J. Gay and V. T. Vasconcelos. Asynchronous functional session types. Technical Report 2007--251, Department of Computing, University of Glasgow, May 2007.
	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.
	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.
	15	James Gosling , Bill Joy , Guy L. Steele, The Java Language Specification, Addison-Wesley Longman Publishing Co., Inc., Boston, MA, 1996
	16	Tim Harris , Simon Marlow , Simon Peyton-Jones , Maurice Herlihy, Composable memory transactions, Proceedings of the tenth ACM SIGPLAN symposium on Principles and practice of parallel programming, June 15-17, 2005, Chicago, IL, USA [doi>10.1145/1065944.1065952]
	17	Kohei Honda , Vasco Thudichum Vasconcelos , Makoto Kubo, Language Primitives and Type Discipline for Structured Communication-Based Programming, Proceedings of the 7th European Symposium on Programming: Programming Languages and Systems, p.122-138, March 28-April 04, 1998
	18	Mark P. Jones, Type Classes with Functional Dependencies, Proceedings of the 9th European Symposium on Programming Languages and Systems, p.230-244, April 02, 2000
	19	O. Kiselyov. Simple variable-state 'monad'. Mailing list message, December 2006. URL http://www.haskell.org/pipermail/haskell/2006-December/018917.html.
	20	O. Kiselyov. Genuine shift/reset in Haskell98. Mailing list message, December 2007. URL http://www.haskell.org/pipermail/haskell/2007-December/020034.html.
	21	Oleg Kiselyov , Ralf Lämmel , Keean Schupke, Strongly typed heterogeneous collections, Proceedings of the 2004 ACM SIGPLAN workshop on Haskell, September 22-22, 2004, Snowbird, Utah, USA [doi>10.1145/1017472.1017488]
	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.
	23	Simon Peyton Jones , Andrew Gordon , Sigbjorn Finne, Concurrent Haskell, Proceedings of the 23rd ACM SIGPLAN-SIGACT symposium on Principles of programming languages, p.295-308, January 21-24, 1996, St. Petersburg Beach, Florida, United States [doi>10.1145/237721.237794]
	24	S. Peyton Jones, M. P. Jones, and E. Meijer. Type classes: An exploration of the design space, 1997.
	25	R. Pucella and A. Heller. Capability-based calculi for session types. Unpublished manuscript, 2008.
	26	Didier Rémy , Jérôme Vouillon, Objective ML: an effective object-oriented extension to ML, Theory and Practice of Object Systems, v.4 n.1, p.27-50, 1998 [doi>10.1002/(SICI)1096-9942(1998)4:1<27::AID-TAPO3>3.0.CO;2-4]
	27	John H. Reppy, CML: A higher concurrent language, Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, p.293-305, June 24-28, 1991, Toronto, Ontario, Canada
	28	John C. Reynolds, Towards a theory of type structure, Programming Symposium, Proceedings Colloque sur la Programmation, p.408-423, April 09-11, 1974
	29	Olin Shivers , Matthew Might, Continuations and transducer composition, Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation, June 11-14, 2006, Ottawa, Ontario, Canada
	30	Ivan E. Sutherland , Gary W. Hodgman, Reentrant polygon clipping, Communications of the ACM, v.17 n.1, p.32-42, Jan. 1974 [doi>10.1145/360767.360802]
	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.
	32	Vasco T. Vasconcelos , Simon J. Gay , António Ravara, Type checking a multithreaded functional language with session types, Theoretical Computer Science, v.368 n.1-2, p.64-87, December, 2006 [doi>10.1016/j.tcs.2006.06.028]
	33	Andrew K. Wright , Matthias Felleisen, A syntactic approach to type soundness, Information and Computation, v.115 n.1, p.38-94, Nov. 15, 1994 [doi>10.1006/inco.1994.1093]