# Semantics of value recursion for Monadic Input/Output

Levent Erkök; John Launchbury; Andrew Moran

RAIRO - Theoretical Informatics and Applications (2010)

- 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 36.2 (2010): 155-180. <http://eudml.org/doc/92695>.

@article{Erkök2010,

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.
},

author = {Erkök, Levent, Launchbury, John, Moran, Andrew},

journal = {RAIRO - Theoretical Informatics and Applications},

keywords = {monads; transition semantics},

language = {eng},

month = {3},

number = {2},

pages = {155-180},

publisher = {EDP Sciences},

title = {Semantics of value recursion for Monadic Input/Output},

url = {http://eudml.org/doc/92695},

volume = {36},

year = {2010},

}

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

DA - 2010/3//

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/92695

ER -

## References

top- 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
- Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106. Zbl0884.03008
- N. Benton and M. Hyland, Traced premonoidal categories (Extended Abstract), in Fixed Points in Computer Science Workshop, FICS'02 (2002).
- P. Bjesse, K. Claessen, M. Sheeran and S. Singh, Lava: Hardware design in Haskell, in International Conference on Functional Programming. Baltimore (1998).
- L. Erkök, Value recursion in monadic computations, Ph.D. Thesis. OGI School of Science and Engineering, OHSU, Portland, Oregon (2002). Zbl1011.68017
- 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
- L. Erkök, J. Launchbury and A. Moran, Semantics of fixIO, in Fixed Points in Computer Science Workshop, FICS'01 (2001).
- 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.68094
- A.D. Gordon, Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994).
- 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.68599
- M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999).
- J. Hughes, Generalising monads to arrows. Sci. Comput. Programming37 (2000) 67-111. Zbl0954.68034
- A. Jeffrey, Premonoidal categories and a graphical view of programs, Unpublished manuscript (1997).
- M.P. Jones, Typing Haskell in Haskell, in Proc. of the 1999 Haskell Workshop (1999).
- A. Joyal, R.H. Street and D. Verity, Traced monoidal categories. Math. Proc. Cambridge Philos. Soc. 119 (1996) 447-468. Zbl0845.18005
- 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.
- 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.
- J. Launchbury and S.L. Peyton Jones, State in Haskell. Lisp Symb. Comput.8 (1995) 293-341.
- 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).
- I.A. Mason and C.L. Talcott, Equivalence in functional languages with effects. J. Funct. Programming1 (1991) 287-327. Zbl0941.68540
- 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.
- R. Milner, Communicating and Mobile Systems: The π-Calculus. Cambridge University Press (1999). Zbl0942.68002
- E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991). Zbl0723.68073
- J. Nordlander, Reactive Objects and Functional Programming, Ph.D. Thesis. ChalmersUniversity of Technology, Göteborg, Sweden (1999).
- 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
- 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
- S.L. Peyton Jones and J. Hughes, Report on the programming language Haskell 98, a non-strict purely-functional programming language (1999).
- 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.
- A.M. Pitts, Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci.10 (2000) 321-359. Zbl0955.68024
- J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci.7 (1997) 453-468. Zbl0897.18002
- P. Sestoft, Deriving a lazy abstract machine. J. Funct. Programming7 (1997) 231-264. Zbl0881.68049
- 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.

## Citations in EuDML Documents

top## NotesEmbed ?

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