We propose a representation of interactive systems in dependent type
theory. This is meant as a basis for an execution environment for
dependently typed programs, and for reasoning about their
construction; there may be wider applications. The inspiration is
the `I/O-monad' of Haskell. The fundamental notion is an I/O-tree;
its definition is parameterised over a general notion of dependently
typed, command-response interactions called a world. I/O trees
represent strategies for one of the parties in a command/response
interaction -- the notion is not confined to functional programming.
The definitions make essential use of the expressive strength of
dependent typing. We present I/O-trees in two forms that we call
`non-normalising' and `normalising'. The first form, which is
simpler, is suitable for Turing-complete functional programming
languages with general recursion. The second is definable within
(ordinary) normalising type theory and we identify programs written
in it as `normalising I/O programs'. We define new looping
constructs (while and repeat), and a new refinement construct
(redirect), which We introduce a bisimulation relation between
interactive programs, with respect to which we prove the monad laws
and defining equations of while.
Keywords: Functional programming, reactive programming, interaction,
dependent types, monadic I/O, while-construct, repeat-construct,
refinement.
