Quotation Adelsberger, Stephan. 2017. Interactive programming in Agda - Objects and graphical user interfaces. Journal of Functional Programming 27, 1-2.




We develop a methodology for writing interactive and object-based programs (in the sense of Wegner) in dependently typed functional programming languages. The methodology is implemented in the ooAgda library. ooAgda provides a syntax similar to the one used in object-oriented programming languages, thanks to Agda's copattern matching facility. The library allows for the development of graphical user interfaces (GUIs), including the use of action listeners. Our notion of interactive programs is based on the IO monad defined by Hancock and Setzer, which is a coinductive data type. We use a sized coinductive type which allows us to write corecursive programs in a modular way. Objects are server-side interactive programs that respond to method calls by giving answers and changing their state. We introduce two kinds of objects: simple objects and IO objects. Methods in simple objects are pure, while method calls in IO objects allow for interactions before returning their result. Our approach also allows us to extend interfaces and objects by additional methods. We refine our approach to state-dependent interactive programs and objects through which we can avoid exceptions. For example, with a state-dependent stack object, we can statically disable the pop method for empty stacks. As an example, we develop the implementation of recursive functions using a safe stack. Using a coinductive notion of object bisimilarity, we verify basic correctness properties of stack objects and show the equivalence of different stack implementations. Finally, we give a proof of concept that our interaction model allows to write GUI programs in a natural way: we present a simple drawing program, and a program which allows the users to move a small spaceship using a button.


Press 'enter' for creating the tag

Publication's profile

Status of publication Published
Affiliation WU
Type of publication Journal article
Journal Journal of Functional Programming
Citation Index SCI
Language English
Title Interactive programming in Agda - Objects and graphical user interfaces
Volume 27
Year 2017
Page from 1
Page to 2
Reviewed? Y
URL https://www.cambridge.org/core/journals/journal-of-functional-programming/article/div-classtitleinteractive-programming-in-agda-objects-and-graphical-user-interfacesdiv/56ECE95C3A0C208D5ABCD072643BC8FB
DOI http://dx.doi.org/10.1017/S0956796816000319


Adelsberger, Stephan (Details)
Institute for Information Systems and New Media IN (Details)
Google Scholar: Search