Dragging proofs out of pictures. (English) Zbl 1343.18007
Lindley, Sam (ed.) et al., A list of successes that can change the world. Essays dedicated to Philip Wadler on the occasion of his 60th birthday. Cham: Springer (ISBN 978-3-319-30935-4/pbk; 978-3-319-30936-1/ebook). Lecture Notes in Computer Science 9600, 152-168 (2016).
Summary: String diagrams provide category theory with a different and very distinctive visual flavour. We demonstrate that they are an effective tool for equational reasoning using a variety of examples evolving around the composition of monads. A deductive approach is followed, discovering necessary concepts as we go along. In particular, we show that the Yang-Baxter equation arises naturally when composing three monads. We are also concerned with the pragmatics of string diagrams. Diagrams are carefully arranged to provide geometric intution for the proof steps being followed. We introduce thick wires to distinguish composite functors and suggest a two-dimensional analogue of parenthesis to partition diagrams.
For the entire collection see [Zbl 1333.68014].
For the entire collection see [Zbl 1333.68014].
MSC:
| 18C15 | Monads (= standard construction, triple or triad), algebras for monads, homology and derived functors for monads |
| 18A10 | Graphs, diagram schemes, precategories |
| 18A15 | Foundations, relations to logic and deductive systems |
| 18D10 | Monoidal, symmetric monoidal and braided categories (MSC2010) |
References:
| [1] | Beck, J.: Distributive laws. In: Appelgate, H., et al. (eds.) Seminar on Triples and Categorical Homotopy Theory. Lecture Notes in Mathematics, vol. 80, pp. 119–140. Springer, Heidelberg (1969) · doi:10.1007/BFb0083084 |
| [2] | Cheng, E.: Iterated distributive laws. ArXiv e-prints, October 2007 |
| [3] | Hinze, R., Marsden, D.: Equational reasoning with lollipops, forks, cups, caps, snakes, and speedometers. José Oliveira Festschrift (2015, to appear) · Zbl 1375.18027 |
| [4] | Joyal, A., Street, R.: Geometry of tensor calculus I. Adv. Math. 88, 55–113 (1991) · Zbl 0738.18005 · doi:10.1016/0001-8708(91)90003-P |
| [5] | King, D.J., Wadler, P.: Combining monads. In: Launchbury, J., Sansom, P. (eds.) Proceedings of the 1992 Glasgow Workshop on Functional Programming. Workshops in Computing, pp. 134–143. Springer, Berlin/Heidelberg (1993) · doi:10.1007/978-1-4471-3215-8_12 |
| [6] | Knuth, D.E.: The Art of Computer Programming. Sorting and Searching, vol. 3, 2nd edn. Addison-Wesley Publishing Company, Reading (1998) · Zbl 0302.68010 |
| [7] | Manes, E.G.: Algebraic Theories. Springer, Heidelberg (1976) · Zbl 0353.18007 · doi:10.1007/978-1-4612-9860-1 |
| [8] | Marsden, D.: Category theory using string diagrams (2014). arXiv preprint arXiv:1401.7220 |
| [9] | Penrose, R.: Applications of negative dimensional tensors. In: Welsh, D.J.A. (ed.) Combinatorial Mathematics and its Applications, pp. 221–244. Academic Press, New York (1971) · Zbl 0216.43502 |
| [10] | Peyton Jones, S.L., Wadler, P.: Imperative functional programming. In: Proceedings of the 20th Annual ACM Symposium on Principles of Programming Languages, pp. 71–84, Charleston, South Carolina, January 1993 · doi:10.1145/158511.158524 |
| [11] | Wadler, P.: Comprehending monads. In: Proceedings of the 1990 ACM Conference on LISP and Functional Programming, Nice, pp. 61–78. ACM Press, June 1990 · Zbl 0798.68040 · doi:10.1145/91556.91592 |
| [12] | Wadler, P.: The essence of functional programming. In: Proceedings of the 19th Annual ACM Symposium on Principles of Programming Languages, Sante Fe, New Mexico, pp. 1–14, January 1992 · doi:10.1145/143165.143169 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
