Abstract
Most interaction with a computer is via graphical user interfaces. These are traditionally implemented imperatively, using shared mutable state and callbacks. This is efficient, but is also difficult to reason about and error prone. Functional Reactive Programming (FRP) provides an elegant alternative which allows GUIs to be designed in a declarative fashion. However, most FRP languages are synchronous and continually check for new data. This means that an FRP-style GUI will “wake up” on each program cycle. This is problematic for applications like text editors and browsers, where often nothing happens for extended periods of time, and we want the implementation to sleep until new data arrives. In this paper, we present an asynchronous FRP language for designing GUIs called \(\lambda _{\mathsf {Widget}}\). Our language provides a novel semantics for widgets, the building block of GUIs, which offers both a natural Curry–Howard logical interpretation and an efficient implementation strategy.
Chapter PDF
Similar content being viewed by others
Keywords
References
Bahr, P., Graulund, C.U., Møgelberg, R.E.: Simply RaTT: a Fitch-style modal calculus for reactive programming without space leaks. Proceedings of the ACM on Programming Languages 3(ICFP), 1–27 (2019)
Bahr, P., Graulund, C.U., Møgelberg, R.: Diamonds are not forever: Liveness in reactive programming with guarded recursion (2020)
Benton, N., Wadler, P.: Linear logic, monads and the lambda calculus. Proceedings 11th Annual IEEE Symposium on Logic in Computer Science pp. 420–431 (1996)
Benton, P.N.: A mixed linear and non-linear logic: Proofs, terms and models. In: Pacholski, L., Tiuryn, J. (eds.) Computer Science Logic. pp. 121–135. Springer Berlin Heidelberg, Berlin, Heidelberg (1995)
Berry, G., Cosserat, L.: The ESTEREL synchronous programming language and its mathematical semantics. In: Brookes, S.D., Roscoe, A.W., Winskel, G. (eds.) Seminar on Concurrency. pp. 389–448. Springer Berlin Heidelberg, Berlin, Heidelberg (1985)
Birkedal, L., Møgelberg, R.E., Schwinghammer, J., Støvring, K.: First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. In: In Proc. of LICS (2011)
Bizjak, A., Grathwohl, H.B., Clouston, R., Møgelberg, R.E., Birkedal, L.: Guarded dependent type theory with coinductive types. In: International Conference on Foundations of Software Science and Computation Structures. pp. 20–35. Springer (2016)
Blackburn, P., de Rijke, M., Venema, Y.: Modal Logic. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press (2002)
Caspi, P., Pilaud, D., Halbwachs, N., Plaice, J.A.: LUSTRE: A Declarative Language for Real-time Programming. In: Proceedings of the 14th ACM SIGACT-SIGPLAN Symposium on Principles of Programming Languages. pp. 178–188. POPL ’87, ACM, New York, NY, USA (1987). https://doi.org/10.1145/41625.41641
Cave, A., Ferreira, F., Panangaden, P., Pientka, B.: Fair Reactive Programming. In: Proceedings of the 41st ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. pp. 361–372. POPL ’14, ACM, San Diego, California, USA (2014). https://doi.org/10.1145/2535838.2535881
Clouston, R.: Fitch-style modal lambda calculi. In: Baier, C., Dal Lago, U. (eds.) Foundations of Software Science and Computation Structures. pp. 258–275. Springer International Publishing, Cham (2018)
Elliott, C.: Push-pull functional reactive programming. In: Haskell Symposium (2009), http://conal.net/papers/push-pull-frp
Elliott, C., Hudak, P.: Functional reactive animation. In: Proceedings of the Second ACM SIGPLAN International Conference on Functional Programming. pp. 263–273. ICFP ’97, ACM, New York, NY, USA (1997). https://doi.org/10.1145/258948.258973
Girard, J.Y.: Linear logic. Theoretical Computer Science 50(1), 1 – 101 (1987). https://doi.org/10.1016/0304-3975(87)90045-4
Graulund, C.: Lambda Calculus for Reactive Programming. Master’s thesis, IT University of Copenhagen (2018)
Haim, M., Malherbe, O.: Linear Hyperdoctrines and Comodules. arXiv e-prints \({\text{arXiv:}}\)1612.06602 (Dec 2016)
Jeffrey, A.: LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs. In: Proceedings of the sixth workshop on Programming Languages meets Program Verification, PLPV 2012, Philadelphia, PA, USA, January 24, 2012. pp. 49–60. Philadelphia, PA, USA (2012). https://doi.org/10.1145/2103776.2103783
Jeltsch, W.: Towards a common categorical semantics for linear-time temporal logic and functional reactive programming. Electronic Notes in Theoretical Computer Science 286, 229–242 (2012)
Jeltsch, W.: Temporal Logic with “Until”, Functional Reactive Programming with Processes, and Concrete Process Categories. In: Proceedings of the 7th Workshop on Programming Languages Meets Program Verification. pp. 69–78. PLPV ’13, ACM, New York, NY, USA (2013). https://doi.org/10.1145/2428116.2428128
Krishnaswami, N.R.: Higher-order Functional Reactive Programming Without Spacetime Leaks. In: Proceedings of the 18th ACM SIGPLAN International Conference on Functional Programming. pp. 221–232. ICFP ’13, ACM, Boston, Massachusetts, USA (2013). https://doi.org/10.1145/2500365.2500588
Krishnaswami, N.R., Benton, N.: Ultrametric semantics of reactive programs. In: 2011 IEEE 26th Annual Symposium on Logic in Computer Science. pp. 257–266. IEEE Computer Society, Washington, DC, USA (June 2011). https://doi.org/10.1109/LICS.2011.38
Lawvere, F.W.: Adjointness in foundations. Dialectica 23(3-4), 281–296 (1969). https://doi.org/10.1111/j.1746-8361.1969.tb01194.x
MacLane, S., Moerdijk, I.: Sheaves in Geometry and Logic: A First Introduction to Topos Theory. Universitext, Springer New York (1994). https://doi.org/10.1007/978-1-4612-0927-0
Maietti, M.E., de Paiva, V., Ritter, E.: Categorical models for intuitionistic and linear type theory. In: Tiuryn, J. (ed.) Foundations of Software Science and Computation Structures. pp. 223–237. Springer Berlin Heidelberg, Berlin, Heidelberg (2000)
Nakano, H.: A modality for recursion. In: Proceedings Fifteenth Annual IEEE Symposium on Logic in Computer Science (Cat. No.99CB36332). pp. 255–266. IEEE Computer Society, Washington, DC, USA (June 2000). https://doi.org/10.1109/LICS.2000.855774
Pfenning, F., Davies, R.: A judgmental reconstruction of modal logic. Mathematical Structures in Computer Science 11(4), 511–540 (2001). https://doi.org/10.1017/S0960129501003322
Pnueli, A.: The temporal logic of programs. In: 18th Annual Symposium on Foundations of Computer Science (sfcs 1977). pp. 46–57. IEEE (1977)
Pouzet, M.: Lucid Synchrone, version 3. Tech. rep., Laboratoire d’Informatique de Paris (2006)
Szamozvancev, D.: Semantics of temporal type systems. Master’s thesis, University of Cambridge (2018)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Open Access This chapter is licensed under the terms of the Creative Commons Attribution 4.0 International License (http://creativecommons.org/licenses/by/4.0/), which permits use, sharing, adaptation, distribution and reproduction in any medium or format, as long as you give appropriate credit to the original author(s) and the source, provide a link to the Creative Commons license and indicate if changes were made.
The images or other third party material in this chapter are included in the chapter's Creative Commons license, unless indicated otherwise in a credit line to the material. If material is not included in the chapter's Creative Commons license and your intended use is not permitted by statutory regulation or exceeds the permitted use, you will need to obtain permission directly from the copyright holder.
Copyright information
© 2021 The Author(s)
About this paper
Cite this paper
Graulund, C.U., Szamozvancev, D., Krishnaswami, N. (2021). Adjoint Reactive GUI Programming. In: Kiefer, S., Tasson, C. (eds) Foundations of Software Science and Computation Structures. FOSSACS 2021. Lecture Notes in Computer Science(), vol 12650. Springer, Cham. https://doi.org/10.1007/978-3-030-71995-1_15
Download citation
DOI: https://doi.org/10.1007/978-3-030-71995-1_15
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-030-71994-4
Online ISBN: 978-3-030-71995-1
eBook Packages: Computer ScienceComputer Science (R0)