Semantics of value recursion for monadic input/output

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

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.

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

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

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

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

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

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

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

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

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

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

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

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

[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