Interactive Programs in Dependent Type Theory

Anton Setzer

(Swansea University)

Functional programming is essentially the evaluation of expressions. Programs we can write in this way are not very interactive: we can only apply an expression to several arguments and get as answer the result of the reduction of this expression, so we have a fixed finite number of inputs and one output. This way one cannot write truly interactive programs like an editor, which have possibly infinitely many interactions with the user.

We will review several approaches taken in functional programming for solving the problem and present our approach which is essentially based on Moggi's monads: interactive programs are possibly non-well-founded trees with nodes labeled by interactive commands and with branching degree over the response set corresponding to this command. We will then discuss the problem: as in ordinary mathematics, in dependent type theory most standard structures are well-founded, but what is needed for defining interactive programs are non-well-founded structures. We will slightly generalize this problem to the problem of having rules for final coalgebras in dependent type theory.

We will then, using ideas present in Peter Aczel's non-well-founded set theory, introduce such rules: Non-well-founded structures are introduced as graphs, but we have only restricted elimination rules available. We define rules corresponding to coiteration and corecursion. We indicate, why the successor for the co-natural numbers is difficult to compute using coiteration and results in high complexity, whereas with corecursion this is simple, similar to the fact that the predecessor is difficult to compute for the natural numbers using iteration, but easy using recursion. Finally we introduce useful functions for defining elements of the final coalgebras: while- and repeat loops, a fixed-point construction and redirect, which allows to translate programs in a high-level language into a low level language by replacing commands of the high level language by programs in the low level language. Redirect allows to refine programs in a top down approach and to build libraries.
Thursday 27th September 2001, 14:00
Robert Recorde Room
Department of Computer Science