Document Open Access Logo

How to Take the Inverse of a Type

Authors Danielle Marshall , Dominic Orchard

PDF
Thumbnail PDF

File

LIPIcs.ECOOP.2022.5.pdf
  • Filesize: 1.09 MB
  • 27 pages

Document Identifiers

Author Details

Danielle Marshall
  • School of Computing, University of Kent, Canterbury, UK
Dominic Orchard
  • School of Computing, University of Kent, Canterbury, UK
  • Department of Computer Science and Technology, University of Cambridge, UK

Funding

This work is supported by an EPSRC Doctoral Training Award (Marshall) and EPSRC grant EP/T013516/1 (Verifying Resource-like Data Use in Programs via Types).

Acknowledgements

Thanks to Nicolas Wu and Harley Eades III for their valuable comments and discussion on earlier drafts, and also to the anonymous reviewers for their helpful feedback.

Cite As Get BibTex

Danielle Marshall and Dominic Orchard. How to Take the Inverse of a Type. In 36th European Conference on Object-Oriented Programming (ECOOP 2022). Leibniz International Proceedings in Informatics (LIPIcs), Volume 222, pp. 5:1-5:27, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2022) https://doi.org/10.4230/LIPIcs.ECOOP.2022.5

Abstract

In functional programming, regular types are a subset of algebraic data types formed from products and sums with their respective units. One can view regular types as forming a commutative semiring but where the usual axioms are isomorphisms rather than equalities. In this pearl, we show that regular types in a linear setting permit a useful notion of multiplicative inverse, allowing us to "divide" one type by another. Our adventure begins with an exploration of the properties and applications of this construction, visiting various topics from the literature including program calculation, Laurent polynomials, and derivatives of data types. Examples are given throughout using Haskell’s linear types extension to demonstrate the ideas. We then step through the looking glass to discover what might be possible in richer settings; the functional language Granule offers linear functions that incorporate local side effects, which allow us to demonstrate further algebraic structure. Lastly, we discuss whether dualities in linear logic might permit the related notion of an additive inverse.

Subject Classification

ACM Subject Classification
  • Theory of computation → Type theory
Keywords
  • linear types
  • regular types
  • algebra of programming
  • derivatives

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Supplementary Materials

References

  1. Michael Abbott, Thorsten Altenkirch, Conor Mcbride, and Neil Ghani. ∂ for data: Differentiating data structures. Fundam. Inf., 65(1–2):1-28, January 2005. Google Scholar
  2. Niels Henrik Abel. Mémoire sur les equations algébriques, où l'on démontre l'impossibilité de la résolution de l'équation générale du cinquième degré. 1:28-33, 1824. URL: https://doi.org/10.1017/CBO9781139245807.004.
  3. Bernardo Almeida, Andreia Mordido, Peter Thiemann, and Vasco T. Vasconcelos. Polymorphic context-free session types, 2021. URL: http://arxiv.org/abs/2106.06658.
  4. Federico Aschieri and Francesco A. Genco. Par means parallel: Multiplicative linear logic proofs as concurrent functional programs. Proc. ACM Program. Lang., 4(POPL), December 2019. URL: https://doi.org/10.1145/3371086.
  5. Gianluigi Bellin, Massimiliano Carrara, Daniele Chiffi, and Alessandro Menti. Pragmatic and dialogic interpretations of bi-intuitionism. Part I. Logic and Logical Philosophy, 23(4):449-480, 2014. Google Scholar
  6. Jean-Philippe Bernardy, Mathieu Boespflug, Ryan R Newton, Simon Peyton Jones, and Arnaud Spiwack. Linear Haskell: practical linearity in a higher-order polymorphic language. Proceedings of the ACM on Programming Languages, 2(POPL):1-29, 2017. Google Scholar
  7. Richard Bird and Oege de Moor. Algebra of Programming. Prentice-Hall, Inc., USA, 1997. Google Scholar
  8. Richard S. Bird. Algebraic identities for program calculation. The Computer Journal, 32(2):122-126, 1989. Google Scholar
  9. Andreas Blass. Seven trees in one. Journal of Pure and Applied Algebra, 103(1):1-21, 1995. Google Scholar
  10. Edwin Brady. Idris 2: Quantitative Type Theory in Practice. In Anders Møller and Manu Sridharan, editors, 35th European Conference on Object-Oriented Programming (ECOOP 2021), volume 194 of Leibniz International Proceedings in Informatics (LIPIcs), pages 9:1-9:26, Dagstuhl, Germany, 2021. Schloss Dagstuhl - Leibniz-Zentrum für Informatik. URL: https://doi.org/10.4230/LIPIcs.ECOOP.2021.9.
  11. Jacques Carette and Amr Sabry. Computing with semirings and weak rig groupoids. In Proceedings of the 25th European Symposium on Programming Languages and Systems - Volume 9632, pages 123-148, Berlin, Heidelberg, 2016. Springer-Verlag. Google Scholar
  12. Chao-Hong Chen and Amr Sabry. A computational interpretation of compact closed categories: Reversible programming with negative and fractional types. Proc. ACM Program. Lang., 5(POPL), January 2021. URL: https://doi.org/10.1145/3434290.
  13. J.R.B. Cockett and R.A.G. Seely. Weakly distributive categories. Journal of Pure and Applied Algebra, 114(2):133-173, 1997. URL: https://doi.org/10.1016/0022-4049(95)00160-3.
  14. Edsko de Vries, Rinus Plasmeijer, and David M Abrahamson. Uniqueness typing simplified. In Symposium on Implementation and Application of Functional Languages, pages 201-218. Springer, 2007. URL: https://doi.org/10.1007/978-3-540-85373-2_12.
  15. Harley Eades III and Gianluigi Bellin. A cointuitionistic adjoint logic, 2017. URL: http://arxiv.org/abs/1708.05896.
  16. Marcelo Fiore and Tom Leinster. Objects of categories as complex numbers. Advances in Mathematics, 190(2):264-277, 2005. URL: https://doi.org/10.1016/j.aim.2004.01.002.
  17. Simon J. Gay and Vasco Thudichum Vasconcelos. Linear type theory for asynchronous session types. J. Funct. Program., 20(1):19-50, 2010. URL: https://doi.org/10.1017/S0956796809990268.
  18. Jeremy Gibbons. Calculating functional programs. In Algebraic and Coalgebraic Methods in the Mathematics of Program Construction, pages 151-203. Springer, 2002. Google Scholar
  19. Jeremy Gibbons. The school of Squiggol - A history of the Bird-Meertens formalism. In Formal Methods. FM 2019 International Workshops - Porto, Portugal, October 7-11, 2019, Revised Selected Papers, Part II, pages 35-53, 2019. URL: https://doi.org/10.1007/978-3-030-54997-8_2.
  20. Jean-Yves Girard. Linear logic. Theoretical Computer Science, 50(1):1-101, 1987. Google Scholar
  21. Dana Harrington. Uniqueness logic. Theoretical Computer Science, 354(1):24-41, 2006. Google Scholar
  22. Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549-554, 1997. Google Scholar
  23. Jack Hughes, Michael Vollmer, and Dominic Orchard. Deriving distributive laws for graded linear types. In TLLA/Linearity, 2020. Google Scholar
  24. Roshan P James and Amr Sabry. The Two Dualities of Computation: Negative and Fractional Types. Technical report, Indiana University, 2012. Google Scholar
  25. Shoaib Kamil, Kaushik Datta, Samuel Williams, Leonid Oliker, John Shalf, and Katherine Yelick. Implicit and explicit optimizations for stencil computations. In Proceedings of the 2006 Workshop on Memory System Performance and Correctness, pages 51-60, 2006. Google Scholar
  26. G Maxwell Kelly. Coherence theorems for lax algebras and for distributive laws. In Category seminar, pages 281-375. Springer, 1974. Google Scholar
  27. Wen Kokke and Ornela Dardha. Deadlock-free session types in linear Haskell. In Proceedings of the 14th ACM SIGPLAN International Symposium on Haskell, pages 1-13, 2021. Google Scholar
  28. Serge Lang. Algebra. Springer, New York, NY, 2002. Google Scholar
  29. Gottfried Wilhelm Leibniz. Nova methodus pro maximis et minimis, itemque tangentibus, qua nec irrationals quantitates moratur. Acta eruditorum, 1684. Google Scholar
  30. Sam Lindley and J Garrett Morris. A semantics for propositions as sessions. In European Symposium on Programming Languages and Systems, pages 560-584. Springer, 2015. Google Scholar
  31. Sam Lindley and J Garrett Morris. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers, pages 265-286, 2017. Google Scholar
  32. John Longley. When is a functional program not a functional program? In ACM SIGPLAN Notices, volume 34(9), pages 1-7. ACM, 1999. Google Scholar
  33. John Longley. The sequentially realizable functionals. Ann. Pure Appl. Log., 117(1-3):1-93, 2002. URL: https://doi.org/10.1016/S0168-0072(01)00110-5.
  34. Saunders Mac Lane. Categories for the Working Mathematician, volume 5. Springer Science & Business Media, 2013. Google Scholar
  35. Danielle Marshall and Dominic Orchard. Replicate, reuse, repeat: Capturing non-linear communication via session types and graded modal types. Proceedings of PLACES 2022, Electronic Proceedings in Theoretical Computer Science, 356:1-11, March 2022. URL: https://doi.org/10.4204/eptcs.356.1.
  36. Danielle Marshall, Michael Vollmer, and Dominic Orchard. Linearity and Uniqueness: An Entente Cordiale. In Ilya Sergey, editor, Programming Languages and Systems, pages 346-375, Cham, 2022. Springer International Publishing. Google Scholar
  37. Conor McBride. The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript, pages 74-88, 2001. Google Scholar
  38. Conor McBride. Clowns to the left of me, jokers to the right (pearl): Dissecting data structures. SIGPLAN Not., 43(1):287-295, January 2008. URL: https://doi.org/10.1145/1328897.1328474.
  39. J. Garrett Morris. The best of both worlds: linear functional programming without compromise. In Jacques Garrigue, Gabriele Keller, and Eijiro Sumii, editors, Proceedings of the 21st ACM SIGPLAN International Conference on Functional Programming, ICFP 2016, Nara, Japan, September 18-22, 2016, pages 448-461. ACM, 2016. URL: https://doi.org/10.1145/2951913.2951925.
  40. Peter Morris, Thorsten Altenkirch, and Conor McBride. Exploring the regular tree types. In International Workshop on Types for Proofs and Programs, pages 252-267. Springer, 2004. Google Scholar
  41. Dominic Orchard. Programming contextual computations. Technical report, University of Cambridge, Computer Laboratory, 2014. Google Scholar
  42. Dominic Orchard, Vilem-Benjamin Liepelt, and Harley Eades III. Quantitative program reasoning with graded modal types. Proceedings of the ACM on Programming Languages, 3(ICFP):1-30, 2019. Google Scholar
  43. Tomas Petricek, Dominic A. Orchard, and Alan Mycroft. Coeffects: a calculus of context-dependent computation. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming, Gothenburg, Sweden, September 1-3, 2014, pages 123-135, 2014. URL: https://doi.org/10.1145/2628136.2628160.
  44. James Propp. Euler measure as generalized cardinality. arXiv: Combinatorics, 2002. Google Scholar
  45. Ben Rudiak-Gould, Alan Mycroft, and Simon Peyton Jones. Haskell is not not ML. In European Symposium on Programming, pages 38-53. Springer, 2006. Google Scholar
  46. Stephen H. Schanuel. Negative sets have Euler characteristic and dimension. In Aurelio Carboni, Maria Cristina Pedicchio, and Guiseppe Rosolini, editors, Category Theory, pages 379-385, Berlin, Heidelberg, 1991. Springer Berlin Heidelberg. Google Scholar
  47. Rui Shi and Hongwei Xi. A linear type system for multicore programming in ATS. Science of Computer Programming, 78(8):1176-1192, 2013. URL: https://doi.org/10.1016/j.scico.2012.09.005.
  48. Kornel Szlachányi. Skew-monoidal categories and bialgebroids. Advances in Mathematics, 231(3-4):1694-1730, 2012. Google Scholar
  49. Jesse A. Tov and Riccardo Pucella. Practical affine types. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2011, Austin, TX, USA, January 26-28, 2011, pages 447-458, 2011. URL: https://doi.org/10.1145/1926385.1926436.
  50. Tarmo Uustalu, Niccolò Veltri, and Noam Zeilberger. The sequent calculus of skew monoidal categories. Electronic Notes in Theoretical Computer Science, 341:345-370, 2018. Google Scholar
  51. Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, volume 3(4), page 5. Citeseer, 1990. Google Scholar
  52. Philip Wadler. The essence of functional programming. In Proceedings of the 19th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pages 1-14, 1992. Google Scholar
  53. Philip Wadler. Call-by-value is dual to call-by-name. In Proceedings of the eighth ACM SIGPLAN International Conference on Functional Programming, pages 189-201, 2003. Google Scholar
  54. Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384-418, 2014. Google Scholar
  55. David Walker. Substructural type systems. Advanced Topics in Types and Programming Languages, pages 3-44, 2005. Google Scholar
  56. Aaron Weiss, Olek Gierczak, Daniel Patterson, and Amal Ahmed. Oxide: The essence of Rust, 2021. URL: http://arxiv.org/abs/1903.00982.
  57. Nobuko Yoshida and Vasco T Vasconcelos. Language primitives and type discipline for structured communication-based programming revisited: Two systems for higher-order session communication. Electronic Notes in Theoretical Computer Science, 171(4):73-93, 2007. Google Scholar
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023-2024 Schloss Dagstuhl – LZI GmbH About DROPS Imprint Privacy Contact