Programming with dependent types
- interactive programs and coalgebras
~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~
Functional programming is based on the principle of reducing
terms applied to arguments to normal form. This allows to
define batch programs, which take a fixed given number of
inputs and compute a fixed number of outputs. Defining
interactive programs, which are given by a potentially
infinite interchange of inputs and outputs doesn't fit
directly into this paradigm, and several approaches have been
made to integrate interactive programs into functional
programming.
In this talk we give a different approach to the standard
approaches of representing interactive programs in functional
programming, which works very well in the presence of
dependent types. It is based on representing interactive
programs as non well-founded trees (trees which have infinite
branches) labelled by commands and with branching degree
given by responses for that command. Using this approach we
can define easily the IO monad, as it is used in Haskell for
defining interactive programs.
In order to have the data type of non well-founded trees as a
first class citizen, we introduce coalgebras in the context
of dependent type theory. Our approach will not define
coalgebras as a set of infinitary objects, but instead define
them dually to the use of algebraic data types (types
introduced by the keyword "data"). Whereas algebraic data
types are determined by their introduction rules
(constructors), coalgebraic types will be determined by their
elimination rules (eliminators).
Literature:
Peter Hancock and Anton Setzer: Interactive Programs in
Dependent Type Theory. In Peter Clote and Helmut
Schwichtenberg (Eds): Computer Science Logic, LNCS 1862,
2000, pp. 317 - 331
Anton Setzer: Coalgebras as Types determined by their
Elimination Rules. In Peter Dybjer et al: Epistemology versus
ontology: Essays on the foundations of mathematics in honour
of Per Martin-L{\"o}f. Springer, 2012, pp. 351 - 369