Interactive Programs in Dependent Type Theory

Peter Hancock^{1} and Anton Setzer^{2}

1 Dept. of Computing Science, University of Edinburgh, James Clerk Maxwell

Building, King’s Buildings, Mayfield Road, Edinburgh EH9 3JZ, Scotland,

fax: +44 131 667 7209, phone: +44 131 650 5129, pgh@dcs.ed.ac.uk. 2 Dept. of Mathematics, Uppsala University, P.O. Box 480, S-751 06 Uppsala, Sweden, fax: +46 18 4713201, phone: +46 18 4713284, setzer@math.uu.se.

Abstract. 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 permits the implementation of libraries. 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, repetition constructs, refinement.

1 I/O Concepts in Type Theory

Programming languages based on dependent types. A bit over 20 years ago Martin-Löf suggested that his type theory, originally developed as a framework for constructive mathematics, could be considered as a programming language [4]. Since that time, his suggestion has been taken up and explored in a number of ways (see for example in [6]). A question which so far seems to have received little attention is what form of input-output interface such programs should have. Indeed it is only in the last 10 years or so that this question has received a satisfactory answer in the context of conventional functional programming, through the efforts of Moggi [5], Wadler [10], and others.

Dependent types give us the ability to set up type systems for programming which can express with full precision any property we know how to define mathematically. For example, we can express the requirement for a function which maps lists to sorted lists using a dependent type [6]. Remarkably, with certain provisos of largely academic interest, we can still check the type of a program mechanically, and type-correctness carries full assurance that it satisfies its specification. The interest of dependent types for programming is therefore considerable. In the past few years, implementations of dependent type systems for functional programming have begun to appear [1].

Conventions, and plan of paper. In the following, we will work in standard dependent type theory (for example [6]) with the usual introduction and elimination rules and intensional equality, extended by some other rules. We will refer to it simply as ‘type theory’. The notation we use, which is for the most part standard, is summarised in the appendix of the paper. Note that we sometimes omit indices and superscripts.

The plan of the paper is as follows. In the remainder of this section, we draw attention to the need for a model of interaction in type theory, and recall the approach taken by the designers of the functional programming language Haskell, using a monadic type form whose values are I/O-programs. In the next section, we present our extension of this notion, making use of type dependency. The third section introduces two repetition constructs (while and repeat), and a refinement construction. In the fourth, we point out that these can destroy normalisation, and develop an alternative formulation which preserves it. Finally there is a concluding section, followed by a summary of our notation.

The need for interactive programs in type theory. Traditional ‘batch’ programs may be written in type theory as functions from input values (given in advance) to output values. The output from such a program is obtained by evaluating the result of applying the function to its input. This batch model is adequate for a large class of programs, typically computationally intensive numerical search or optimisation programs. It is not however adequate for a program which runs, say, in the guidance system of an airplane.

The programs with which one is ordinarily confronted participate in interactions with their environment, i.e. us, while they are running. We give input via various devices like keyboard, mouse, or microphone and get output via devices like monitor, printer or loudspeaker, and this input-output cycle is repeated again and again. There may also be interaction with the file system and the network. Other kinds of program may be embedded in a physical system, in which there is continual interaction with physical sensors and actuators of some kind. So if we want to use type theory as a practical functional programming language, we have to consider how to use it to write interactive (or reactive) programs.

Some approaches to interactive programs in type theory. In conventional functional programming, several approaches to interaction have been pursued. A good survey of some of these approaches is made in [7]: dialogues (or lazy streams), continuations, and monadic I/O. (Mention should also be made of the ‘uniqueness types’ of the language Concurrent Clean, although a definitive exposition of this approach doesn’t seem to have been published yet.^{1} In this paper we follow the monadic approach, introduced by E. Moggi [5], upon which the input/output (I/O-) system of the language Haskell^{2} has been erected. A monad (the concept comes from category theory) is a triple (M, ∗, η), whose components, written in dependent type theory, have types

M : Set → Set ,
∗ : (A, B : Set, p : M A, q : A → M B) → M B ,
η : (A : Set, a : A) → M A ,

such that the following laws hold with respect to suitable equality = (which will not be definitional equality).

η_{a}^{A} ∗_{A,B} q = q a ,
p ∗_{A,B} λx.η_{x}^{A} = p ,
(p ∗_{A,B} q) ∗_{B,C} r = p ∗_{A,B} (λx.q x ∗_{B,C} r) .

A special case of a monad is the I/O-monad. When referring to the I/O-monad we write (IO A) instead of (M A). The interpretation of IO is as follows.

(a) For a given set A, (IO A) is the set of interactive programs which may or may not terminate, but terminate only with a result a of type A.

(b) p ∗ q is a program whose execution begins by executing p. If execution terminates with result a, then the program continues with (q a). The result of the whole program is the result of (q a).

(c) η_{a} is the program which has no interaction but terminates immediately, yielding result a.

In addition to these general components of any monad, there are functions specific to the kind of computations the programs are to evoke. For example, we can deal with programs that communicate by writing and reading strings (such as text lines): write : String → IO 1, read : IO String. Here (write s) is the program which outputs s on some device and returns •, and read : IO String, is the program which reads a string and returns it.

Note that type checking does not require any interaction. What we really type check is the text of the program, rather than its execution. To execute or run a program means to interpret the program text as the specification of a certain I/O-behaviour.

For the I/O-monad, one sees that the laws mentioned above should hold with respect to an equality which identifies behaviourally equal programs.

Interactive programs are written in Haskell by using a form of the I/O-monad that gives access to most of the usual facilities of a traditional operating system, including files, graphics, time, as well as control features such as exception handling or multi-threading.

1 http://www.cs.kun.nl/~clean
2 http://haskell.org

The I/O-monad seems to be the most promising approach for the representation of interactive programs within dependent type theory. To add it to type theory as a new concept with new typing rules would however require extending a considerable body of metatheoretical research to the extended theory. Since we can define in type theory powerful data types, an easier approach is to define the I/O-monad directly in type theory. Thus the only feature we need over and above ‘mathematical’ type theory is that of actually running an I/O-program.

2 I/O-Trees

Worlds. Interactive programs are built from interactive commands. In dependent type theory we can define such a set of interactive commands in a very general way:

General assumption and definition 2.1. A world w is a pair ⟨C, R⟩ such that C : Set and R : C → Set. In the following w is always a world ⟨C, R⟩. We will in most cases omit the parameter w.

The idea is that C is the set of instructions or commands. These include commands to obtain input, commands to obtain output, and commands with a mixed effect. If c : C is a command, then (R c) is the type of responses or termination codes produced when such the command c has been performed. So we might have constructors

(a) write : String → C with R(write s) = 1, and (write s) is the command to write s and return • : 1 for success.

(b) read : C, with (R read = String), where read stands for the command to read a string and returns it.

Of course in practice the commands would be more complex. For example, there might be an embellishment of write where R(write s) = {success, fail} and (write r) returns the information whether the output was performed successfully or not. More generally, there may be commands expressing interaction with file systems, network etc.

I/O-trees. We want to define the I/O-monad as a data type already in type theory. It seems particularly suitable to define it as an inductive data type, because using the elimination rule associated with such types we can then carry out program transformations. A naïve approach would be to take ∗, η and the additional primitive instructions such as read and (write a) as constructors for this type. However we need to verify the monad laws, and it turns out to that the naïve approach requires us to define a rather complicated equality relation. The situation is analogous to the definition of the set of natural numbers. We could define it from 0, 1 and +, which correspond in the I/O-monad to η, the primitive instructions and ∗. It is however much better to take 0 and successor S as constructors, and to define 1 and addition. What corresponds now to S in the IO-monad? This should be the operation which takes an instruction and a family of programs depending on the result of performing that instruction, and creates a new program that begins by performing this instruction and then continues with the program determined by its result. Instructions are given by C, where w = ⟨C, R⟩ is a world, and R provides the result type.The rules for IO_{w} A are:

IO_{w} : Set → Set, where IO_{w} A has constructors
leaf : A → IO_{w} A ,
do : (c : C, p : R c → IO A) → IO A .

The constructor (leaf a) is what was written η_{a}^{A} before, and (do c p) denotes the program that first executes the command c, and depending on the result r : R c of this execution continues with (p r).

Note that (IO_{w} A) is now parametrised with respect to w, a feature which can be expressed only with dependent types.

(IO_{w} A) is the set of well-founded trees with leaves in A and inner nodes labelled by some c : C having branching degree (R c). If we compare (IO_{w} A) with standard type theory we see that we simply have a slight extension of the W-type. In fact we can even define (IO_{w} A) directly in terms of the W-type:

IO_{w} A = Wx : (C + A).R′ x , where \begin{matrix}R′(inl c) = R c , \\ R′(inr a) = 0 . \end{matrix}

We therefore call (IO_{w} A) the type of I/O-trees with leaves in A.

Execution of I/O-programs. Up to now we have defined an inductive data type of I/O-programs within constructive type theory, but there is still no way to actually run such a program. Execution is an external operation rather than a constant within type theory. Just as an implementation of type theory will provide an external operation or facility to compute (and display) the (head-) normal form of a term, so we propose to provide a second operation which executes a term which denotes an I/O-program.

More precisely, this works as follows. Let w_{0} = ⟨C_{0}, R_{0}⟩ be a world corresponding to the real commands, so that to every c : C_{0} there corresponds a real I/O-command c having some value r : R_{0} c as result. If we have derived p : IO_{w_{0}} A then the external operation execute can be performed upon p. The operation execute does the following. It reduces p to canonical form, i.e. to a term of constructor form. This form must be either (leaf a) or (do c q). If it is (leaf a), then a : A and execution terminates, yielding as result a (which, when running the program from a command line will be displayed in a similar way as the result of the evaluation of an expression). If it is (do c q), then first the interactive command corresponding to c is performed obtaining a result r : R c, after which execution continues with (q r).

Roughly speaking a program p is evaluated to normal form, as it were ‘fetching’ the next instruction. The instruction is ‘executed’, and the result used to select the next program to be evaluated. Another way of looking at it is that through successive interactions we trace out a descending chain through the tree p.

A first example. In the following example we assume commands readstr for reading a string, (writestr s) for writing a string s. Further let =_{String} be a decidable (boolean valued) equality on strings. The following program prompts for the root-password. If the user types in the right one (“Wurzel”^{3}) the program terminates successfully, but otherwise responds with “Login incorrect” and then fails. We use some syntactic sugar.

C = { readstr } ∪ { writestr s | s : string } : Set ,
R : C → Set ,
R readstr = string ,
R (writestr s) = 1 ,
Wurzel = do writestr “Password (root):” λa. do readstr λs. if s = “Wurzel” then leaf success else do (writestr “Login incorrect”) λa. leaf fail

: IO { success, fail } .

η, ∗, interact. It is now easy to define the operations η and ∗:

η_{a}^{A} = leaf a ,
leaf a ∗_{A,B} q = q a ,
do c p ∗_{A,B} q = do c (λx.p x ∗_{A,B} q) .

The monad laws are then provable for well-founded trees with respect to extensional equality.

Additionally we can define a function interact : (c : C) → IO (R c) by interact c = do c (λx.leaf x). The program (interact c) simply executes the command c and returns its result.

3 Constructions for Defining I/O-trees

It should be possible to define interactive programs with infinitely many interactions. For instance, if we execute an editor and never terminate the program, the execution should go on for ever. So we need constructions for defining such programs. This will however destroy normalisation. We will see in Sect. 4, how to modify the concept in order to obtain a normalising type theory. The definitions of all constructions in this section are possible only in the presence of dependent types, which demonstrate their expressive power.

We will first look at the repeat-loop, which is very useful in examples.

3 This really happened.

repeat. Assume A, B : Set, b : B, p : B → IO_{w} (B + A). We want to define a program repeat_{A} B b p : IO_{w} A, which, when executed, operates as follows. First program (p b) is executed. If it terminates with result (inl b′), then the program continues with (repeat_{A} B b′ p). If it terminates with (inr a), the program terminates and returns a.

However, if p b = leaf a for some b : B, this might result in an expression that does not evaluate to constructor form – for instance (repeat_{B} bλx.leaf (inl b)). Therefore we have to restrict p, and the easiest solution is to replace (IO_{w} (B + A)) by (IO_{w}^{+} (B + A)). Here for D : Set let IO_{w}^{+} D = Σc : C.R c → IO_{w} D be the set of I/O-programs with results in D, with one interaction (namely command c). Let do^{+} c p = ⟨c, p⟩ : IO_{w} D and, if p : IO_{w}^{+} D, let p^{−} : IO_{w} D be defined by (do^{+} c p)^{−} = do c p.

The definition (which uses full recursion and so allows us to define non-well-founded trees and form non-normalising terms) of the repeat construction is as follows:

repeat_{w} : (A, B : Set, b : B, p : B → IO_{w}^{+} (B + A)) → IO_{w} B ,
repeat_{w,A} B b p = (p b)^{−} ∗_{w,B+A,A} q ,

where

q (inl b′) = repeat_{w,A} B b′ p ,
q (inr a) = leaf a .

Example. As an example we define a rudimentary editor. The only command is readchar, which has as result either a character c typed in, cursorleft for the cursor-left-button or terminate for some key associated with termination. The program reads the text created by these keys and returns the result. ((truncate s) will be the result of deleting from string s the last letter, (append s c) an operation which appends at the end of string s character c and “ ” the empty string.)

C = {readchar} : Set ,
R : C → Set ,
R c = {ch c | c : char} ∪ {cursorleft, terminate} .
editor = repeat_{⟨C,R⟩,string} string “ ” λs.do^{+} readchar q ,

where

q (ch c) = leaf (inl (append s c)) ,
q cursorleft = leaf (inl (truncate s)) ,
q terminate = leaf (inr s) .

While-loop. While loops are defined similarly to repeat loops.

while_{w} : (A, B : Set, b : B, p : B → (IO_{w}^{+} B + IO_{w} A)) → IO_{w} A .

The definition proceeds by cases on the value of (p b). If it is of the form (inl q), then q is executed, and, once it terminates with result b′, the program continues with (while_{w,A} B b′ p). If it is (inr q), q is executed and its result returned as final result. The definition, which uses again full recursion, is

while_{w,A} B b p = f (p b) ,
where f (inl q) = q^{−} ∗_{w,B,A} λb′.while_{w,A} B b′ p ,
f (inr q) = q .

It is now an easy exercise to express while by repeat and vice versa.

Redirect. ∗ can be regarded as “horizontal composition” of programs. There is also a “vertical composition”: Assume worlds w = ⟨C, R⟩ and w′ = ⟨C′, R′⟩, A : Set and p : IO_{w} A. We want to refine p to a program in world w′, by replacing every command c : C by a program (q c) in world w′ which has as result an answer r : R c. This suggest q to have type (c : C) → IO_{w′}(R c). However, if we allow (q c) to be a leaf and p has infinitely many commands, this will allow us to construct an expression that cannot be evaluated to constructor form. To avoid this we assume q : (c : C) → IO_{w′}^{+}(R c). The construction that results is

redirect_{w,w′} : (A : Set, p : IO_{w} A, q : (c : C) → IO_{w′}^{+}(R c)) → IO_{w′} A ,
where redirect_{w,w′,A} (leaf a) q = leaf a ,

redirect_{w,w′,A} (do c p) q = (q c)^{−} ∗_{w′,R c,A} λr.redirect_{w,w′,A} (p r) q .

Example. Let the high level world be w_{0} = ⟨C_{0}, R_{0}⟩, with C_{0} = {read} ∪ {write s | s : string}. read should be a command for reading a string, so R_{0} read = string, and (write s) should be an instruction for writing a string, R_{0} (write s) = 1. Let the low level world w_{1} have commands for reading a key, writing a symbol, and movements of the cursor left and right. Let q : (c : C_{0}) → IO_{w_{1}} (R_{0} c), where (q read) is some editor, which uses the keys to define a string and has as result that string, and (q (write s)) be some output routine for strings. (redirect p q) generates a program using basic commands from a program p using the high level commands .

This illustrates that with redirect we have the possibility of building up libraries. In other words, we can define worlds with very complex and powerful I/O-commands and write in the same language programs for transforming these high level programs into those using very basic commands.

Equality. With while− and repeat−loops we introduce non-well-founded I/Otrees. Even with extensional equality it seems that it is no longer possible to prove the monad laws. So extensional equality seems to be too weak for dealing with non-well-founded programs. Instead we use bisimulation as equality. In [3] I. Lindström has given a very elegant definition of such an equality. This equality, transferred to our setting, is defined as ∀n.p ≃′_{w,A,n} q, where p ≃′_{w,A,n} q expresses that p and q coincide up to height n. In the following the world w will be a parameter in all definitions, which we omit for simplicity. We will refer to the equality-types =_{C} and =_{A} on C and A and only identify commands and leaves, which are equal with respect to these equalities. So we do not make use of any user-defined (setoid-)equality on C, A. In a followup to this article, we will consider the generalisation to user-defined equalities.

≃ : (A : Set, p, q : IO A) → Set ,
≃′ : (A : Set, n : ℕ, p, q : IO A) → Set ,
(p ≃_{A} q) = ∀n : ℕ.p ≃′_{A,n} q,
(p ≃_{A,0} q) = ⊤ ,
(leafa ≃′_{A,n+1} do c p) = (do c p ≃′_{A,n+1} leaf a) =⊥ ,
(leaf a ≃′_{A,n+1} leaf a′) = (a =_{A} a′) ,
(do c p ≃′_{A,n+1} do c′ p′) = ∃p : (c =_{C} c′).∀r : R c.p r ≃′_{A,n} p′ (J_{C} R c c′ p r) .

Definition 3.1. (a) Let case-distinction for IO be the rule (under the assumptions that A : Set, B : (p : IO A) → Set):

C_{A,B}^{IO} : ((a : A) → B (leaf a), (c : C, q : R c → IO A) → B (do c q),
p : IO A) → B p .

(b) Let TT(IO) be the extension of the standard type theory used in this article by the defining rules for IO and case-distinction for IO.

Lemma 3.2. TT(IO) proves the following (under the assumptions that A, B : Set, and all other variables are of appropriate type)

(a) ≃_{A} is reflexive, symmetric and transitive.

(b) p ≃_{A} p′ → (∀a : A.q a ≃_{B} q′ a) → p ∗_{A,B} q ≃_{A} p′ ∗_{A,B} q′.

Proof. (a): First we prove the lemma with ≃_{A} replaced by ≃′_{A,n} by induction on n : ℕ, using the elimination rules for equality. Then the assertion follows by the definition of ≃. (b) Show that p ≃′_{A,n} p′ and ∀a : A.q a ≃′_{B,m} q′ a imply do p q ≃′_{B,min{n,m}} do p′ q′ by induction on n. ⊓ ⊔

Theorem 3.3. TT(IO) proves the monad laws with respect to ≃_{A}.

Proof. The first law holds definitionally and a fortiori with respect to ≃_{A}, by its reflexivity. The second and third laws are proved first with ≃_{A} replaced by ≃′_{A,n} using induction on n and case distinction on p. Then the assertion follow from the definition of ≃_{A}. ⊓ ⊔

I/O-trees as a general concept for command/response-interaction. It seems that the applications of I/O-trees, which are in general non-well-founded trees, are not limited only to functional programming languages. I/O-trees cover in a general way command/response-interaction with one agent (a program) having control over the commands. Every I/O-behaviour corresponds, up to the equality we have introduced above, to exactly one I/O-tree. Therefore I/O-trees are suitable models for this kind of interaction.

4 Normalising Version

Counterexample to normalization. If we take standard reduction rules corresponding to the equalities given above, the above definitions give non-norma-lizing programs. Let for instance A = B = C = ℕ, let (R c) be arbitrary, and let w = ⟨C, R⟩, f : ℕ → ℕ. We omit the parameter w.

p := λn.do^{+} (f n) λx.leaf (inl (n + 1)) : ℕ → IO^{+} (A + B) ,
repeat 0 p ⟶ do (f 0) λx.repeat (S 0) p
⟶ do (f 0) λx.do (f (S 0)) λy.repeat (S (S 0)) p
⟶ do (f 0) λx.do (f (S 0)) λy.do (f (S (S 0))) λz.repeat (S (S (S 0))) p
⟶ · · · .

We see that definitional equality is no longer decidable, since we cannot decide whether two functions ℕ → ℕ are extensionally equal. This implies the undecidability of type checking, since with an type checking algorithm we can decide definitional equality (for a, b : A, the term λB, f.f a is of type (B : (x : A) → Set, f : (x : A) → B x) → B b if and only if a and b are definitionally equal). In the following we are going to develop a normalizing variant of the above.

How to regain normalisation. The main idea is to introduce either repeat or while as a constructor, where with while, the definition of ∗ and the proofs of equalities turn out to be easier. One problem is however that while (the same is the case with repeat) defines an element of (IO_{w} A) by referring to (IO_{w} B) for an arbitrary set B. To demand that (IO_{w} A) is a set means to define a set by referring negatively to all sets, which is a problematic definition. (The typing rules require that if A is a set, (IO_{w} A) is a type).

In order to control this we will restrict the sets referred to in while to elements of a universe, which we extend in order to get representatives for 1 + R c.

General assumption and definition 4.1. (a) Let w = ⟨C, R⟩ be a world.

(b) Let U : Set, T : U → Set be some fixed collection of sets (i.e. a universe).

(c) Let set := U + C, el : set → Set, el (inl u) = T u, el (inr c) = 1 + R c, R according to the world w. We write { \atop (1 + R c)} for (inr c).

All the following definitions depend on w, U, and T as parameters, which we however omit for simplicity.

We can now omit the constructor do, since it can be simulated by while.

Definition of IO A.

IO : Set → Set , where (IO A) has constructors
leaf : A → IO A ,
while : (u : set, a : el u, n : el u → (IO^{+} (el u) + IO A)) → IO A ,
and IO^{+} : Set → Set ,
IO^{+} A = Σc : C.R c → IO A .

Monad operations. Now we can define the Monad operations (where sets have to be replaced by elements of the universe)

η_{a}^{A} := leaf a ,
leaf a ∗_{A,B} q = q a ,
while u a p ∗_{A,B} q = while u a (p◯ ∗ _{A,B,u}q) ,
where ◯ ∗ : (A, B : Set, u : set, p : el u → (IO^{+} (el u) + IO A),
q : A → IO B) → el u → (IO^{+}(el u) + IO B) ,
if p b = inl p′, then (p◯ ∗ _{A,B,u}q) b = inl p′ ,
if p b = inr p′, then (p◯ ∗ _{A,B,u}q) b = inr (p′ ∗_{A,B} q) .

Do. We define now the operation (do_{A} c p) (note that do is not a constructor):

do_{A} c p = while { \atop (1 + R c)} (inl •) q ,
where q (inl •) = inl ⟨c, λr.leaf (inr r)⟩ ,
q (inr r) = inr (p r) .

Split. Elements of (IO A) can be regarded as representatives of non-wellfounded trees. We define a function split_{A}, which determines whether a value p : IO A is a leaf labelled by a : A (then split_{A} p = inr a) or represents a program which executes command c and depending on the result r : R c of it executes program q r (then split_{A} p = inl ⟨c, q⟩). In the latter case p represents a tree with root labelled by c and rth subtree being the tree represented by (q r).

split : (A : Set, p : IO A) → (IO^{+} A + A) ,
split_{A} (leaf a) = inr a ,
If p a = inr q, then split_{A} (while u a p) = split_{A} q ,
If p a = inl ⟨c, q⟩, then
split_{A} (while u a p) = inl ⟨c, λr.q r ∗_{el(u),A} λx.while u x p⟩ .

Execution of I/O-programs. Assume a fixed world w_{0} = ⟨C_{0}, R_{0}⟩ corresponding to real commands, as before. execute, adapted to the new setting, operates as follows: Applied to a program p : IO_{C_{0},R_{0}} A it evaluates split_{A} p. If the result is (inr a), then execute stops with result a. If split_{A} p = inl ⟨c, q⟩, then c is executed, and depending on the result r, execute continues with (q r).

Normalising I/O-programs. When using only inductive data types with their elimination rules, the type theory in question is strongly normalising. Therefore, when running execute, at the beginning and after the result of a command is obtained, split_{A} applied to the respective program will always reduce to an element of the form (inr a) or (inl ⟨c, q⟩). However, it might be that infinitely many commands are executed, which is to say that the tree is not necessarily well-founded. We call a program which at the beginning and after the result of a command is obtained, executes the next command after finite amount of time, or terminates, a normalising I/O-program. (IO A) (together with execute) represents a class of normalising I/O-programs.

Equality. Under the same assumptions as in Sect. 3 we can define now an equality on elements of IO A. However, we use split in order to get access to the corresponding tree-structure:

≃ : (A : Set, p, q : IO A) → Set ,
≃′ : (A : Set, n : ℕ, p, q : IO A) → Set ,
(p ≃_{A} q) = ∀n : ℕ.p ≃′_{A,n} q ,
p ≃′_{A,0} q = ⊤ ,
p ≃′_{A,n+1} q = (split_{A} p ≃′′_{A,n} split_{A} q) , where
≃′′ : (A : Set, n : ℕ, p, q : IO^{+} A + A) → Set ,
(inr a ≃′′_{A,n} inl ⟨c, p⟩) = (inl ⟨c, p⟩ ≃′′_{A,n} inr a) =⊥ ,
(inr a ≃′′_{A,n} inr a′) = (a =_{A} a′) ,
(inl ⟨c, q⟩ ≃′′_{A,n} inl ⟨c′, q′⟩) = ∃p : (c =_{C} c′).∀r : R c.q r ≃′_{A,n} q′ (J C R c c′ p r) .

Note that ≃′_{A,n} identifies programs which behave identically in the first n steps, and therefore ≃_{A} identifies exactly behaviourally equal programs. Note however that we only identify commands c : C, which are equal with respect to =_{C}.

Proof of the monad laws, definitional equalities for while and other standard properties. The following can be proved inside type theory. (Some indices or superscripts have been left implicit).

Lemma 4.2. (a) η_{a} ∗ p ≃_{A} p a.

(b) ≃_{A} and ≃′_{A,n} are reflexive, symmetric and transitive.

(c) If p a =_{IO (el u)+IO A} inr q, then while u a p ≃_{A} q.

Proof. (a) is trivial. (b) follows with ≃_{A} replaced by ≃′_{A,n} by induction on n – in case of symmetry and transitivity one uses additionally the elimination rules for =_{C}. From this the assertion follows.

(c) split (while u a p) =_{IO^{+} A+A} split q. ⊓ ⊔

For stating and proving the next lemmata we introduce an equality on the type of p in (while u a p), i.e. (el u) → (IO^{+} (el u) + A):

Definition 4.3.

≃^{w} : (A : Set, u : set,
p, q : (el u) → (IO^{+} (el u) + IO A)) → Set ,
p ≃_{A,u}^{w} q = ∀x : el u.p x ≃_{A,u}^{w,aux} q x , where
≃^{w,aux} : (A : Set, u : set, p, q : IO^{+} (el u) + IO A)
→ Set ,
(inl q ≃_{A,u}^{w,aux} inr q) = (inr q ≃_{A,u}^{w,aux} inl q) = ⊥ ,
(inr q ≃_{A,u}^{w,aux} inr q) = (q ≃_{A} q′) ,
(inl ⟨c, q⟩ ≃_{A,u}^{w,aux} inl ⟨c′, q′⟩) = ∃p : (c =_{C} c′).∀r : R c.
q r ≃_{el u} q′ (J C R c c′ p r) .

Similarly we define ≃^{w}′, ≃^{w,aux}′ with an additional argument n : N and refer to ≃′_{A,n}, ≃′_{el u,n} instead of ≃_{A}, ≃_{el u}.

Lemma 4.4. (a) (p_{0} ≃_{A} p_{1} ∧ ∀a : A.q_{0} a ≃_{B} q_{1} a) → (p_{0} ∗ q_{0} ≃_{B} p_{1} ∗ q_{1}).

(b) p_{0} ≃_{A,u}^{w} p_{1} → while u a p_{0} ≃_{A} while u a p_{1}.

(c) For p : IO A, q : A → IO B, r : B → IO D it follows (p ∗ q) ∗ r ≃_{D} p ∗ λx.((q x) ∗ r).

Proof. We prove (a) – (c), with λx. ≃_{x}, λx. ≃_{x,u}^{w} replaced by λx. ≃′_{x,n}, λx. ≃_{x,u,n}^{′w}, simultaneously by induction on n. The case n = 0 is trivial, so we assume the assertion has been proved for n and prove it for n + 1:

(a) Side-induction on p_{0}, side-side-induction on p_{1}: If p_{0} = leaf a_{0} and p_{1} = leaf a_{1}, then a_{0} =_{A} a_{1} and q_{0} a_{0} ≃′_{B,n+1} q_{1} a_{1}. If p_{0} = while u a p̃_{0} with p̃_{0} a = inr p̂_{0}, then p_{0} ≃_{A} p̂_{0}, and by p_{0} ∗ q_{0} = while u a (p̃_{0}◯ ∗ q_{0}), (p̃_{0}◯ ∗ q_{0}) a = inr (p̂_{0} ∗ q_{0}) it follows p_{0} ∗ q_{0} ≃_{B} p̂_{0} ∗ q_{0}, and the assertion follows by side-IH for p̂_{0} instead of p_{0}. Similarly the assertion follows if p_{1} is of a similar form. Otherwise p_{i} = while u_{i} a_{i} p̃_{i}, with p̃_{i} a_{i} = inl ⟨c_{i}, p̂_{i}⟩,

split p_{i} = inl ⟨c_{i}, λr.p̂_{i} r ∗ λx.while u_{i} x p̃_{i}⟩. By p_{i} ≃_{A,n+1} p′_{i} there exists p_{c_{0}c_{1}} : (c_{0} =_{C} c_{1}), and for

r_{0} : R c_{0}, r_{1} := J C R c_{0} c_{1} p_{c_{0}c_{1}} r_{0} there exist proofs of

p̂_{0} r_{0} ∗ λx.while u_{0} x p̃_{0} ≃′_{A,n} p̂_{1} r_{1} ∗ λx.while u_{1} x p̃_{1}.

split (p_{i} ∗ q_{i}) = inl ⟨c_{i}, λr.p̂_{i} r ∗ λx.while u_{i} x (p̃_{i}◯ ∗ q_{i})⟩

= inl ⟨c_{i}, λr.p̂_{i} r ∗ λx.while u_{i} x p̃_{i} ∗ q_{i}⟩. We have to show that for r_{0}, r_{1} as above p̂_{0} r_{0} ∗ λx.while u_{0} x p̃_{0} ∗ q_{0} ≃′_{n} p̂_{1} r_{1} ∗ λx.while u_{1} x p̃_{1} ∗ q_{1}. By IH (c) and symmetry p̂_{i} r_{i}∗λx.while u_{i} x p̃_{i}∗q_{i} ≃′_{B,n} (p̂_{i} r_{i}∗λx.while u_{i} x p̃_{i})∗q_{i}, and by IH (a) (p̂_{0} r_{0} ∗ λx.while u_{0} x p̃_{0}) ∗ q_{0} ≃′_{B,n} (p̂_{1} r_{1} ∗ λx.while u_{1} x p̃_{1}) ∗ q_{1}. The assertion follows now by transitivity and symmetry.

(b) If p_{i} a_{i} = inr q_{i}, then while u a_{i} p_{i} = q_{i}, q_{0} ≃′_{A,n+1} q_{1}. Otherwise p_{i} a_{i} = inl ⟨c_{i}, q_{i}⟩, split (while u a_{i} p_{i}) = inl ⟨c_{i}, λr.q_{i} r ∗ λx.while u x p_{i}⟩. By assumption there exists p_{c_{0},c_{1}} as in (a) and for r_{0} and r_{1} as in (a) proofs of q_{0} r_{0} ≃′_{el u} q_{1} r_{1}, and furthermore by IH (b) proofs of while u x p_{0} ≃′_{A,n} while u x p_{1} for x : el(u). The assertion follows by IH (a).

(c) is proved by side-induction on p. If p = leaf a this follows by reflexivity. Otherwise p = while u a p̃, (p ∗ q) ∗ r = while u a ((p̃◯ ∗ q)◯ ∗ r), p ∗ λx.q x ∗ r = while u a (p̃◯ ∗ λx.q x◯ ∗ r), by side-IH (p̃◯ ∗ q)◯ ∗ r≃^{w}′_{D,u,n+1}p̃◯ ∗ λx.q x◯ ∗ r, and by (b) for n + 1, as just proved, the assertion follows. ⊓ ⊔

Lemma 4.5. (a) p ∗ λx.η_{x} ≃_{A} p.

(b) split (do c p) =_{IO^{+} A+A} inl ⟨c, p′⟩ for some p′ s.t. ∀r : R c.p r ≃_{A} p′ r.

(c) If p a =_{IO^{+} (el u)+IO A} inl ⟨c, q⟩ then while u a p ≃_{A} do c λr.q r ∗ λx.while u x p.

Proof. (a) follows by straightforward induction on p and Lemma 4.4 (b).

(b) split (do c p) = ⟨c, λr.(leaf (inr r)) ∗ λx.while { \atop (1 + R c)} x q⟩

= ⟨c, λr.while { \atop (1 + R c)} (inr r) q⟩,

where q is as in the definition of (do c p). For r : R c we have by Lemma 4.2 (c) while { \atop (1 + R c)} (inr r) q ≃_{A} p r.

(c) follows by (b) and split (while u a p) = inl ⟨c, λr.q(r) ∗ λx.while u x p⟩.

⊓ ⊔

5 Conclusion

We have identified a need for a general and workable way of representing and reasoning about interactive programs in dependent type theory. We introduced in dependent type theory the notion of an I/O-tree, parameterised over a world, making essential use of type dependency. We gave it in two forms. The first breaks normalisation, but is conceptually simpler and suitable if one is tolerant of a programming language with ‘bottom’, or divergent programs. The second preserves normalisation. We called programs of this kind “normalising I/O-programs”. We introduced an equality relation identifying behaviourally indistinguishable programs and showed that the monad laws hold, modulo this equality. (For the normalising version these are Lemma 4.2 (a), 4.5 (a) and 4.4 (c)). We introduced while-loops in both versions and repeat-loops and redirect in the first version (and leave it as an interesting exercise to extend the last two constructions to the normalising version). In the non-normalising version the characteristic equations for while and repeat are fulfilled by definition, whereas in the normalising version we have shown them for while (Lemma 4.2 (c) and 4.5 (c)). We have characterised do as well in the latter version (Lemma 4.5 (b)).

In a future paper we will show how to move from one universe to another in the normalising version, and will explore the case in which C is a setoid given with a specific equivalence relation. In addition we will introduce state-dependent I/O-programs, in which the set of commands available depends on the current state of knowledge about the world.

Appendix: notations

In the paper we do not distinguish between Σ and Π-type on the logical framework level and as set-constructions. The empty set is denoted by 0, the set containing one element by 1 (with element •). The set of natural numbers is denoted by ℕ. The injections for the disjoint union A + B of sets A and B are written inl : A → (A + B), inr : B → (A + B). The elements of Σx : A.B are denoted by ⟨a, b⟩. The dependent function type (sometimes written as Πx : A.B) is denoted by by (x : A) → B, with abbreviations like (x : A, y : B) → C for (x : A) → (y : B) → C, (x : A, B) → C for (x : A, y : B) → C with y new, and (x, y : A) → B for (x : A, y : A) → B. We use juxtaposition (f a) for application, having a higher precedence than all other operators, so that for example f a = g b means (f a) = (g b). The scope of variable-binding operators λx., ∀x., ∃x., Σx. is maximal (so λx.f a =_{A} b stands for λx.((f a) =_{A} b)). Some functions are represented as infix operators, writing some of the first few arguments as indices. (For instance we write p ∗_{A,B} q for (∗ A B p q).) Arguments which are written as indices are often omitted. We will omit the type in equality judgements, writing r = s instead of r = s : A. An equation sign = without indices denotes definitional equality, whereas we write r =_{A} s (never omitting the A) for equality types (which are actually sets). The intensional equality has elimination rule J : (A : Set, B : A → Set, a, a′ : A, p : (a =_{A} a′), B a) → B a′. Note that with extensional equality J could trivially be defined as λA, B, a, a′, p, b. b.

References

1. L. Augustsson. Cayenne — a language with dependent types. In Proc. of the International Conference on Functional Programming (ICFP’98). ACM Press, September 1998.

2. P. Hancock and A. Setzer. The IO monad in dependent type theory. DTP’99,

http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/dtp99/proceedings.html, 1999.

3. I. Lindström. A construction of non-well-founded sets within Martin-Löf’s type theory. Journal of Symbolic Logic, 54(1):57–64, 1989.

4. P. Martin-Löf. Constructive mathematics and computer programming. In J. L. Cohen, J. Łos̀, H. Pfeiffer, and K.-D. Podewski, editors, Proceedings 6th Intl. Congress on Logic, Methodology and Philosophy of Science, Hannover, FRG, 22–29 Aug 1979, pages 153–175. North Holland, Amsterdam, 1982.

5. E. Moggi. Notions of computation and monads. Information and Computation, 93(1):55–92, 1991.

6. B. Nordström, K. Petersson, and J. M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990.

7. S. L. Peyton Jones and P. Wadler. Imperative functional programming. In 20’th ACM Symposium on Principles of Programming Languages, Charlotte, North Carolina, January 1993.

8. P.N.Benton, G.M.Benton, and V.C.V.de Paiva. Computational types from a logical perspective. J. Functional Programming, 8(2):177–193, January 1993.

9. P. Wadler. The essence of functional programming. In 19’th Symposium on Principles of Programming Languages, Albuquerque, volume 19. ACM Press, January 1992.

10. P. Wadler. Monads for functional programming. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS. Springer Verlag,