Complexity bounds for container functors and comonads. (English) Zbl 1394.68240
Summary: M. Abbott et al.’s notion of containers [Lect. Notes Comput. Sci. 2620, 23–38 (2003; Zbl 1029.68096); Theor. Comput. Sci. 342, No. 1, 3–27 (2005; Zbl 1077.68015)] characterises a subset of parametric data types which can be described by a set of shapes and set of positions for each shape. This captures common data types such as tuples, lists, trees, arrays, and graphs. Various useful categorical structures can be derived for containers given additional information. For example, directed containers give rise to container comonads [D. Ahman et al., Lect. Notes Comput. Sci. 7213, 74–88 (2012; Zbl 1338.68171); Log. Methods Comput. Sci. 10, No. 3, Paper No. 14, 48 p. (2014; Zbl 1338.68172)]. Containers provide a useful reasoning principle and abstraction mechanism for programming. This paper studies the performance characteristics of traversal schemes over containers, modelled by functor and comonad structures. A cost model for container transformations is defined from which complexity bounds for the operations of container functors and comonads are derived. These bounds suggest optimisations for programs structured using these idioms. The abstract interface provided by the syntax of containers and category theory provides complexity bounds and subsequent optimisations that are implementation agnostic (machine free).
MSC:
| 68Q65 | Abstract data types; algebraic specification |
| 68N30 | Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) |
Software:
GHCReferences:
| [1] | Abbott, M.; Altenkirch, T.; Ghani, N., Categories of containers, (Foundations of Software Science and Computation Structures, (2003), Springer), 23-38 · Zbl 1029.68096 |
| [2] | Abbott, M.; Altenkirch, T.; Ghani, N., Containers: constructing strictly positive types, Theor. Comput. Sci., 342, 1, 3-27, (2005) · Zbl 1077.68015 |
| [3] | Ahman, D.; Chapman, J.; Uustalu, T., When is a container a comonad?, (Foundations of Software Science and Computational Structures, (2012)), 74-88 · Zbl 1338.68171 |
| [4] | Ahman, D.; Chapman, J.; Uustalu, T., When is a container a comonad?, Log. Methods Comput. Sci., 10, 3, (2014), (extended version) · Zbl 1338.68172 |
| [5] | Cockett, R.; Díaz-Boïls, J.; Gallagher, J.; Hrubeš, P., Timed sets, functional complexity, and computability, Electron. Notes Theor. Comput. Sci., 286, 117-137, (2012) · Zbl 1342.68127 |
| [6] | Dal Lago, U.; Martini, S., An invariant cost model for the lambda calculus, (Logical Approaches to Computational Barriers, (2006), Springer), 105-114 · Zbl 1145.68375 |
| [7] | Foner, Kenneth, Functional pearl: getting a quick fix on comonads, (ACM SIGPLAN Not., vol. 50, (2015), ACM), 106-117 |
| [8] | Girard, J.-Y., Normal functors, power series and λ-calculus, Ann. Pure Appl. Log., 37, 2, 129-177, (1988) · Zbl 0646.03056 |
| [9] | Havel, J.; Herout, A., Rendering pipeline modelled by category theory, (GraVisMa 2010 Workshop Proceedings, (2010), University of West Bohemia in Pilsen), 101-105 |
| [10] | Hayashi, Y., Shape-based cost analysis of skeletal parallel programs, (2001) |
| [11] | Hinze, R., Kan extensions for program optimisation or: art and dan explain an old trick, (Mathematics of Program Construction, (2012), Springer), 324-362 · Zbl 1358.68057 |
| [12] | Jay, C. Barry, A semantics for shape, Sci. Comput. Program., 25, 2, 251-283, (1995) · Zbl 0853.68119 |
| [13] | Jay, C. Barry, Costing parallel programs as a function of shapes, Sci. Comput. Program., 37, 1, 207-224, (2000) · Zbl 0954.68043 |
| [14] | Jay, C. Barry; Cockett, J. Robin B., Shapely types and shape polymorphism, (Programming Languages and Systems - ESOP’94, (1994), Springer), 302-316 |
| [15] | Lechtchinsky, R.; Chakravarty, M.; Keller, G., Costing nested array codes, Parallel Process. Lett., 12, 02, 249-266, (2002) |
| [16] | Orchard, D., Programming contextual computations, (2014), University of Cambridge, PhD dissertation |
| [17] | Orchard, D.; Bolingbroke, M.; Mycroft, A., Ypnos: declarative, parallel structured grid programming, (DAMP ’10: Proceedings of the 5th ACM SIGPLAN Workshop on Declarative Aspects of Multicore Programming, (2010), ACM New York, NY, USA), 15-24 |
| [18] | Orchard, D.; Mycroft, A., A notation for comonads, (IFL ’12: Implementation and Application of Functional Languages, Revised Selected Papers, vol. 8241, (2012)) |
| [19] | Peyton Jones, S.; Tolmach, A.; Hoare, T., Playing by the rules: rewriting as a practical optimisation technique in GHC, (Haskell Workshop, vol. 1, (2001)), 203-233 |
| [20] | Riely, J.; Prins, J., Flattening is an improvement, (Static Analysis, (2000), Springer), 360-376 · Zbl 0966.68506 |
| [21] | Skillicorn, D., Models for practical parallel computation, Int. J. Parallel Program., 20, 2, 133-158, (1991) |
| [22] | Skillicorn, D.; Cai, W., A cost calculus for parallel functional programming, J. Parallel Distrib. Comput., 28, 1, 65-83, (1995) · Zbl 0833.68021 |
| [23] | Uustalu, T.; Vene, V., Comonadic notions of computation, Electron. Notes Theor. Comput. Sci., 203, 5, 263-284, (2008) · Zbl 1279.68088 |
| [24] | Uustalu, Tarmo, Container combinatorics: monads and Lax monoidal functors, (International Conference on Topics in Theoretical Computer Science, (2017), Springer), 91-105 · Zbl 1485.18004 |
| [25] | Voigtländer, J., Asymptotic improvement of computations over free monads, (Mathematics of Program Construction, (2008), Springer), 388-403 · Zbl 1156.68363 |
| [26] | Wadler, P., Strictness analysis aids time analysis, (Proceedings of the 15th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, (1988), ACM), 119-132 |
| [27] | Wadler, P., Deforestation: transforming programs to eliminate trees, Theor. Comput. Sci., 73, 2, 231-248, (1990) · Zbl 0701.68013 |
| [28] | Yanofsky, N. S., Towards a definition of an algorithm, J. Log. Comput., 21, 2, 253-286, (2011) · Zbl 1214.68459 |
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.
