Purely Functional Interactive Programming
Neelakantan Krishnaswami ( University of Birmingham )
Programming graphical user interfaces is simultaneously one of the most common and most difficult of all programming tasks. Correctly using typical GUI libraries requires writing programs in an imperative, concurrent, continuation-passing style. Any one of these adjectives is a serious intellectual challenge, and so confronting all three at once is a rather daunting challenge!
Moreover, while functional programming languages such as Ocaml and Haskell have demonstrated that many -- even most -- programming tasks lend themselves to simple and elegant formulations in terms of functional programming, interactive programs have proven surprisingly resistant to being written in a functional style.
In this talk, I will describe how two well-understood and natural extensions to the typed lambda calculus -- guarded recursion and linear types -- permit writing GUI programs in a purely functional style. Guarded recursion permits using types to describe temporal behaviour, and linear types permit describing spatial behaviour and object identity, which together permit giving types which accurately describe the behavior of interactive programs, without compromising the strong reasoning principles that make functional programming useful.
I will demonstrate this point by giving code examples in AdjS, a new purely functional language supporting these features.