Document

# How to Take the Inverse of a Type

## File

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

## 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

Daniel 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

## 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.
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.
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.
7. Richard Bird and Oege de Moor. Algebra of Programming. Prentice-Hall, Inc., USA, 1997.
8. Richard S. Bird. Algebraic identities for program calculation. The Computer Journal, 32(2):122-126, 1989.
9. Andreas Blass. Seven trees in one. Journal of Pure and Applied Algebra, 103(1):1-21, 1995.
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.
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.
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.
21. Dana Harrington. Uniqueness logic. Theoretical Computer Science, 354(1):24-41, 2006.
22. Gérard Huet. The zipper. Journal of Functional Programming, 7(5):549-554, 1997.
23. Jack Hughes, Michael Vollmer, and Dominic Orchard. Deriving distributive laws for graded linear types. In TLLA/Linearity, 2020.
24. Roshan P James and Amr Sabry. The Two Dualities of Computation: Negative and Fractional Types. Technical report, Indiana University, 2012.
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.
26. G Maxwell Kelly. Coherence theorems for lax algebras and for distributive laws. In Category seminar, pages 281-375. Springer, 1974.
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.
28. Serge Lang. Algebra. Springer, New York, NY, 2002.
29. Gottfried Wilhelm Leibniz. Nova methodus pro maximis et minimis, itemque tangentibus, qua nec irrationals quantitates moratur. Acta eruditorum, 1684.
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.
31. Sam Lindley and J Garrett Morris. Lightweight functional session types. Behavioural Types: from Theory to Tools. River Publishers, pages 265-286, 2017.
32. John Longley. When is a functional program not a functional program? In ACM SIGPLAN Notices, volume 34(9), pages 1-7. ACM, 1999.
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.
35. Daniel 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. Daniel 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.
37. Conor McBride. The derivative of a regular type is its type of one-hole contexts. Unpublished manuscript, pages 74-88, 2001.
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.
41. Dominic Orchard. Programming contextual computations. Technical report, University of Cambridge, Computer Laboratory, 2014.
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.
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.
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.
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.
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.
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.
51. Philip Wadler. Linear types can change the world! In Programming Concepts and Methods, volume 3(4), page 5. Citeseer, 1990.
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.
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.
54. Philip Wadler. Propositions as sessions. Journal of Functional Programming, 24(2-3):384-418, 2014.
55. David Walker. Substructural type systems. Advanced Topics in Types and Programming Languages, pages 3-44, 2005.
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.
X

Feedback for Dagstuhl Publishing