Abstract
A session type is an abstraction of a set of sequences of heterogeneous values sent and received over a communication channel. Session types can be used for specifying stream-based Internet protocols.
Typically, session types are attached to communication-based program calculi, which renders them theoretical tools which are not readily usable in practice. To transfer session types into practice, we propose an embedding of a core calculus with session types into the functional programming language Haskell. The embedding preserves typing. A case study (a client for SMTP, the Simple Mail Transfer Protocol) demonstrates the feasibility of our approach.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Amtoft, T., Nielson, F., Nielson, H.R.: Type and Effect Systems: Behaviours for Concurrency. Imperial College Press, London (1999)
Armstrong, J.: Getting erlang to talk to the outside world. In: Proceedings of the 2002 ACM SIGPLAN workshop on Erlang, pp. 64–72. ACM Press, New York (2002)
Baars, A.I., Doaitse Swierstra, S.: Typing dynamic typing. In: Peyton-Jones [24], pp. 157–166
Benton, N., Kennedy, A.: Interlanguage working without tears: Blending SML with Java. In: Lee, P. (ed.) Proc. International Conference on Functional Programming 1999, Paris, France, September 1999, pp. 126–137. ACM Press, New York (1999)
Berry, G., Boudol, G.: The chemical abstract machine. Theoretical Computer Science 96 (1992)
Chen, C., Xi, H.: Meta-programming through typeful code representation. In: Olin Shivers, editor, Proc. International Conference on Functional Programming 2003, Uppsala, Sweden, August 2003, pp. 275–286. ACM Press, New York (2003)
Cheney, J., Hinze, R.: A lightweight implementation of generics and dynamics. In: Proceedings of the ACM SIGPLAN workshop on Haskell, pp. 90–104. ACM Press, New York (2002)
Danvy, O., Rhiger, M., Rose, K.: Normalization by evaluation with typed abstract syntax. Journal of Functional Programming 11(6), 673–680 (2001)
Fournet, C., Gonthier, G.: The reflexive CHAM and the join-calculus. In: POPL 1996 [28], pp. 372–385
Gay, S., Hole, M.: Types and subtypes for client-server interactions. In: Swierstra, S.D. (ed.) ESOP 1999. LNCS, vol. 1576, pp. 74–90. Springer, Heidelberg (1999)
Gay, S., Vasconcelos, V., Ravara, A.: Session types for inter-process communication. Technical Report TR-2003-133, Department of Computing Science, University of Glasgow (2003)
Giacalone, A., Mishra, P., Prasad, S.: FACILE: A symmetric integration of concurrent and functional programming. In: Díaz, J., Orejas, F. (eds.) CAAP 1989 and TAPSOFT 1989. LNCS, vol. 351, pp. 184–209. Springer, Heidelberg (1989)
Haskell 98, a non-strict, purely functional language (December 1998), http://www.haskell.org/definition
Honda, K., Tokoro, M.: An object calculus for asynchronous communication. In: America, P. (ed.) ECOOP 1991. LNCS, vol. 512, pp. 133–147. Springer, Heidelberg (1991)
Honda, K., Vasconcelos, V.T., Kubo, M.: Language primitives and type discipline for structured communication-based programming. In: Hankin, C. (ed.) ESOP 1998. LNCS, vol. 1381, pp. 122–138. Springer, Heidelberg (1998)
Jones, M.P.: Type classes with functional dependencies. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 230–244. Springer, Heidelberg (2000)
Leijen, D., Meijer, E.: Domain-specific embedded compilers. In: 2nd Conference on Domain-Specific Languages, Austin, Texas, USA (October 1999), USENIX http://usenix.org/events/dsl99/index.html
McBride, C.: Faking it—simulating dependent types in Haskell (2001), http://www.dur.ac.uk/~dcs1ctm/faking.ps
Meijer, E., Hutton, G.: Bananas in space: Extending fold and unfold to exponential types. In: Jones, S.P. (ed.) Proc. Functional Programming Languages and Computer Architecture 1995, La Jolla, CA, June 1995, pp. 324–333. ACM Press, New York (1995)
Milner, R.: Communication and Concurrency. Prentice Hall, Englewood Cliffs (1989)
Milner, R., Parrow, J., Walker, D.: A calculus of mobile processes, Part I + II. Information and Control 100(1), 1–77 (1992)
Neubauer, M., Thiemann, P., Gasbichler, M., Sperber, M.: A functional notation for functional dependencies. In: Hinze, R. (ed.) Proceedings of the 2001 Haskell Workshop (2001) to appear
Odersky, M., Läufer, K.: Putting type annotations to work. In: POPL 1996 [28], pp. 54–67
Peyton-Jones, S. (ed.) International Conference on Functional Programming, Pittsburgh, PA, USA, October 2002, ACM Press, New York (2002)
Jones, S.P., Gordon, A., Finne, S.: Concurrent Haskell. In: POPL 1996 [28], pp. 295–308
Jones, S.P., Meijer, E., Leijen, D.: Scripting COM components in Haskell. In: Proc. International Conference of Software Reuse (1998)
Jones, S.L.P.: Tackling the awkward squad: Monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell. In: Hoare, T., Broy, M., Steinbruggen, R. (eds.) Engineering Theories of Software Construction, pp. 47–96. IOS Press, Amsterdam (2001)
Proceedings of the 1996 ACM SIGPLAN Symposium on Principles of Programming Languages, St. Petersburg, FL, USA, January 1996, ACM Press, New York (1996)
Reppy, J.H.: Concurrent Programming in ML. Cambridge University Press, Cambridge (1999)
Simple mail transfer protocol (April 2001), http://www.faqs.org/rfcs/rfc2821.html
Rhiger, M.: A foundation for embedded languages. ACM Transactions on Programming Languages and Systems 25(3), 291–315 (2003)
Schmitt, A., Stefani, J.-B.: The m-calculus: a higher-order distributed process calculus. In: Proceedings of the 30th ACM SIGPLAN-SIGACT symposium on Principles of programming languages, pp. 50–61. ACM Press, New York (2003)
Stuckey, P.J., Sulzmann, M.: A theory of overloading. In: Peyton-Jones [24], pp. 167–178
Weirich, S.: Type-safe cast: Functional pearl. In: Philip Wadler, editor, Proc. International Conference on Functional Programming 2000, Montreal, Canada, September 2000, pp. 58–67. ACM Press, New York (2000)
Yang, Z.: Encoding types in ML-like languages. In: Paul Hudak, editor, Proc. International Conference on Functional Programming 1998, Baltimore, USA, September 1998, pp. 289–300. ACM Press, New York (1998)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2004 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Neubauer, M., Thiemann, P. (2004). An Implementation of Session Types. In: Jayaraman, B. (eds) Practical Aspects of Declarative Languages. PADL 2004. Lecture Notes in Computer Science, vol 3057. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-24836-1_5
Download citation
DOI: https://doi.org/10.1007/978-3-540-24836-1_5
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-22253-8
Online ISBN: 978-3-540-24836-1
eBook Packages: Springer Book Archive