Top

Published in:

2019 | OriginalPaper | Chapter

Towards Optic-Based Algebraic Theories: The Case of Lenses

Authors : J. López-González, Juan M. Serrano

Published in: Trends in Functional Programming

Publisher: Springer International Publishing

Activate our intelligent search to find suitable subject content or patents.

search-config

AI-assisted search

Off

Abstract

Optics provide rich abstractions and composition patterns to access and manipulate immutable data structures. However, the state of real applications is mostly handled through databases, caches, web services, etc. In this effectful setting, the usefulness of optics is severely limited, whereas algebraic theories, thanks to their potential to abstract away from particular infrastructures, shine. Unfortunately, there is a severe lack of standard algebraic theories, e.g. like MonadState, that programmers can reuse to avoid writing their domain repositories from scratch. This paper argues that optics can serve as a fruitful metaphor to design a rich catalogue of state-based algebraic theories, and focuses on the paradigmatic case of lenses. It shows how lenses can be generalised into an algebraic theory; how compositionality of these algebraic theories can be founded on lens composition; and how to exploit the resulting abstractions in the modular design of data layers. The paper systematically uses Coq for all its definitions and proofs.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Online-Abonnement

Mit Springer Professional "Wirtschaft+Technik" erhalten Sie Zugriff auf:

über 102.000 Bücher
über 537 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Finance + Banking
Management + Führung
Marketing + Vertrieb
Maschinenbau + Werkstoffe
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Technik"

Online-Abonnement

Mit Springer Professional "Technik" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 390 Zeitschriften

aus folgenden Fachgebieten:

Automobil + Motoren
Bauwesen + Immobilien
Business IT + Informatik
Elektrotechnik + Elektronik
Energie + Nachhaltigkeit
Maschinenbau + Werkstoffe

Jetzt Wissensvorsprung sichern!

inform now

Springer Professional "Wirtschaft"

Online-Abonnement

Mit Springer Professional "Wirtschaft" erhalten Sie Zugriff auf:

über 67.000 Bücher
über 340 Zeitschriften

aus folgenden Fachgebieten:

Bauwesen + Immobilien
Business IT + Informatik
Finance + Banking
Management + Führung
Marketing + Vertrieb
Versicherung + Risiko

Jetzt Wissensvorsprung sichern!

inform now

previous chapter Intrinsic Currying for C++ Template Metaprograms

next chapter Saint: An API-Generic Type-Safe Interpreter

Available only for authorised users

Coq will be used throughout the paper.

For the moment, we will ignore the details about lens representations.

We could also have defined accessors to update the name or departments with a new value passed as parameter, but they are not used in the upcoming examples.

We assume familiarity with monads. You can find the particular Coq encoding that we use for

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figao_HTML.gif

in the supplementary material (Sect. A).

There exists a polymorphic lens version which is more general, where

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figaz_HTML.gif

declares a different type for the part, leading to a different type for the resulting whole.

If we discard

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figbb_HTML.gif

, we can talk about well-behaved lenses.

We represent

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figcj_HTML.gif

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figck_HTML.gif

to simplify signatures.

Here, we assume that

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figef_HTML.gif

also collects a

https://static-content.springer.com/image/chp%3A10.1007%2F978-3-030-18506-0_4/MediaObjects/482829_1_En_4_Figeg_HTML.gif

evidence.

Note that this would only involve the math department in the new configuration.

https://github.com/hablapps/stateless.

https://github.com/hablapps/lensalgebra.

https://github.com/hablapps/koky.

Foster, J.N., Greenwald, M.B., Moore, J.T., Pierce, B.C., Schmitt, A.: Combinators for bi-directional tree transformations: a linguistic approach to the view update problem. ACM SIGPLAN Not. 40(1), 233–246 (2005)CrossRef

O’Connor, R.: Functor is to lens as applicative is to biplate: introducing multiplate. In: 7th ACM SIGPLAN Workshop on Generic Programming. ACM (2011)

Gibbons, J.: Unifying theories of programming with monads. In: Wolff, B., Gaudel, M.-C., Feliachi, A. (eds.) UTP 2012. LNCS, vol. 7681, pp. 23–67. Springer, Heidelberg (2013). https://doi.org/10.1007/978-3-642-35705-3_2CrossRefMATH

Wadler, P., Blott, S.: How to make ad-hoc polymorphism less ad hoc. In: Proceedings of the 16th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, pp. 60–76. ACM (1989)

Van Deursen, A., Klint, P., Visser, J.: Domain-specific languages: an annotated bibliography. ACM SIGPLAN Not. 35(6), 26–36 (2000)CrossRef

Abou-Saleh, F., Cheney, J., Gibbons, J., McKinna, J., Stevens, P.: Notions of bidirectional computation and entangled state monads. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 187–214. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19797-5_9CrossRefMATH

Abou-Saleh, F., Cheney, J., Gibbons, J., McKinna, J., Stevens, P.: Reflections on monadic lenses. In: Lindley, S., McBride, C., Trinder, P., Sannella, D. (eds.) A List of Successes That Can Change the World. LNCS, vol. 9600, pp. 1–31. Springer, Cham (2016). https://doi.org/10.1007/978-3-319-30936-1_1CrossRef

Cheney, J., McKinna, J., Stevens, P., Gibbons, J., Abou, F., et al.: Entangled state monads. In: BX Workshop (2014)

Pickering, M., Wu, N., Gibbons, J.: Profunctor optics: modular data accessors. Art Sci. Eng. Program. 1(2) (2017)

10.

Wadler, P.: Monads for functional programming. In: Jeuring, J., Meijer, E. (eds.) AFP 1995. LNCS, vol. 925, pp. 24–52. Springer, Heidelberg (1995). https://doi.org/10.1007/3-540-59451-5_2CrossRef

11.

Fischer, S., Hu, Z., Pacheco, H.: A clear picture of lens laws. In: Hinze, R., Voigtländer, J. (eds.) MPC 2015. LNCS, vol. 9129, pp. 215–223. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-19797-5_10CrossRefMATH

12.

Shkaravska, O.: Side-effect monad, its equational theory and applications. Arvutiteaduse teooriaseminar (2005)

13.

Jones, M.P.: Type classes with functional dependencies. In: Smolka, G. (ed.) ESOP 2000. LNCS, vol. 1782, pp. 230–244. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46425-5_15CrossRef

14.

Johnson, M., Rosebrugh, R.: Lens put-put laws: monotonic and mixed. Electr. Commun. EASST 49 (2012)

15.

Cheney, J., Lindley, S., Wadler, P.: A practical theory of language-integrated query. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming, ICFP 2013, New York, NY, USA, pp. 403–416. ACM (2013)

16.

Suzuki, K., Kiselyov, O., Kameyama, Y.: Finally, safely-extensible and efficient language-integrated query. In: Proceedings of the 2016 ACM SIGPLAN Workshop on Partial Evaluation and Program Manipulation, PEPM 2016, New York, NY, USA, pp. 37–48. ACM (2016)

17.

Rompf, T., Odersky, M.: Lightweight modular staging: a pragmatic approach to runtime code generation and compiled DSLs. ACM SIGPLAN Not. 46, 127–136 (2010)CrossRef

18.

Moors, A., Rompf, T., Haller, P., Odersky, M.: Scala-virtualized. In: Proceedings of the ACM SIGPLAN 2012 Workshop on Partial Evaluation and Program Manipulation, pp. 117–120. ACM (2012)

Title: Towards Optic-Based Algebraic Theories: The Case of Lenses
Authors: J. López-González
Juan M. Serrano
Publisher: Springer International Publishing
Book: Trends in Functional Programming
Print ISBN: 978-3-030-18505-3

Electronic ISBN: 978-3-030-18506-0

Copyright Year: 2019
DOI: https://doi.org/10.1007/978-3-030-18506-0_4

Springer Professional

Abstract

Please log in to get access to your license.

Dont have a licence yet? Then find out more about our products and how to get one now:

Springer Professional "Wirtschaft+Technik"

Springer Professional "Technik"

Springer Professional "Wirtschaft"

Premium Partner