no. 2
Semantics of value recursion for monadic input/output
Erkök, Levent ; Launchbury, John  ; Moran, Andrew1
1 Galois Connections, Inc.
RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 2, pp. 155-180

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.

DOI : 10.1051/ita:2002008
Classification : 68N18, 68Q55, 18C15

Erkök, Levent  ; Launchbury, John  ; Moran, Andrew 1

1 Galois Connections, Inc. 
@article{ITA_2002__36_2_155_0,
     author = {Erk\"ok, Levent and Launchbury, John and Moran, Andrew},
     title = {Semantics of value recursion for monadic input/output},
     journal = {RAIRO - Theoretical Informatics and Applications - Informatique Th\'eorique et Applications},
     pages = {155--180},
     year = {2002},
     publisher = {EDP Sciences},
     volume = {36},
     number = {2},
     doi = {10.1051/ita:2002008},
     mrnumber = {1948767},
     zbl = {1011.68017},
     language = {en},
     url = {https://www.numdam.org/articles/10.1051/ita:2002008/}
}
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
SP  - 155
EP  - 180
VL  - 36
IS  - 2
PB  - EDP Sciences
UR  - https://www.numdam.org/articles/10.1051/ita:2002008/
DO  - 10.1051/ita:2002008
LA  - en
ID  - ITA_2002__36_2_155_0
ER  - 
%0 Journal Article
%A Erkök, Levent
%A Launchbury, John
%A Moran, Andrew
%T Semantics of value recursion for monadic input/output
%J RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
%D 2002
%P 155-180
%V 36
%N 2
%I EDP Sciences
%U https://www.numdam.org/articles/10.1051/ita:2002008/
%R 10.1051/ita:2002008
%G en
%F ITA_2002__36_2_155_0
Erkök, Levent; Launchbury, John; Moran, Andrew. Semantics of value recursion for monadic input/output. RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, Tome 36 (2002) no. 2, pp. 155-180. doi: 10.1051/ita:2002008

[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. | Zbl

[2] Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106. | Zbl | MR

[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. | Zbl | MR

[9] A.D. Gordon, Functional Programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994). | Zbl

[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. | Zbl | MR

[11] M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999). | Zbl | MR

[12] J. Hughes, Generalising monads to arrows. Sci. Comput. Programming 37 (2000) 67-111. | Zbl | MR

[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. | Zbl | MR

[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. | Zbl | MR

[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). | Zbl | MR

[23] E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991). | Zbl | MR

[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.

[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. | Zbl

[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. | Zbl | MR

[30] J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. | Zbl | MR

[31] P. Sestoft, Deriving a lazy abstract machine. J. Funct. Programming 7 (1997) 231-264. | Zbl | MR

[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. | MR

Cité par Sources :