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

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 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
  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.  
  2. Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106.  
  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).  
  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.  
  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.  
  9. A.D. Gordon, Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994).  
  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.  
  11. M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999).  
  12. J. Hughes, Generalising monads to arrows. Sci. Comput. Programming37 (2000) 67-111.  
  13. A. Jeffrey, Premonoidal categories and a graphical view of programs, Unpublished manuscript (1997).  
  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.  
  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. Programming1 (1991) 287-327.  
  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 π-Calculus. Cambridge University Press (1999).  
  23. E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991).  
  24. J. Nordlander, Reactive Objects and Functional Programming, Ph.D. Thesis. ChalmersUniversity 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.  
  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.  
  27. S.L. Peyton Jones and J. Hughes, Report on the programming language Haskell 98, a non-strict purely-functional programming language (1999).  
  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.  
  30. J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci.7 (1997) 453-468.  
  31. P. Sestoft, Deriving a lazy abstract machine. J. Funct. Programming7 (1997) 231-264.  
  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.  

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.