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

Voir la notice de l'article provenant de la source Numdam

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},
     publisher = {EDP-Sciences},
     volume = {36},
     number = {2},
     year = {2002},
     doi = {10.1051/ita:2002008},
     mrnumber = {1948767},
     zbl = {1011.68017},
     language = {en},
     url = {http://geodesic.mathdoc.fr/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  - http://geodesic.mathdoc.fr/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 http://geodesic.mathdoc.fr/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. http://geodesic.mathdoc.fr/articles/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 :