Bernd Finkbeiner
ABSTRACT
Functional Reactive Programming (FRP) is a paradigm that has simplified the construction of reactive programs. There are many libraries that implement incarnations of FRP, using abstractions such as Applicative, Monads, and Arrows. However, finding a good control flow, that correctly manages state and switches behaviors at the right times, still poses a major challenge to developers. An attractive alternative is specifying the behavior instead of programming it, as made possible by the recently developed logic: Temporal Stream Logic (TSL). However, it has not been explored so far how Control Flow Models (CFMs), resulting from TSL synthesis, are turned into executable code that is compatible with libraries building on FRP. We bridge this gap, by showing that CFMs are a suitable formalism to be turned into Applicative, Monadic, and Arrowized FRP. We demonstrate the effectiveness of our translations on a real-world kitchen timer application, which we translate to a desktop application using the Arrowized FRP library Yampa, a web application using the Monadic Threepenny-GUI library, and to hardware using the Applicative hardware description language ClaSH.
- Heinrich Apfelmus. 2012. Reactive-banana. Haskell library available at http://www. haskell. org/haskellwiki/Reactive-banana (2012).Google Scholar
- Heinrich Apfelmus. 2013. Threepenny-gui. https://wiki.haskell.org/ Threepenny-gui .Google Scholar
- C.P.R. Baaij. 2015. Digital circuit in C λaSH: functional specifications and type-directed synthesis. Ph.D. Dissertation.Google Scholar
- Manuel Bärenz and Ivan Perez. 2018. Rhine: FRP with type-level clocks. In Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, Haskell@ICFP 2018, St. Louis, MO, USA, September 27-17, 2018, Nicolas Wu (Ed.). ACM, 145–157. Google ScholarDigital Library
- Tewodros Beyene, Swarat Chaudhuri, Corneliu Popeea, and Andrey Rybalchenko. 2014. A Constraint-based Approach to Solving Games on Infinite Graphs. In POPL. ACM, 221–233. Google ScholarDigital Library
- Roderick Bloem, Barbara Jobstmann, Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. 2012. Synthesis of reactive (1) designs. J. Comput. System Sci. 78, 3 (2012), 911–938. Google ScholarDigital Library
- Andrew Cave, Francisco Ferreira, Prakash Panangaden, and Brigitte Pientka. 2014. Fair Reactive Programming (POPL ’14). ACM, New York, NY, USA, 361–372. Google ScholarDigital Library
- Antony Courtney, Henrik Nilsson, and John Peterson. 2003. The Yampa Arcade. In Proceedings of the 2003 ACM SIGPLAN workshop on Haskell. ACM, 7–18. Google ScholarDigital Library
- David Cyrluk and Paliath Narendran. 1994. Ground temporal logic: A logic for hardware verification. In CAV. Springer, 247–259. Google ScholarDigital Library
- Evan Czaplicki and Stephen Chong. 2013. Asynchronous Functional Reactive Programming for GUIs (PLDI ’13). ACM, New York, NY, USA, 411–422. Google ScholarDigital Library
- Rayna Dimitrova and Bernd Finkbeiner. 2012. Counterexample-Guided Synthesis of Observation Predicates. Springer Berlin Heidelberg, Berlin, Heidelberg, 107–122. Google ScholarDigital Library
- Conal Elliott and Paul Hudak. 1997. Functional reactive animation. In ACM SIGPLAN Notices, Vol. 32. ACM, 263–273. Google ScholarDigital Library
- Bernd Finkbeiner, Felix Klein, Ruzica Piskac, and Mark Santolucito. 2019. Temporal Stream Logic: Synthesis beyond the Bools. In Computer Aided Verification - 31th International Conference, CAV 2019, New York, NY, USA, July 15-18, 2019, Proceedings, Part I.Google Scholar
- Samuel Gélineau. 2016. FRPzoo - Comparing many FRP implementations by reimplementing the same toy app in each. https://github.com/gelisam/ frp-zoo .Google Scholar
- Caleb Helbling and Samuel Z. Guyer. 2016. Juniper: A Functional Reactive Programming Language for the Arduino (FARM 2016). ACM, New York, NY, USA, 9. Google ScholarDigital Library
- John Hughes. 2000. Generalising monads to arrows. Science of computer programming 37, 1 (2000), 67–111. Google ScholarDigital Library
- Alan Jeffrey. 2012. LTL types FRP: linear-time temporal logic propositions as types, proofs as functional reactive programs, Koen Claessen and Nikhil Swamy (Eds.). ACM, 49–60. Google ScholarDigital Library
- Wolfgang Jeltsch. 2012. Towards a common categorical semantics for lineartime temporal logic and functional reactive programming. ENTCS 286 (2012), 229–242. Google ScholarDigital Library
- Gangyuan Jing, Tarik Tosun, Mark Yim, and Hadas Kress-Gazit. 2016. An End-To-End System for Accomplishing Tasks with Modular Robots. In RSS.Google Scholar
- Ayrat Khalimov, Roderick Paul Bloem, and Swen Jacobs. 2014. Parameterized Synthesis Case Study: AMBA AHB. In SYNT 2014, Susmit Jha Krishnendu Chatterjee, Rüdiger Ehlers (Ed.).Google Scholar
- Neelakantan R Krishnaswami. 2013. Higher-order functional reactive programming without spacetime leaks. In ACM SIGPLAN Notices, Vol. 48. ACM, 221–232. Google ScholarDigital Library
- Viktor Kuncak, Mikaël Mayer, Ruzica Piskac, and Philippe Suter. 2010. Complete functional synthesis. ACM Sigplan Notices 45, 6 (2010), 316–329. Google ScholarDigital Library
- Sam Lindley, Philip Wadler, and Jeremy Yallop. 2011. Idioms are oblivious, arrows are meticulous, monads are promiscuous. ENTCS 229, 5 (2011), 97–117. Google ScholarDigital Library
- Hai Liu, Eric Cheng, and Paul Hudak. 2011. Causal commutative arrows. J. Funct. Program. 21, 4-5 (2011), 467–496. Google ScholarDigital Library
- Hai Liu and Paul Hudak. 2007. Plugging a space leak with an arrow. ENTCS 193 (2007), 29–45. Google ScholarDigital Library
- Parthasarathy Madhusudan. 2011. Synthesizing reactive programs. In LIPIcsLeibniz International Proceedings in Informatics, Vol. 12.Google Scholar
- Geoffrey Mainland. 2007. Why It’s Nice to be Quoted: Quasiquoting for Haskell. In Proceedings of the ACM SIGPLAN workshop on Haskell workshop. ACM, 73–82. Google ScholarDigital Library
- Philipp J. Meyer, Salomon Sickert, and Michael Luttenberger. 2018. Strix: Explicit Reactive Synthesis Strikes Back!. In Computer Aided Verification - 30th International Conference, CAV 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 14-17, 2018, Proceedings, Part I (Lecture Notes in Computer Science), Hana Chockler and Georg Weissenbacher (Eds.), Vol. 10981. Springer, 578–586.Google Scholar
- Tom E Murphy. 2016. A livecoding semantics for functional reactive programming. In Functional Art, Music, Modelling, and Design. ACM, 48–53. Google ScholarDigital Library
- Peter Michael Osera and Steve Zdancewic. 2015. Type-and-example-directed program synthesis. In ACM SIGPLAN Notices, Vol. 50. ACM, 619–630. Google ScholarDigital Library
- Gergely Patai. 2010. Efficient and compositional higher-order streams. In International Workshop on Functional and Constraint Logic Programming. Springer. Google ScholarDigital Library
- Ross Paterson. 2001. A New Notation for Arrows. In International Conference on Functional Programming. ACM Press, 229–240. http://www.soi.city. ac.uk/~ross/papers/notation.html Google ScholarDigital Library
- Ivan Perez. 2017. GALE: a functional graphic adventure library and engine. In Proceedings of the 5th ACM SIGPLAN International Workshop on Functional Art, Music, Modeling, and Design, FARM@ICFP 2018, Oxford, UK, September 9, 2017. 28–35. Google ScholarDigital Library
- Ivan Perez, Manuel Bärenz, and Henrik Nilsson. 2016. Functional reactive programming, refactored. In International Conference on Functional Programming. ACM. Google ScholarDigital Library
- Ivan Perez and Henrik Nilsson. 2017. Testing and debugging functional reactive programming. PACMPL 1, ICFP (2017), 2:1–2:27. Google ScholarDigital Library
- Nir Piterman, Amir Pnueli, and Yaniv Sa’ar. 2006. Synthesis of Reactive(1) Designs. In VMCAI. Google ScholarDigital Library
- Atze van der Ploeg and Koen Claessen. 2015. Practical principled FRP: forget the past, change the future, FRPNow!. In ACM SIGPLAN Notices, Vol. 50. ACM, 302–314. Google ScholarDigital Library
- Nadia Polikarpova, Ivan Kuraj, and Armando Solar-Lezama. 2016. Program synthesis from polymorphic refinement types. In Proceedings of the 37th ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI 2016, Santa Barbara, CA, USA, June 13-17, 2016, Chandra Krintz and Emery Berger (Eds.). ACM, 522–538. Google ScholarDigital Library
- Vasumathi Raman, Alexandre Donzé, Dorsa Sadigh, Richard M. Murray, and Sanjit A. Seshia. 2015. Reactive Synthesis from Signal Temporal Logic Specifications. In HSCC. 239–248. Google ScholarDigital Library
- Mark Santolucito, Donya Quick, and Paul Hudak. 2015. Media Modules: Intermedia Systems in a Pure Functional Paradigm. In ICMC 2015, Denton, TX, USA. http://hdl.handle.net/2027/spo.bbp2372.2015.077Google Scholar
- Kensuke Sawada and Takuo Watanabe. 2016. Emfrp: a functional reactive programming language for small-scale embedded systems. In Companion Proceedings of the 15th International Conference on Modularity, Málaga, Spain, March 14 - 18, 2016, Lidia Fuentes, Don S. Batory, and Krzysztof Czarnecki (Eds.). ACM, 36–44. Google ScholarDigital Library
- Neil Sculthorpe and Henrik Nilsson. 2010. Keeping calm in the face of change. Higher-Order and Symbolic Computation 23, 2 (2010), 227–271. Google ScholarDigital Library
- Zhiyong Shan, Tanzirul Azim, and Iulian Neamtiu. 2016. Finding Resume and Restart Errors in Android Applications (OOPSLA 2016). ACM, New York, NY, USA, 864–880. Google ScholarDigital Library
- Armando Solar-Lezama. 2013. Program sketching. STTT 15, 5-6 (2013), 475–495. Google ScholarDigital Library
- Ryan Trinkle. 2017. Reflex-FRP. https://github.com/reflex-frp/reflex .Google Scholar
- Martin T. Vechev, Eran Yahav, and Greta Yorsh. 2013. Abstraction-guided synthesis of synchronization. STTT 15, 5-6 (2013), 413–431. Google ScholarDigital Library
- Andreas Voellmy, Junchang Wang, Y Richard Yang, Bryan Ford, and Paul Hudak. 2013. Maple: Simplifying SDN programming using algorithmic policies. CCR 43, 4 (2013), 87–98. Google ScholarDigital Library
- Daniel Winograd-Cort. 2015. Effects, Asynchrony, and Choice in Arrowized Functional Reactive Programming. Ph.D. Dissertation. Yale University.Google Scholar
- Daniel Winograd-Cort and Paul Hudak. 2014. Settable and Non-interfering Signal Functions for FRP: How a First-order Switch is More Than Enough. In Proceedings of the 19th ACM SIGPLAN International Conference on Functional Programming (ICFP ’14). ACM, New York, NY, USA, 213–225. Google ScholarDigital Library
- Jeremy Yallop and Hai Liu. 2016. Causal commutative arrows revisited. In Proceedings of the 9th International Symposium on Haskell. ACM, 21–32. Google ScholarDigital Library
Index Terms
- Synthesizing functional reactive programs
Recommendations
Functional reactive programming, continued
Haskell '02: Proceedings of the 2002 ACM SIGPLAN workshop on HaskellFunctional Reactive Programming (FRP) extends a host programming language with a notion of time flow. Arrowized FRP (AFRP) is a version of FRP embedded in Haskell based on the arrow combinators. AFRP is a powerful synchronous dataflow programming ...
Safe functional reactive programming through dependent types
ICFP '09Functional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-...
Safe functional reactive programming through dependent types
ICFP '09: Proceedings of the 14th ACM SIGPLAN international conference on Functional programmingFunctional Reactive Programming (FRP) is an approach to reactive programming where systems are structured as networks of functions operating on signals. FRP is based on the synchronous data-flow paradigm and supports both continuous-time and discrete-...
Comments