Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-24T01:21:13.987Z Has data issue: false hasContentIssue false
  • English
  • Français

Semantics of value recursion for Monadic Input/Output

Published online by Cambridge University Press:  15 December 2002

Levent Erkök ,
John Launchbury  and
Andrew Moran
Levent Erkök
Affiliation:
OGI School of Science and Engineering, OHSU; [email protected].
John Launchbury
Affiliation:
OGI School of Science and Engineering, OHSU; [email protected]. Galois Connections, Inc.
Andrew Moran
Affiliation:
Galois Connections, Inc.
Get access

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.

Keywords

Type
Research Article
Information
RAIRO - Theoretical Informatics and Applications , Volume 36 , Issue 2: Fixed Points in Computer Science (FICS'01) , April 2002 , pp. 155 - 180
Copyright
© EDP Sciences, 2002

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

References

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.
Z.M. Ariola and S. Blom, Cyclic lambda calculi, in Theoretical Aspects of Computer Software (1997) 77-106.
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).
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.
L. Erkök, J. Launchbury and A. Moran, Semantics of fixIO, in Fixed Points in Computer Science Workshop, FICS'01 (2001).
Felleisen, M. and Hieb, R., A revised report on the syntactic theories of sequential control and state. Theoret. Comput. Sci. 103 (1992) 235-271. CrossRef
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. CrossRef
M. Hasegawa, Models of Sharing Graphs, A categorical semantics of let and letrec. Distinguished Dissertations in Computer Science. Springer Verlag (1999).
Hughes, J., Generalising monads to arrows. Sci. Comput. Programming 37 (2000) 67-111. CrossRef
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. CrossRef
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.
Launchbury, J. and Peyton Jones, S.L., State in Haskell. Lisp Symb. Comput. 8 (1995) 293-341. CrossRef
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).
Mason, I.A. and Talcott, C.L., Equivalence in functional languages with effects. J. Funct. Programming 1 (1991) 287-327. CrossRef
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).
E. Moggi, Notions of computation and monads. Inform. and Comput. 93 (1991).
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.
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.
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.
Pitts, A.M., Parametric polymorphism and operational equivalence. Math. Struct. Comput. Sci. 10 (2000) 321-359. CrossRef
Power, J. and Robinson, E., Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453-468. CrossRef
Sestoft, P., Deriving a lazy abstract machine. J. Funct. Programming 7 (1997) 231-264. CrossRef
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.