skip to main content
research-article

Universal properties of impure programming languages

Published: 23 January 2013 Publication History

Abstract

We investigate impure, call-by-value programming languages. Our first language only has variables and let-binding. Its equational theory is a variant of Lambek's theory of multicategories that omits the commutativity axiom.
We demonstrate that type constructions for impure languages --- products, sums and functions --- can be characterized by universal properties in the setting of 'premulticategories', multicategories where the commutativity law may fail. This leads us to new, universal characterizations of two earlier equational theories of impure programming languages: the premonoidal categories of Power and Robinson, and the monad-based models of Moggi. Our analysis thus puts these earlier abstract ideas on a canonical foundation, bringing them to a new, syntactic level.

References

[1]
M. Abadi, L. Cardelli, P.-L. Curien, and J.-J. Levy. Explicit substitutions. J. Funct. Program., 1(4):375--416, 1991.
[2]
T. Altenkirch, J. Chapman, and T. Uustalu. Monads need not be endofunctors. In FOSSACS'10, pages 297--311, 2010.
[3]
R. Atkey. What is a categorical model of arrows? In Proc. MSFP'08, pages 19--37, 2011.
[4]
P. N. Benton and P. Wadler. Linear logic, monads and the lambda calculus. In Proc. LICS'96, pages 420--431, 1996.
[5]
A. Burroni. T-categories (categories dans un triple). Cahiers Topologie Geom. Differentielle, 12(3):215--312, 1971.
[6]
A. Burroni. Higher dimensional word problem. In Proc. CTCS'91, pages 94--105, 1991.
[7]
P.-L. Curien. Operads, clones, and distributive laws. In Operads and Universal Algebra, 2010.
[8]
J. Egger, R. E. Møgelberg, and A. Simpson. Enriching an effect calculus with linear types. In Proc. CSL'09, pages 240--254, 2009.
[9]
M. P. Fiore. Semantic analysis of normalisation by evaluation for typed lambda calculus. In Proc. PPDP'02, pages 26--37, 2002.
[10]
C. Flanagan, A. Sabry, B. F. Duba, and M. Felleisen. The essence of compiling with continuations. In Proc. PLDI'93, pages 237--247, 1993.
[11]
F. Foltz, C. Lair, and G. M. Kelly. Algebraic categories with few monoidal biclosed structures or none. J. Pure and Applied Algebra, 17:171--177, 1980.
[12]
C. Führmann. Direct models of the computational lambda-calculus. In Proc. MFPS XV, pages 147--172, 1999.
[13]
H. Herbelin. A lambda-calculus structure isomorphic to Gentzen-style sequent calculus structure. In Proc. CSL'94, pages 61--75, 1994.
[14]
C. Hermida. Representable multicategories. Advances in Mathematics, 151:164--225, 2000.
[15]
M. Hyland. Multicategories in and around algebra and logic. Invited talk, TACL'09. Slides available from the author's home page, 2009.
[16]
B. Jacobs. Semantics of weakening and contraction. Annals of Pure and Applied Logic, 69(1):73--106, 1994.
[17]
B. Jacobs and I. Hasuo. Freyd is Kleisli, for arrows. In Proc. MSFP'06, 2006.
[18]
A. Jeffrey. Premonoidal categories and a graphical view of programs. Unpublished, 1997.
[19]
A. Kock. Monads on symmetric monoidal closed categories. Archiv der Math., 21:1--10, 1970.
[20]
Y. Lafont. Towards an algebraic theory of Boolean circuits. J. Pure Appl. Algebra, 184(2-3):257--310, 2003.
[21]
J. Lambek. Deductive systems and categories II. In Category theory, homology theory and their applications, volume 86 of LNM, pages 76--122. Springer, 1969.
[22]
T. Leinster. Higher operads, higher categories. CUP, 2004.
[23]
P. B. Levy. Call-by-push-value. Springer, 2004.
[24]
P. B. Levy, J. Power, and H. Thielecke. Modelling environments in call-by-value programming languages. Inform. Comput., 2003.
[25]
F. Linton. Autonomous equational categories. Indiana Univ. Math. J., 15:637--642, 1966.
[26]
G. McCusker. A fully abstract relational model of syntactic control of interference. In Proc. CSL'02, pages 247--261, 2002.
[27]
P. Melli`es and N. Tabareau. Linear continuations and duality. hal.archives-ouvertes.fr/hal-00339156, 2008.
[28]
R. E. Møgelberg and S. Staton. Linearly-used state in models of callby-value. In CALCO'11, pages 298--313, 2011.
[29]
E. Moggi. Computational lambda-calculus and monads. In LICS'89, pages 14--23, 1989.
[30]
E. Moggi. Notions of computation and monads. Inform. Comput., 93 (1), 1991.
[31]
P. W. O'Hearn. On bunched typing. J. Funct. Program., 13(4):747--796, 2003.
[32]
J. Power. Premonoidal categories as categories with algebraic structure. Theor. Comput. Sci., 278(1-2):303--321, 2002.
[33]
J. Power and E. Robinson. Premonoidal categories and notions of computation. Math. Struct. Comput. Sci., 7(5):453--468, 1997.
[34]
J. Power and H. Thielecke. Closed Freyd- and kappa-categories. In Proc. ICALP'99, 1999.
[35]
U. S. Reddy. Global state considered unnecessary: An introduction to object-based semantics. Lisp and Symbolic Computation, 9(1):7--76, 1996.
[36]
J. G. Stell. Modelling term rewriting systems by sesqui-categories. Technical Report TR94-02, Keele University, 1994.

Cited By

View all
  • (2025)The Univalence PrincipleMemoirs of the American Mathematical Society10.1090/memo/1541305:1541Online publication date: 14-Jan-2025
  • (2023)Optics for Premonoidal CategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.10397(152-171)Online publication date: 14-Dec-2023
  • (2023)A skew approach to enrichment for Gray-categoriesAdvances in Mathematics10.1016/j.aim.2023.109327434(109327)Online publication date: Dec-2023
  • Show More Cited By

Recommendations

Comments

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices
ACM SIGPLAN Notices  Volume 48, Issue 1
POPL '13
January 2013
561 pages
ISSN:0362-1340
EISSN:1558-1160
DOI:10.1145/2480359
Issue’s Table of Contents
  • cover image ACM Conferences
    POPL '13: Proceedings of the 40th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages
    January 2013
    586 pages
    ISBN:9781450318327
    DOI:10.1145/2429069
Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 23 January 2013
Published in SIGPLAN Volume 48, Issue 1

Check for updates

Author Tags

  1. multicamonads
  2. multicategories
  3. premonoidal categories

Qualifiers

  • Research-article

Contributors

Other Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

  • Downloads (Last 12 months)23
  • Downloads (Last 6 weeks)7
Reflects downloads up to 19 Feb 2025

Other Metrics

Citations

Cited By

View all
  • (2025)The Univalence PrincipleMemoirs of the American Mathematical Society10.1090/memo/1541305:1541Online publication date: 14-Jan-2025
  • (2023)Optics for Premonoidal CategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.10397(152-171)Online publication date: 14-Dec-2023
  • (2023)A skew approach to enrichment for Gray-categoriesAdvances in Mathematics10.1016/j.aim.2023.109327434(109327)Online publication date: Dec-2023
  • (2021)Compositional semantics for probabilistic programs with exact conditioningProceedings of the 36th Annual ACM/IEEE Symposium on Logic in Computer Science10.1109/LICS52264.2021.9470552(1-13)Online publication date: 29-Jun-2021
  • (2015)A short introduction to the coalgebraic methodACM SIGLOG News10.1145/2766189.27661932:2(16-27)Online publication date: 22-Apr-2015
  • (2023)Collages of String DiagramsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.397.3397(39-53)Online publication date: 14-Dec-2023
  • (2023)Universal Properties of Partial Quantum MapsElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.394.11394(192-207)Online publication date: 16-Nov-2023
  • (2023)Promonads and String Diagrams for Effectful CategoriesElectronic Proceedings in Theoretical Computer Science10.4204/EPTCS.380.20380(344-361)Online publication date: 7-Aug-2023
  • (2023)Central Submonads and Notions of Computation: Soundness, Completeness and Internal Languages2023 38th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS56636.2023.10175687(1-13)Online publication date: 26-Jun-2023
  • (2021)Compositional Semantics for Probabilistic Programs with Exact Conditioning2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)10.1109/LICS52264.2021.9470552(1-13)Online publication date: 29-Jun-2021
  • Show More Cited By

View Options

Login options

View options

PDF

View or Download as a PDF file.

PDF

eReader

View online with eReader.

eReader

Figures

Tables

Media

Share

Share

Share this Publication link

Share on social media