# 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

## Access Full Article

top## Abstract

top## How to cite

topErkö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] 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] Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106. Zbl0884.03008MR1608938
- [3] N. Benton and M. Hyland, Traced premonoidal categories (Extended Abstract), in Fixed Points in Computer Science Workshop, FICS’02 (2002).
- [4] P. Bjesse, K. Claessen, M. Sheeran and S. Singh, Lava: Hardware design in Haskell, in International Conference on Functional Programming. Baltimore (1998).
- [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] 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] L. Erkök, J. Launchbury and A. Moran, Semantics of fixIO, in Fixed Points in Computer Science Workshop, FICS’01 (2001).
- [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] A.D. Gordon, Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994). Zbl0841.68022
- [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] M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999). Zbl0943.68109MR1696494
- [12] J. Hughes, Generalising monads to arrows. Sci. Comput. Programming 37 (2000) 67-111. Zbl0954.68034MR1766319
- [13] A. Jeffrey, Premonoidal categories and a graphical view of programs, Unpublished manuscript (1997). URL: fpl.cs.depaul.edu/ajeffrey/premon/paper.html
- [14] M.P. Jones, Typing Haskell in Haskell, in Proc. of the 1999 Haskell Workshop (1999).
- [15] A. Joyal, R.H. Street and D. Verity, Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119 (1996) 447-468. Zbl0845.18005MR1357057
- [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] 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] J. Launchbury and S.L. Peyton Jones, State in Haskell. Lisp Symb. Comput. 8 (1995) 293-341.
- [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] I.A. Mason and C.L. Talcott, Equivalence in functional languages with effects. J. Funct. Programming 1 (1991) 287-327. Zbl0941.68540MR1122962
- [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] R. Milner, Communicating and Mobile Systems: The $\pi $-Calculus. Cambridge University Press (1999). Zbl0942.68002MR1695885
- [23] E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991). Zbl0723.68073MR1115262
- [24] J. Nordlander, Reactive Objects and Functional Programming, Ph.D. Thesis. Chalmers University of Technology, Göteborg, Sweden (1999).
- [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] 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] 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] 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] A.M. Pitts, Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10 (2000) 321-359. Zbl0955.68024MR1771182
- [30] J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. Zbl0897.18002MR1486319
- [31] P. Sestoft, Deriving a lazy abstract machine. J. Funct. Programming 7 (1997) 231-264. Zbl0881.68049MR1473158
- [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 ?

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