An abstract monadic semantics for value recursion

Eugenio Moggi; Amr Sabry

RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications (2004)

  • Volume: 38, Issue: 4, page 375-400
  • ISSN: 0988-3754

Abstract

top
This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations.

How to cite

top

Moggi, Eugenio, and Sabry, Amr. "An abstract monadic semantics for value recursion." RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications 38.4 (2004): 375-400. <http://eudml.org/doc/245821>.

@article{Moggi2004,
abstract = {This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations.},
author = {Moggi, Eugenio, Sabry, Amr},
journal = {RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications},
language = {eng},
number = {4},
pages = {375-400},
publisher = {EDP-Sciences},
title = {An abstract monadic semantics for value recursion},
url = {http://eudml.org/doc/245821},
volume = {38},
year = {2004},
}

TY - JOUR
AU - Moggi, Eugenio
AU - Sabry, Amr
TI - An abstract monadic semantics for value recursion
JO - RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications
PY - 2004
PB - EDP-Sciences
VL - 38
IS - 4
SP - 375
EP - 400
AB - This paper proposes an operational semantics for value recursion in the context of monadic metalanguages. Our technique for combining value recursion with computational effects works uniformly for all monads. The operational nature of our approach is related to the implementation of recursion in Scheme and its monadic version proposed by Friedman and Sabry, but it defines a different semantics and does not rely on assignments. When contrasted to the axiomatic approach proposed by Erkök and Launchbury, our semantics for the continuation monad invalidates one of the axioms, adding to the evidence that this axiom is problematic in the presence of continuations.
LA - eng
UR - http://eudml.org/doc/245821
ER -

References

top
  1. [1] D. Ancona, Modular Formal Frameworks for Module Systems. Ph.D. Thesis, Univ. di Pisa (1998). 
  2. [2] D. Ancona, S. Fagorzi, E. Moggi and E. Zucca, Mixin modules and computational effects, in Proc. 30th Int’l Coll. Automata, Languages, and Programming, Springer-Verlag. Lect. Notes Comput. Sci. 2719 (2003). Zbl1039.68541
  3. [3] D. Ancona and E. Zucca, A primitive calculus for module systems, in Proc. Int’l Conf. Principles & Practice Declarative Programming. Springer-Verlag. Lect. Notes Comput. Sci. 1702 (1999) 62–79. 
  4. [4] D. Ancona and E. Zucca, A calculus of module systems. J. Funct. Programming 12 (2002) 91–132. Extended version of [3]. Zbl0994.68033
  5. [5] Z.M. Ariola and M. Felleisen, The call-by-need lambda calculus. J. Funct. Programming 7 (1997) 265–301. Zbl0887.68007
  6. [6] Z.M. Ariola, J. Maraist, M. Odersky, M. Felleisen and P. Wadler, A call-by-need lambda calculus in Conference record of POPL ’95, 22nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, papers presented at the Symposium: San Francisco, California, January 22–25, 1995, New York, USA, ACM Press (1995) 233–246. 
  7. [7] H.P. Barendregt, The Lambda Calculus: Its Syntax and Semantics, revised ed. North-Holland (1984). Zbl0551.03007MR774952
  8. [8] A. Bawden, Letrec and callcc implement references. Message to comp.lang.scheme (1988). 
  9. [9] N. Benton and M. Hyland, Traced pre-monoidal categories, in Fixed Points in Computer Science, July 20–21, 2002, edited by Z. Ésik and A. Ingólfsdóttir. BRICS Notes Series, NS-02-2 12–19. 
  10. [10] G. Boudol, The recursive record semantics of objects revisited. Lect. Notes Comput. Sci. 2028 (2001) 269–283. Zbl0977.68517
  11. [11] G. Boudol, The recursive record semantics of objects revisited. J. Funct. Programming 14 (2004) 263–315. Zbl1088.68036
  12. [12] G. Boudol and P. Zimmer, Recursion in the call-by-value λ -calculus. Fixed Points in Comput. Sci., BRICS Notes Series NS-02-2 (2002). 
  13. [13] G. Bracha, The Programming Language Jigsaw: Mixins, Modularity, and Multiple Inheritance. Ph.D. Thesis, Univ. of Utah (Mar. 1992). 
  14. [14] M. Carlsson, Value recursion in the continuation monad. Unpublished Note (2003). 
  15. [15] W. Cook, A Denotational Semantics of Inheritance. Ph.D. Thesis, Brown University (1989). 
  16. [16] W. Cook and J. Palsberg, A denotational semantics of inheritance and its correctness, in Conf. on Object-Oriented Programming: Systems, Languages and Applications, ACM (1989). 
  17. [17] G. Cousineau, P.L. Curien and M. Mauny, The categorical abstract machine, in Functional Programming Languages and Computer Architecture, edited by J.-P. Jouannaud, Springer Verlag. Lect. Notes Comput. Sci. 201 (Sept. 1985) 50–64. Zbl0592.68045
  18. [18] D. Dreyer, R. Harper and K. Crary, A type system for well-founded recursion. Tech. Rep. CMU-CS-03-163, Carnegie Mellon University (2003). Zbl1321.68167
  19. [19] L. Erkök, Value Recursion in Monadic Computations. Ph.D. Thesis, OGI School of Science and Engineering, OHSU, Portland, Oregon (2002). Zbl1011.68017
  20. [20] L. Erkök and J. Launchbury, Recursive monadic bindings, in Proc. of the ACM Sigplan International Conference on Functional Programming (ICFP-00), New York, 18–21 Sept. ACM Sigplan Notices 35.9 (2000) 174–185. Zbl1321.68151
  21. [21] L. Erkök, J. Launchbury and A. Moran, Semantics of value recursion for monadic input/output. J. Theor. Inform. Appl. 36 (2002) 155–180. Zbl1011.68017
  22. [22] A. Filinski, Representing monads, in Conf. Record of 21st ACM SIGPLAN-SIGACT Symp. on Principles of Programming Languages, POPL’94, Portland, OR, USA, 17–21 Jan., ACM Press, New York (1994) 446–457. 
  23. [23] D.P. Friedman and A. Sabry, Recursion is a computational effect. Tech. Rep. 546, Computer Science Department, Indiana University (2000). 
  24. [24] T. GHC Team, The glasgow haskell compiler user’s guide, version 4.08. Available online from http://haskell.org/ghc/. Viewed on 12/28/2000. 
  25. [25] T. Hirschowitz, Mixin Modules, Modules and Extended Value Binding in a Call-By-Value Setting. Ph.D. Thesis, Univ. Paris 7 (2003). 
  26. [26] T. Hirschowitz and X. Leroy, Mixin modules in a call-by-value setting, in 11th European Symp. Programming, Springer-Verlag. Programming Languages & Systems 2305 (2002) 6–20. Zbl1077.68557
  27. [27] T. Hirschowitz, X. Leroy and J.B. Wells, Compilation of extended recursion in call-by-value functional languages, in Proc. 5th Int’l Conf. Principles & Practice Declarative Programming (2003). Zbl1183.68140
  28. [28] J. Hughes, Generalising monads to arrows. Sci. Comput. Program. 37 (2000) 67–111. Zbl0954.68034
  29. [29] Report on the programming language Haskell 98 (Feb. 1999). 
  30. [30] M.P. Jones and J.C. Peterson, Hugs 1.4 User Manual. Research Report YALEU/DCS/RR-1123. Yale University, Department of Computer Science (1997). 
  31. [31] R. Kelsey, W. Clinger and J. Ree, Revised report on the algorithmic language Scheme. ACM SIGPLAN Notices 33 (1998) 26–76. 
  32. [32] P.J. Landin, The mechanical evaluation of expressions. Comput. J. 6 (1964) 308–320. Zbl0122.36106
  33. [33] J. Launchbury, J.R. Lewis and B. Cook, On embedding a microarchitectural design language within Haskell, in Proc. 1999 Int’l Conf. Functional Programming, ACM Press (1999) 60–69. 
  34. [34] J. Maraist, M. Odersky and P. Wadler, The call-by-need lambda calculus. J. Funct. Programming 8 (1998) 275–317. Zbl0918.03019
  35. [35] E. Moggi and S. Fagorzi, A monadic multi-stage metalanguage, in Proc. FoSSaCS ’03, Springer-Verlag. Lect. Notes Comput. Sci. 2620 (2003). Zbl1029.68042
  36. [36] J.H. Morris, Lambda-Calculus Method of Programming Language. Ph.D. Thesis, MIT (Dec. 1968). 
  37. [37] R. Paterson, A new notation for arrows, in Proc. of the sixth ACM SIGPLAN international conference on Functional programming, ACM Press (2001) 229–240. Zbl1323.68147
  38. [38] J. Power and E. Robinson, Premonoidal categories and notions of computation. Math. Struct. Comput. Sci. 7 (1997) 453–468. Zbl0897.18002
  39. [39] O. Waddell, D. Sarkar and R.K. Dybvig, Robust and effective transformation of letrec, in Scheme Workshop (Oct. 2002). Zbl1086.68524
  40. [40] A. Wright and M. Felleisen, A syntactic approach to type soundness. Inform. Comput. 115 (1994) 38–94. Zbl0938.68559

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.