Hostname: page-component-78c5997874-dh8gc Total loading time: 0 Render date: 2024-11-03T00:36:38.687Z Has data issue: false hasContentIssue false
  • English
  • Français

A representation theorem for second-order functionals

Part of: JFP Research Articles

Published online by Cambridge University Press:  08 September 2015

MAURO JASKELIOFF  and
RUSSELL O'CONNOR
MAURO JASKELIOFF
Affiliation:
CIFASIS, CONICET, Argentina, FCEIA, Universidad Nacional de Rosario, Argentina (e-mail: [email protected])
RUSSELL O'CONNOR
Affiliation:
Google Canada, Kitchener, Ontario, Canada (e-mail: [email protected])
Rights & Permissions [Opens in a new window]

Abstract

Core share and HTML view are not available for this content. However, as you have access to this content, a full PDF is available via the ‘Save PDF’ action button.

Representation theorems relate seemingly complex objects to concrete, more tractable ones. In this paper, we take advantage of the abstraction power of category theory and provide a datatype-generic representation theorem. More precisely, we prove a representation theorem for a wide class of second-order functionals which are polymorphic over a class of functors. Types polymorphic over a class of functors are easily representable in languages such as Haskell, but are difficult to analyse and reason about. The concrete representation provided by the theorem is easier to analyse, but it might not be as convenient to implement. Therefore, depending on the task at hand, the change of representation may prove valuable in one direction or the other. We showcase the usefulness of the representation theorem with a range of examples. Concretely, we show how the representation theorem can be used to prove that traversable functors are finitary containers, how coalgebras of a parameterised store comonad relate to very well-behaved lenses, and how algebraic effects might be implemented in a functional language.

Type
Articles
Information
Journal of Functional Programming , Volume 25 , 2015 , e13
Creative Commons
Creative Common License - CCCreative Common License - BYCreative Common License - NCCreative Common License - SA
This is an Open Access article, distributed under the terms of the Creative Commons Attribution licence (http://creativecommons.org/licenses/by/3.0/), which permits unrestricted re-use, distribution, and reproduction in any medium, provided the original work is properly cited.
Copyright
Copyright © Cambridge University Press 2015

References

Abbott, M., Altenkirch, T. & Ghani, N. (2003) Categories of containers. In Proceedings of Foundation s of Software Science and Computation Structures. pp. 23–38.CrossRefGoogle Scholar
Atkey, R. (2009a) Algebras for parameterised monads. In Proceedings of the Algebra and Coalgebra in Computer Science, 3rd International Conference, CALCO 2009, Udine, Italy (September 7–10, 2009), Kurz, A., Lenisa, M. & Tarlecki, A. (eds), vol. 5728. Lecture Notes in Computer Science, Springer, pp. 3–17.Google Scholar
Atkey, R. (2009b) Parameterised notions of computation. J. Funct. Program. 19 (3 & 4), 335–376.CrossRefGoogle Scholar
Awodey, S. (2006) Category Theory. USA: Oxford University Press.CrossRefGoogle Scholar
Bainbridge, E. S., Freyd, P. J., Scedrov, A. & Scott, P. J. (1990) Functorial polymorphism. Theor. Comput. Sci. 70 (1), 35–64.CrossRefGoogle Scholar
Bauer, A., Hofmann, M. & Karbyshev, A. (2013) On monadic parametricity of second-order functionals. In Foundations of Software Science and Computation Structures, Pfenning, F. (ed), vol. 7794. Lecture Notes in Computer Science, . Berlin Heidelberg: Springer, pp. 225–240.CrossRefGoogle Scholar
Bernardy, J.-P., Jansson, P. & Claessen, K. (2010) Testing polymorphic properties. In Programming Languages and Systems, Gordon, A. D. (ed), vol. 6012. Lecture Notes in Computer Science. Berlin Heidelberg: Springer, pp. 125–144.CrossRefGoogle Scholar
Bird, R. & de Moor, O. (1997) Algebra of Programming. Upper Saddle River, NJ, USA: Prentice-Hall.Google Scholar
Bird, R., Gibbons, J., Mehner, S., Voigtländer, J. & Schrijvers, T. (2013) Understanding idiomatic traversals backwards and forwards. In Proceedings of the 2013 ACM SIGPLAN Symposium on Haskell. Haskell '13. New York, NY, USA: ACM, pp. 25–36.CrossRefGoogle Scholar
Capriotti, P. & Kaposi, A. 2014 (April) Free applicative functors. In Proceedings of the 5th Workshop on Mathematically Structured Functional Programming. MSFP '14, pp. 2–30.Google Scholar
Danielsson, N. A., Hughes, J., Jansson, P. & Gibbons, J. (2006) Fast and loose reasoning is morally correct. Sigplan Not. 41 (1), 206–217.CrossRefGoogle Scholar
Foster, J. N., Greenwald, M. B., Moore, J. T., Pierce, B. C. & Schmitt, A. (2007) Combinators for bidirectional tree transformations: A linguistic approach to the view-update problem. ACM Trans. Program. Lang. Syst. 29 (3). (Article 17).CrossRefGoogle Scholar
Gibbons, J. & Johnson, M. (2012) Relating algebraic and coalgebraic descriptions of lenses. 49 (Bidirectional Transformations 2012). Berlin, Germany.Google Scholar
Gibbons, J. & Oliveira, B. C. D. S. (2009) The essence of the iterator pattern. J. Funct. Program., 19, 377–402.CrossRefGoogle Scholar
Jaskelioff, M. & Rypacek, O. (2012) An investigation of the laws of traversals. In Proceedings of the 4th Workshop on Mathematically Structured Functional Programming. EPTCS, Chapman, J. & Levy, P. B. (eds), vol. 76, pp. 40–49.CrossRefGoogle Scholar
Kmett, E. 2013 (October) Lens-4.0: Lenses, Folds and Traversals. Available at: http://ekmett.github.io/lens/Control-Lens-Traversal.html.Google Scholar
Mac Lane, S. (1971) Categories for the Working Mathematician. Graduate Texts in Mathematics, no. 5, 2nd ed., Springer-Verlag, 1998.CrossRefGoogle Scholar
McBride, C. & Paterson, R. (2008) Applicative programming with effects. J. Funct. Program. 18 (01), 1–13.CrossRefGoogle Scholar
Milewski, B. 2013 (October) Lenses, Stores, and Yoneda. Available at: http://bartoszmilewski.com/2013/10/08/lenses-stores-and-yoneda.Google Scholar
Moggi, E., Bellè, G. & Jay, C. B. (1999) Monads, shapely functors and traversals. Electron. Notes Theor. Comput. Sci. 29, 187–208.CrossRefGoogle Scholar
O'Connor, R. 2010 (Nov.) Lenses are Exactly the Coalgebras for the Store Comonad. Available at: http://r6research.livejournal.com/23705.html.Google Scholar
O'Connor, R. (2011) Functor is to lens as applicative is to biplate: Introducing multiplate. Corr, abs/1103.2841v1.Google Scholar
O'Connor, R., Kmett, E. A. & Morris, T. 2013 (October) Data-lens-2.10.4: Haskell 98 lenses. Available at: http://hackage.haskell.org/package/data-lens-2.10.4/docs/Data-Lens-Partial-Common.html.Google Scholar
Plotkin, G. & Power, J. (2003) Algebraic operations and generic effects. Appl. Categ. Struct. 11 (1), 69–94.CrossRefGoogle Scholar
Plotkin, G. & Pretnar, M. (2009) Handlers of algebraic effects. In Programming Languages and Systems, Castagna, G. (ed), vol. 5502. Lecture Notes in Computer Science, . Berlin Heidelberg: Springer.Google Scholar
Reynolds, J. C. & Plotkin, G. D. (1993) On functors expressible in the polymorphic typed lambda calculus. Inform. Comput. 105 (1), 1–29.CrossRefGoogle Scholar
Swierstra, W. (2008) Data types à la carte. J. Funct. Program. 18 (4), 423–436.CrossRefGoogle Scholar
Van Laarhoven, T. 2009a (Aug.) CPS Based Functional References. Available at: http://twanvl.nl/blog/haskell/cps-functional-references.Google Scholar
Van Laarhoven, T. 2009b (Apr.) A Non-Regular Data Type Challenge. Available at: http://twanvl.nl/blog/haskell/non-regular1.Google Scholar
Van Laarhoven, T. 2009c (Apr.) Where Do I Get My Non-Regular Types? Available at: http://twanvl.nl/blog/haskell/non-regular2.Google Scholar
Submit a response

Discussions

No Discussions have been published for this article.