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, SE-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. 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/Otrees represent strategies for one of the parties in a command/response interaction – the notion is not confined to functional programming. We present I/O-trees in two forms. The first form, which is simpler, is suitable for Turing-complete functional programming languages with general recursion, but is non-normalising. 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. Most definitions in this article make essential use of the expressive strength of dependent typing.

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. Some 20 years ago, Martin-Löf [6] suggested that his type theory, originally a framework for constructive mathematics, could be considered as a programming language, and his suggestion has been taken up and explored in a number of ways (see for example [9]). A question which seems to have received little attention is the form of the inputoutput interface of such programs. Indeed it is only in the last 10 years that this question has been satisfactory answered in the context of conventional functional programming, through the efforts of Moggi [8], Wadler [13], and others.

Dependent types give us the ability to express with full precision any extensional property of a program, which can be defined mathematically. For example, we can express the requirement for a function which maps lists to sorted lists using a dependent type [9]. Remarkably, with certain provisos of largely academic interest, we can still check the type of a program mechanically, and typecorrectness carries full assurance that it satisfies its specification. In the past few years, implementations of dependent type systems for functional programming have begun to appear [1]. So far however the implications of dependent types for specification of interfaces and programs have not been examined.

Conventions, and plan of paper. In the following, we will work in a standard dependent type theory (for example [9]) with the usual introduction and elimination rules, including 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 explain why one needs a model of interaction in type theory, and recall the approach taken in 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 or redirection construction. In the fourth, we point out that the repetition constructs 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 the result of applying the function to its input. This batch model is adequate for a large class of programs, typically 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 one is ordinarily confronted with interact with their environment while they are running. We give input via devices like keyboard or microphone and get output via devices like monitor or loudspeaker, and this inputoutput cycle is repeated again and again. Programs may also interact with the file system, the network or via 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 [10]: dialogues (or lazy streams), continuations, and monadic I/O. Mention should also be made of the ‘uniqueness types’ of the language Concurrent Clean^{1}. In this paper we follow the monadic approach, introduced by E. Moggi [8], 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

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

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 a given equivalence relation =. (Instead of η A a we will write η_{a}^{A}).

η_{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 that may or may not terminate, but terminate only with a result a of type A.

(b) The program p ∗ q first executes p. If p terminates with result a, then the program continues with (q a). The result of the whole program is the result of (q a).

(c) The program η_{a} simply terminates with result a, without any interaction.

Additionally, one adds functions for specific interactions. 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 that outputs s on some device and returns •, and read : IO String is the program that reads a string and returns it.

For the reader unfamiliar with type checking programs written using an I/Omonad, it is worth stressing that type checking interactive programs does not require itself any interaction, since we type check the programtext.

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

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

The I/O-monad seems to be the most promising approach for the representation of interactive programs within dependent type theory. To add it as a new concept would however involve adding besides new typing judgements also new judgement level equations for the monad laws. This is more than the relativisation of type theory to a context of typed variables. The implications of this for the metamathematical properties of type theory are unclear to the authors.

Since we have access to powerful data type constructions in type theory, an easier approach is to define the I/O-monad and derive the monad laws directly in type theory. We still need something beyond mere evaluation of expressions, namely the ability to actually run an I/O-program. However we can use elimination rules for modifying I/O-programs and we shall make substantial use of it in the following. Note that for efficiency reasons one might implement the execution of I/O programs in a different way, using for example a continuation monad with an ‘answer’ type of I/O programs. The paper [4] describes some of the options one has for implementing datatypes such as monads.

2 I/O-Trees

Worlds. Interactive programs are built from interactive commands. In dependent type theory we can define such sets of interactive commands in a very general way, parameterise over them and switch between command sets.

Let C be a set of instructions or commands. These include commands to obtain input, commands to produce output, and commands with a mixed effect. For commands c : C let (R c) be a type of responses produced when command c has been performed. ⟨C, R⟩ will be called a world:

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.

Examples for constructors of C might be

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

(b) read : C, with (R read = String): read a string and return 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. We might as well have commands for interaction with file systems, network etc.

I/O-trees. We want to define the I/O-monad as a data type constructed in type theory. It seems particularly suitable to define it as an inductive data type, because we can then carry out program transformations using the elimination rule associated with such types. A naïve idea 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 that the naïve approach would require 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 or ‘jump table’ of programs depending on the result of performing that instruction, and creates a new program that begins by issuing this instruction and then, when the instruction has been performed, 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. So we have the following rules for IO_{w} A:

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 issues the command c, and depending on the result r : R c returned by the environment continues with (p r). Note that (IO_{w} A) is now parameterised with respect to w, a feature expressible only with dependent types.

(IO_{w} A) is the set of well-founded I/O-trees with leaves in A and inner nodes labelled by some c : C and with branching degree (R c) (ie. the subtrees of that node are indexed over (R c)). (IO_{w} A) is a near variant of the “W-type” in standard type theory: The type expression Wx : A.B denotes the type of wellfounded trees with nodes labelled by elements a : A and having then branching degree B[x := a], see [9, pages 109–114]and [7, pages 79–86] for details. In proof theory, the W-type turns out to be a very powerful construction: see [11]

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 that executes a term denoting 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 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. So through successive interactions we trace out a descending chain through the tree p.

A first example. In the following example we assume commands readstr and (writestr s) for reading and writing strings and a Boolean valued equality =_{String} on strings. The following program prompts for the root-password. If the user types in the right one (“Wurzel”^{3}) the program terminates successfully, otherwise

3 This really happened.

it responds with “Login incorrect” and 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 =_{String} “Wurzel” then leaf success else do (writestr “Login incorrect”) λa. leaf fail

: IO { success, fail } .

η, ∗. It is now easy to define η and ∗ and verify the monad laws for well-founded trees with extensional equality (by [4] this is not the most efficient solution):

η_{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) .

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 forever. 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.

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 has result (inl b′), then the program continues with (repeat_{A} B b′ p). If it has result (inr a), the program terminates and returns a.

However, if p b = leaf a for some b : B, we might get an expression that does not evaluate to constructor form, e.g. (repeat_{B} b λx.leaf (inl b)). So we have to restrict p, and the easiest way 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 at least one interaction (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 general recursion and so allows us to define nonwell-founded trees and form non-normalising terms) of repeat 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 done for some key associated with termination. The program reads the text created using these keys and returns the result. ((truncate s) will be the result of deleting the last character from string s, (append s c) an operation which appends character c to the end of string s, and “ ” the empty string.)

C = {readChar} : Set ,
R : C → Set ,
R c = {ch c | c : Char} ∪ {cursorLeft, done} .
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 done = 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 general 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′ with a result r : R c. So q has 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 replace the type of q by (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 .

Using redirect for building libraries. We can now define a world in which high level I/O-commands are first class objects – they do not evaluate directly into low level commands – together with an interpretation of each command as a program in the basic language used by execute, and so construct libraries. To implement execute one can therefore restrict oneself to a basic world with simple commands.

Example. Let the high level world be w_{0} = ⟨C_{0}, R_{0}⟩, with C_{0} = {read} ∪ {write s | s : String}. Here read is a command for reading a string, R_{0} read = String, and (write s) 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 an editor that uses the keys to manipulate a string and has as result that string, and (q (write s)) is an output routine for strings. Then (redirect p q) translates a program using high level commands into one that uses the basic ones.

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. (We do not yet have a proof of this.) So extensional equality seems to be too weak for dealing with non-well-founded programs. Instead we use bisimulation as equality. In [5] I. Lindström has given a very elegant definition of such an equality. The definition is based on an idea that occurs in work on non-wellfounded sets by Lars Hallnäs [2]. Transferred to our setting, the equality 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, and will be omitted for clarity. We will use equality-types =_{C} and =_{A} on C and A. (We will in a follow-up to this article consider a generalisation where instead of assuming =_{C} we establish C with a setoid structure; in this case we need a reindexing map, which replaces J_{C}R below. Additional reindexing maps will be needed to establish the properties of the equality which we define.)

≃ : (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′) = ∃x : (c =_{C} c′).∀r : R c.p r ≃′_{A,n} p′ (J_{C} R c c′ x 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 (intensional) Martin-Löf type theory extended 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 by reflexivity therefore with respect to ≃_{A}. The second and third laws are proved first with ≃_{A} replaced by ≃′_{A,n} by induction on n. Then the assertion follows 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 normalisation. If we take standard reduction rules corresponding to the equalities given above (by directing the equations in an obvious way), the above definitions give non-normalising programs. Let for instance A = B = C = ℕ, (R c) be arbitrary, 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 now undecidable, 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 = b : A).

One solution would be to extend dependent type theory by coinductive types with rules chosen such that normalisation is preserved. This requires extensive meta-theoretical investigations that have not yet been completely carried out. Instead we represent non-well-founded trees in normalising standard type theory.

How to regain normalisation. In type theory with inductive types and standard elimination rules for them, while and repeat cannot be defined. We can however add one of them as a constructor to (IO_{w} A). We choose while, for which the definition of ∗ and the proofs of equalities turn out to be easier. We can then define repeat by using while. We modify execute, so that it operates on (while u a p) in the same way as it operated on the non-well-founded trees defined using the function while in the previous version. 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 problematic. (The typing rules require that if A is a set, (IO_{w} A) is a type).

To fix this, we will restrict the sets referred to in while to elements of a universe. A universe is a set-indexed collection of sets, ie. a pair ⟨U, T ⟩ s.t. U : Set and T : U → Set. The elements of U represent “small sets”. With such a restriction (IO_{w} A) no longer refers to the collection of all sets, and can now be typed as a set. We will however extend U to a slightly bigger universe with representatives for 1 + R c, and this extension will be called set, since it is in the definition of (IO_{w} A) the “collection of small sets”.

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).

For simplicity, in the following we will omit the parameters w, U, and T. We can now omit the constructor do (which can be simulated by while) and

obtain the following 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. In the monad operations 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. Now we define 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. In the non-normalising theory, each element of (IO A) according to the new definition can be interpreted as a non-well-founded tree; we replace all occurrences of the constructor while with the function while defined before. In normalising type theory this is not possible. Instead we can obtain the structure of the represented non-well-founded trees by defining a function split_{A}, which determines for every p : IO A whether its interpretation as a non-well-founded tree is that of a leaf labelled by a : A (split_{A} p = inr a) or whether it is an inner node labelled by c : C, which has for r : R c subtree q r (split_{A} p = inl ⟨c, q⟩):

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. With only inductive data types with their elimination rules, type theory is normalising. Therefore split_{A} q reduces to a value of the form (inr a) or (inl ⟨c, q⟩). So when a program is executed, and it is its ‘turn to go’ (ie. at the beginning and after obtaining a response to a command), after a finite time, either it terminates, or it issues another command. (Whether a response to a command c is obtained after a finite time depends firstly on whether a response is even possible – the response set R c may be empty – and secondly on what happens in the real world – the user may walk away from the keyboard and never return.) However, it may still be that infinitely many commands are executed. As trees, I/O-programs are not necessarily well-founded. We call an I/O-program normalising if both initially and after the result of a command is obtained, it either terminates, or issues the next command after a finite amount of time. The set (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 identify only those commands c : C which are equal with respect to =_{C}.

Proof of the monad laws, defining equalities for while and other standard properties with respect to bisimulation. 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 explore what happens if C is a setoid with a specific equivalence relation. In addition we will introduce state-dependent I/Oprograms, 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 (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 do, 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 that 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 introduction rule ref : (A : Set, a : A) → a =_{A} a expressing reflexivity, and elimination rule J : (A : Set, B : A → Set, a, a′ : A, p : (a =_{A} a′), B a) → B a′, which corresponds to the second equality axiom: from a =_{A} a′ and B a we can conclude B a′. The equality rule is J_{A} B a a ref_{a}^{A} b = b. Note that with extensional equality J could be defined trivially 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. L. Hallnäs. An intensional characterization of the largest bisimulation. Theoretical Computer Science, 53:335–343, 1987.

3. 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.

4. J. Hughes. The design of a pretty-printing library. In J. Jeuring and E. Meijer, editors, Advanced Functional Programming, volume 925 of LNCS, pages 53–93. Springer, 1995.

5. 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.

6. 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.

7. P. Martin-Löf. Intuitionistic Type Theory, volume 1 of Studies in Proof Theory: Lecture Notes. Bibliopolis, Napoli, 1984.

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

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

10. 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.

11. A. Setzer. Well-ordering proofs for Martin-Löf type theory. Annals of Pure and Applied Logic, 92:113 – 159, 1998.

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

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