Hostname: page-component-cd9895bd7-jkksz Total loading time: 0 Render date: 2024-12-25T17:47:22.690Z Has data issue: false hasContentIssue false
  • English
  • Français

Parameterised notions of computation

Part of: JFP Research Articles

Published online by Cambridge University Press:  01 July 2009

ROBERT ATKEY
ROBERT ATKEY*
Affiliation:
Laboratory for Foundations of Computer Science, School of Informatics, University of Edinburgh, Informatics Forum, 10 Crichton Street, Edinburgh EH8 9AB, UK (e-mail: bob.atkey@ed.ac.uk)
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Moggi's Computational Monads and Power et al.'s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages. Examples include non-termination, non-determinism, exceptions, continuations, side effects and input/output. We present generalisations of both computational monads and Freyd categories, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters. Examples of such are composable continuations, side effects where the type of the state varies and input/output where the range of inputs and outputs varies. By considering structured parameterisation also, we extend the range of effects to cover separated side effects and multiple independent streams of I/O. We also present two typed λ-calculi that soundly and completely model our categorical definitions – with and without symmetric monoidal parameterisation – and act as prototypical languages with parameterised effects.

Type
Articles
Information
Journal of Functional Programming , Volume 19 , Issue 3-4 , July 2009 , pp. 335 - 376
Copyright
Copyright © Cambridge University Press 2009

References

Atkey, R. (2006) Substructural Simple Type Theories for Separation and In-place Update. PhD thesis, University of Edinburgh.Google Scholar
Barendsen, E. & Smetsers, S. (1993) Conventional and uniqueness typing in graph rewrite systems (extended abstract). In Proceedings of the 13th Conference on the Foundations of Software Technology and Theoretical Computer Science, FSTTCS '93 (Bombay, December 1993), Shyamasundar, R. K. (ed). Lecture Notes in Computer Science, vol. 761. Springer, pp. 41–51.Google Scholar
Benton, N., Kennedy, A., Hofmann, M. & Beringer, L. (2006) Reading, writing and relations. In Proceedings of the 4th Asian Symposium on Programming Languages and Systems, APLAS 2006 (Sydney, November 2006), Kobayashi, N. (ed). Lecture Notes in Computer Science, vol. 4279. Springer, pp. 114–139.Google Scholar
Birkedal, L., Torp-Smith, N. & Yang, H. (2006) Semantics of separation-logic typing and higher-order frame rules for Algol-like languages, Logical Meth. Comput. Sci. 2 (5), article 1.Google Scholar
Danvy, O. & Filinski, A. (1989) A functional abstraction of typed contexts. Technical Report 89/12, Computer Science Department, University of Copenhagen.Google Scholar
Ghani, N. (1995) Adjoint Rewriting. PhD thesis, University of Edinburgh.Google Scholar
Girard, J.-Y. (1987) Linear logic, Theor. Comput. Sci. 50 (1): 1–101.CrossRefGoogle Scholar
Harrington, D. (2006) Uniqueness logic, Theor. Comput. Sci. 354 (1): 24–41.CrossRefGoogle Scholar
Hofmann, M. (2000) A type system for bounded space and functional in-place update, Nordic J. Comput. 7 (4): 258–289.Google Scholar
Levy, P. B., Power, J. & Thielecke, H. (2003) Modelling environments in call-by-value programming languages, Info. Comput. 185 (2): 182–210.CrossRefGoogle Scholar
Lucassen, J. M. & Gifford, D. K. (1988) Polymorphic effect systems. In Conference Record of 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL '88, San Diego, CA, January 1988. ACM Press, pp. 47–57.CrossRefGoogle Scholar
Mac Lane, S. (1998) Categories for the Working Mathematician, 2nd ed., Graduate Texts in Mathematics, vol. 5. Springer.Google Scholar
Moggi, E. (1989) Computational lambda-calculus and monads. In Proceedings of the 4th Annual IEEE Symposium on Logic in Computer Science, LICS '89 (Pacific Grove, CA, June 1989), IEEE CS Press, pp. 14–23.Google Scholar
Moggi, E. (1991) Notions of computation and monads, Info. Comput. 93 (1): 55–92.CrossRefGoogle Scholar
Morrisett, G., Ahmed, A. & Fluet, M. (2005) L3: A linear language with locations. In Proceedings of the 7th International Conference on Typed Lambda Calculi and Applications, TLCA 2005 (Nara, April 2005), Urzyczyn, P. (ed). Lecture Notes in Computer Science, vol. 3461. Springer, pp. 293–307.Google Scholar
Nanevski, A., Morrisett, G. & Birkedal, L. (2006) Polymorphism and separation in Hoare type theory. In Proceedings of the 11th ACM SIGPLAN International Conference on Functional Programming, ICFP '06 (Portland, OR, September 2006), ACM Press, pp. 62–73.Google Scholar
Nielson, F. & Riis Nielson, H. (1996) From CML to its process algebra, Theor. Comput. Sci. 155 (1): 179–219.CrossRefGoogle Scholar
O'Hearn, P., Reynolds, J. & Yang, H. (2001) Local reasoning about programs that alter data structures. In Proceedings of the 15th International Workshop on Computer Science Logic, CSL 2001 (Paris, September 2001), Fribourg, L. (ed). Lecture Notes in Computer Science, vol. 2142. Springer, pp. 1–19.Google Scholar
O'Hearn, P. W., Yang, H. & Reynolds, J. C. (2004) Separation and information hiding. In Proceedings of the 31st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2004 (Venice, January 2004), ACM Press, pp. 268–280.Google Scholar
Peyton Jones, S. L. & Wadler, P. (1993) Imperative functional programming. In Conference Record of 20th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 1993, Charleston, SC, January 1993. ACM Press, pp. 71–84.CrossRefGoogle Scholar
Plotkin, G. & Power, J. (2002) Notions of computation determine monads. In Proceedings of the 5th International Conference on Foundations of Software Science and Computation Structures, FoSSaCS 2002 (Grenoble, April 2002), Nielsen, M. & Engberg, U. (eds). Lecture Notes in Computer Science, vol. 2303. Springer, pp. 342–356.Google Scholar
Power, J. & Robinson, E. (1997) Premonoidal categories and notions of computation, Math. Struct. Comput. Sci. 7 (5): 453–468.CrossRefGoogle Scholar
Power, J. & Thielecke, H. (1999) Closed Freyd- and k-categories. In Proceedings of the 26th International Colloquium on Automata, Languages and Programming, ICALP 1999 (Prague, July 1999), Wiedermann, J., van Emde Boas, P. & Nielsen, M. (eds). Lecture Notes in Computer Science, vol. 1644. Springer, pp. 625–634.Google Scholar
Skalka, C. & Smith, S. (2004) History effects and verification. In Proceedings of the 2nd Asian Symposium on Programming Languages and Systems, APLAS 2004 (Taipei, November 2004), Chin, W.-N. (ed). Lecture Notes in Computer Science, vol. 3302. Springer, pp. 107–128.Google Scholar
Smith, F., Walker, D. & Morrisett, G. (2000) Alias types. In Proceedings of the 9th European Symposium on Programming, ESOP 2000 (Berlin, March/April 2000), Smolka, G. (ed). Lecture Notes in Computer Science, vol. 1782. Springer, pp. 366–381.Google Scholar
Taylor, P. (1999) Practical Foundations of Mathematics. Cambridge Studies in Advanced Mathematics, vol. 59. Cambridge University Press.Google Scholar
Thielecke, H. (1997) Categorical Structure of Continuation Passing Style. PhD thesis, University of Edinburgh.Google Scholar
Uustalu, T. (2003) Generalizing substitution, Generalizing substitution 37 (4): 315–336.Google Scholar
Vasconcelos, V., Gay, S. & Ravara, A. (2006) Typechecking a multithreaded functional language with session types, Typechecking a multithreaded functional language with session types 368 (1–2): 64–87.Google Scholar
Wadler, P. (1990) Linear types can change the world! In Proceedings of the IFIP WG2.2/2.3 Working Conference on Programming Concepts and Methods (Tiberias, April 1990), Broy, M. & Jones, C. (eds). North-Holland, pp. 561–581.Google Scholar
Wadler, P. (1991) Is there a use for linear logic? In Proceedings of the 1991 ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM 1991 (New Haven, CT, June 1991), ACM Press, pp. 255–273.Google Scholar
Wadler, P. (1994) Monads and composable continuations, Monads and composable continuations 7 (1): 39–56.Google Scholar
Wadler, P. & Thiemann, P. (2003) The marriage of effects and monads, The marriage of effects and monads 4 (1): 1–32.Google Scholar
Walker, D. (2005) Substructural type systems. In Advanced Topics in Types and Programming Languages, Pierce, B. C. (ed). MIT Press pp. 3–43.Google Scholar
Walker, D., Crary, K. & Morrisett, G. (2000) Typed memory management via static capabilities, Typed memory management via static capabilities 22 (4): 701–771.Google Scholar
Walker, D. & Morrisett, G. (2000) Alias types for recursive data structures. In Revised Selected Papers from 3rd International Workshop on Types in Compilation, TIC 2000, Montreal, September 2000, Harper, R. (ed). Lecture Notes in Computer Science, vol. 2071. Springer, pp. 177–206.Google Scholar
Zhu, D. & Xi, H. (2005) Safe programming with pointers through stateful views. In Proceedings of the 7th International Symposium on Practical Aspects of Declarative Languages, PADL 2005 (Long Beach, CA, January 2005), Hermenegildo, M. & Cabeza, D. (eds). Lecture Notes in Computer Science, vol. 3350. Springer, pp. 83–97.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.