Semantics of value recursion for monadic input/output

Levent Erkök; John Launchbury; Andrew Moran[1]

  • [1] Galois Connections, Inc.

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2002)

  • Volume: 36, Issue: 2, page 155-180
  • ISSN: 0988-3754

Abstract

top
Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell’s IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this paper, we describe a semantics for a lazy language based on Haskell, supporting monadic I/O, mutable variables, usual recursive definitions, and value recursion. Our semantics is composed of two layers: a natural semantics for the functional layer, and a labeled transition semantics for the IO layer.

How to cite

top

Erkök, Levent, Launchbury, John, and Moran, Andrew. "Semantics of value recursion for monadic input/output." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 36.2 (2002): 155-180. <http://eudml.org/doc/245819>.

@article{Erkök2002,
abstract = {Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell’s IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this paper, we describe a semantics for a lazy language based on Haskell, supporting monadic I/O, mutable variables, usual recursive definitions, and value recursion. Our semantics is composed of two layers: a natural semantics for the functional layer, and a labeled transition semantics for the IO layer.},
affiliation = {Galois Connections, Inc.},
author = {Erkök, Levent, Launchbury, John, Moran, Andrew},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
keywords = {monads; transition semantics},
language = {eng},
number = {2},
pages = {155-180},
publisher = {EDP-Sciences},
title = {Semantics of value recursion for monadic input/output},
url = {http://eudml.org/doc/245819},
volume = {36},
year = {2002},
}

TY - JOUR
AU - Erkök, Levent
AU - Launchbury, John
AU - Moran, Andrew
TI - Semantics of value recursion for monadic input/output
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2002
PB - EDP-Sciences
VL - 36
IS - 2
SP - 155
EP - 180
AB - Monads have been employed in programming languages for modeling various language features, most importantly those that involve side effects. In particular, Haskell’s IO monad provides access to I/O operations and mutable variables, without compromising referential transparency. Cyclic definitions that involve monadic computations give rise to the concept of value-recursion, where the fixed-point computation takes place only over the values, without repeating or losing effects. In this paper, we describe a semantics for a lazy language based on Haskell, supporting monadic I/O, mutable variables, usual recursive definitions, and value recursion. Our semantics is composed of two layers: a natural semantics for the functional layer, and a labeled transition semantics for the IO layer.
LA - eng
KW - monads; transition semantics
UR - http://eudml.org/doc/245819
ER -

References

top
  1. [1] P. Achten and S. Peyton Jones, Porting the Clean Object I/O Library to Haskell, in Proc. of the 12th International Workshop on Implementation of Functional Languages (2000) 194-213. Zbl0977.68728
  2. [2] Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106. Zbl0884.03008MR1608938
  3. [3] N. Benton and M. Hyland, Traced premonoidal categories (Extended Abstract), in Fixed Points in Computer Science Workshop, FICS’02 (2002). 
  4. [4] P. Bjesse, K. Claessen, M. Sheeran and S. Singh, Lava: Hardware design in Haskell, in International Conference on Functional Programming. Baltimore (1998). 
  5. [5] L. Erkök, Value recursion in monadic computations, Ph.D. Thesis. OGI School of Science and Engineering, OHSU, Portland, Oregon (2002). Zbl1011.68017
  6. [6] L. Erkök and J. Launchbury, Recursive monadic bindings, in Proc. of the Fifth ACM SIGPLAN International Conference on Functional Programming, ICFP’00. ACM Press (2000) 174-185. Zbl1321.68151
  7. [7] L. Erkök, J. Launchbury and A. Moran, Semantics of fixIO, in Fixed Points in Computer Science Workshop, FICS’01 (2001). 
  8. [8] M. Felleisen and R. Hieb, A revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103 (1992) 235-271. Zbl0764.68094MR1185458
  9. [9] A.D. Gordon, Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994). Zbl0841.68022
  10. [10] M. Hasegawa, Recursion from cyclic sharing: Traced monoidal categories and models of cyclic lambda calculi, in Typed Lambda Calculus and Applications (1997) 196-213. Zbl1063.68599MR1480472
  11. [11] M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999). Zbl0943.68109MR1696494
  12. [12] J. Hughes, Generalising monads to arrows. Sci. Comput. Programming 37 (2000) 67-111. Zbl0954.68034MR1766319
  13. [13] A. Jeffrey, Premonoidal categories and a graphical view of programs, Unpublished manuscript (1997). URL: fpl.cs.depaul.edu/ajeffrey/premon/paper.html 
  14. [14] M.P. Jones, Typing Haskell in Haskell, in Proc. of the 1999 Haskell Workshop (1999). 
  15. [15] A. Joyal, R.H. Street and D. Verity, Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119 (1996) 447-468. Zbl0845.18005MR1357057
  16. [16] J. Launchbury, A natural semantics for lazy evaluation, in Conference record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Charleston, South Carolina (1993) 144-154. 
  17. [17] J. Launchbury, J. Lewis and B. Cook, On embedding a microarchitectural design language within Haskell, in Proc. of the ACM SIGPLAN International Conference on Functional Programming (ICFP ’99) (1999) 60-69. 
  18. [18] J. Launchbury and S.L. Peyton Jones, State in Haskell. Lisp Symb. Comput. 8 (1995) 293-341. 
  19. [19] S. Marlow, S.L. Peyton Jones, A. Moran and J. Reppy, Asynchronous exceptions in Haskell, in ACM SIGPLAN 2001 Conference on Programming Language Design and Implementation (PLDI). Snowbird, Utah (2001). 
  20. [20] I.A. Mason and C.L. Talcott, Equivalence in functional languages with effects. J. Funct. Programming 1 (1991) 287-327. Zbl0941.68540MR1122962
  21. [21] J. Matthews, B. Cook and J. Launchbury, Microprocessor specification in Hawk, in Proc. of the 1998 International Conference on Computer Languages. IEEE Computer Society Press (1998) 90-101. 
  22. [22] R. Milner, Communicating and Mobile Systems: The π -Calculus. Cambridge University Press (1999). Zbl0942.68002MR1695885
  23. [23] E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991). Zbl0723.68073MR1115262
  24. [24] J. Nordlander, Reactive Objects and Functional Programming, Ph.D. Thesis. Chalmers University of Technology, Göteborg, Sweden (1999). 
  25. [25] R. Paterson, A new notation for arrows, in Proc. of the Sixth ACM SIGPLAN International Conference on Functional Programming, ICFP’01, Florence, Italy. ACM Press (2001) 229-240. Zbl1323.68147
  26. [26] S.L. Peyton Jones, Tackling the awkward squad: monadic input/output, concurrency, exceptions, and foreign-language calls in Haskell, in Engineering theories of software construction, edited by T. Hoare, M. Broy and R. Steinbruggen. IOS Press (2001) 47-96. Zbl0989.68021
  27. [27] S.L. Peyton Jones and J. Hughes, Report on the programming language Haskell 98, a non-strict purely-functional programming language (1999). URL: www.haskell.org/onlinereport 
  28. [28] S.L. Peyton Jones and P. Wadler, Imperative functional programming, in Conference record of the Twentieth Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. Charleston, South Carolina (1993) 71-84. 
  29. [29] A.M. Pitts, Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10 (2000) 321-359. Zbl0955.68024MR1771182
  30. [30] J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. Zbl0897.18002MR1486319
  31. [31] P. Sestoft, Deriving a lazy abstract machine. J. Funct. Programming 7 (1997) 231-264. Zbl0881.68049MR1473158
  32. [32] A. Simpson and G. Plotkin, Complete axioms for categorical fixed-point operators, in Proc. of the Fifteenth Annual IEEE Symposium on Logic in Computer Science (2000) 30-41. MR1946083

NotesEmbed ?

top

You must be logged in to post comments.

To embed these notes on your page include the following JavaScript code on your page where you want the notes to appear.

Only the controls for the widget will be shown in your chosen language. Notes will be shown in their authored language.

Tells the widget how many notes to show per page. You can cycle through additional notes using the next and previous controls.

    
                

                
Note: Best practice suggests putting the JavaScript code just before the closing </body> tag.