Interactive Programs and Weakly Final Coalgebras in Dependent Type Theory

(Extended Version)

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

1 Department of Computer Science University of Wales Swansea Singleton Park Swansea SA2 8PP, UK.

                    a.g.setzer@swan.ac.uk

2 7 Cluny Avenue, Edinburgh EH10 4RN, UK.

                     hancock@spamcop.net

Abstract. We reconsider the representation of interactive programs in dependent type theory that the authors proposed in earlier papers. Whereas in previous versions the type of interactive programs was introduced in an ad hoc way, it is here defined as a weakly final coalgebra for a general form of polynomial functor. The are two versions: in the first the interface with the real world is fixed, while in the second the potential interactions can depend on the history of previous interactions. The second version may be appropriate for working with specifications of interactive programs. We focus on command-response interfaces, and consider both client and server programs, that run on opposite sides such an interface. We give formation/introduction/elimination/equality rules for these coalgebras. These are explored in two dimensions: coiterative versus corecursive, and monadic versus non-monadic. We also comment upon the relationship of the corresponding rules with guarded induction. It turns out that the introduction rules are nothing but a slightly restricted form of guarded induction. However, the form in which we write guarded induction is not recursive equations (which would break normalisation – we show that type checking becomes undecidable), but instead involves an elimination operator in a crucial way.

Keywords: Dependently typed programming, interactive programs, coalgebras, weakly final coalgebras, coiteration, corecursion, monad

⋆ Supported by Nuffield Foundation, grant ref. NAL/00303/G and EPSRC grant GR/S30450/01.

1 Introduction

According to Martin-Löf [19]:

“… I do not think that the search for logically ever more satisfactory high level programming languages can stop short of anything but a language in which (constructive) mathematics can be adequately expressed.”

The reason offered is that the programmer thereby gains access to the entire conceptual apparatus of constructive mathematics, in a form in which the correctness of programs (formed according to the rules of a such a language) can be automatically checked.

What is the benefit of “the entire conceptual apparatus of constructive mathematics” to a programmer? Does it mean we can write more programs? On the contrary, the restriction to a language in which programs are normalising means there will be programs we will not be able to write, in comparision with languages which are Turing-complete. Some of them we may even want or need to write. To make that possible the language will need to be extended with rules for more powerful mathematical principles. No such extension can be once-and-for-all.

Programming isn’t just writing code. If only it were: then we could all become superb programmers by learning to type quickly and more accurately. It is of course the problem of figuring out what code to write. If the relation between programs and specifications is essentially the ‘∈’ or ‘:’ of the typing judgement a : A, then programming is as much or more concerned with the right hand side of the :’ as it is with its left, and it is here that the real benefit lies of access to the conceptual apparatus of contructive mathematics. It lets us express and work with the specification of programs with mathematical precision.

Nowadays these points are more widely appreciated than in the late 70’s. Indeed, one may feel that they amount to a recitation of platitudes. Our feeling is that on the contrary there are implications in the conception of programming as an application of constructive mathematics which remain very much underappreciated. Here we want to draw attention to the interaction of programs “with the outside world”, as in for example the control of machinery. The general issue is input/output, and how to benefit from access to the conceptual apparatus of constructive mathematics in developing programs that do the right thing.

Naïvely conceived, programs developed in dependent type theory are not interactive. They are functions that receive one or more arguments as input, and return a single value as output or result. Indeed, in the paper by Martin-Löf cited above, inputs and outputs are explicitly correlated with arguments and values of functions. This view of program execution as consisting of a single step of interaction is perhaps appropriate for batch programming, prevalent in the 60’s and 70’s. At that time a job was submitted to the computer, typically consisting of some numerical computation on prepared data, and the results printed or stored in a file.

Nowadays one expects programs to be interactive. A running program should receive input from external devices (e.g. keyboard, mouse, network or sensors), and in response send output to external devices (e.g. display, sound card, network, actuators). This cycle should repeat over and over again, as often as required, perhaps forever.

The chief interest of dependent type theory for programming is not merely that it is a programming language, but rather that it is a framework for specifying and reasoning about programs. It is therefore necessary to understand how to develop interactive programs in dependent type theory. We hope to use it to develop verified interactive programs, assisted by automatic type-checking.

In this article we explore one approach to the representation of interactive programs in dependent type theory. This approach takes as its starting point the notion of “monadic IO” ([21]) used in functional programming. We shall see that in dependent type theory, besides non-dependent interactive programs in which the interface between the user and the real world is fixed as in ordinary functional programming, there is a natural notion of state-dependent interactive program, in which the interface changes over time, and depends on the history of interactions. The representation is based on a structure identified by Petersson and Synek in [24]. The structure, which can be seen as a generalisation of the ‘W-type’ that has received so much attention recently, is rich in applications.

We shall see that the representation of interactive programs is closely connected with the weakly final coalgebras for certain specific functors. This notion will then be generalised to coalgebras for general polynomial functors.

We introduce here an extension of Martin-Löf type theory by new rules, for weakly final coalgebras. There is ongoing work on encoding weakly final coalgebras in standard intensional Martin-Löf type theory. However, because it seems likely that reasoning about final coalgebras will be important in the future, we believe that it is natural to have them as “first class”, directly-represented objects, as given by our rules. We shall see that a restricted form of guarded induction (where there is exactly one constructor on the right hand side and where reference can be made only to the function one is defining and not to elements of the coalgebra defined previously) is in exact correspondence with coiteration. Finally we will show that bisimulation is a state-dependent weakly final coalgebra.

Other approaches to interactive programs in dependent type theory.

As pointed out to us by Peter Dybjer, in a certain sense one can use an expression with an algebraic data type as an interactive program. First one brings the expression to constructor form. (The reductions considered by Martin-Löf reduce a term only to weak head normal form.) Then one can “peel away” the constructor, choose one of its operands, and reduce it further. To use the expression as an interactive program, one associates with each constructor some action upon the world, and with each response or output forthcoming from that action a selector, that determines an operand of the constructor. For instance, 2 + 3 reduces to S(2 + 2), and one can then decide to investigate the argument 2 + 2 further and find that 2 + 2 reduces to S(2 + 1) etc. These successive reductions gives rise to a sequence of (trivial) interactions: handing over a coin to a shop-keeper for example, and waiting for an acknowledgement. Or, if one defines B : {0, 1} → Set, B 0 = ∅, B 1 = ℕ, C := Wx : {0, 1}.B x, and starts with an element c : C, then c reduces to the form sup a f. In the case a = 1 one can apply f to an externally given natural number in order to obtain another element of C, and so on; in the case a = 0 no response is possible, and the process comes to an end. Note that the process of interpreting a constructor as a command or action, peeling off the constructor and using the response to select an operand with which to continue is not an operation within type theory, but an extra-mathematical application of type theory. However, in order to obtain strong normalisation and therefore decidable type checking (one might of course obtain decidable type checking without having strong normalisation) one usually requires that types are well-founded, entailing that such a sequence of interactions will necessarily terminate eventually with some constructor without operands. So nonterminating sequences of interactions are impossible. For this reason, if we are not content merely to model terminating interactive programs, we need to consider coalgebras rather than algebras.

Related work. H. Geuvers has introduced in [6] rules for inductive and coinductive types corresponding to corecursion in the context of the simply typed λ-calculus and in the context of system F. He showed that the resulting systems are strongly normalising. E. Gimenéz ([7]; see as well the book on Coq [2], chapter 13, for an exposition of the coalgebraic data types in Coq, which are based on the work by Gimenéz) has studied guarded recursion for weakly final coalgebras and a corresponding general recursive scheme for initial algebras in the context of Coq. He showed that the definable functions are extensionally the same as those definable by the rules given by Geuvers. However, interactive programs are not studied in their work, nor do they investigate in depth the formation/introduction/elimination/equality rules in the context of Martin-Löf type theory. What is not obvious in the work by Gimenéz is that not only can guarded induction be interpreted using the rules for weakly final coalgebras, but in fact the rules for weakly final coalgebras are exactly those arising from a slightly restricted form of guarded induction. Furthermore, the syntax used by Gimenéz seems to suggest that when one introduces recursive functions by guarded induction, it is only lazy evaluation which prevents their complete reduction. On the other hand, when looking at the rules one realises that this is not the case, and the evaluation of these functions is driven by applying case distinction to an element of the coalgebra, corresponding to our elim-function discussed below.

The problem of representing final coalgebras in type theory was addressed in the special case of of Aczel’s non-well-founded sets by Lindström in [16], who gave a representation using an inverse-limit construction that requires an extensional form of type theory. Markus Michelbrink is working on an encoding of weakly final coalgebras in standard intensional Martin-Löf type theory, i.e. on introducing sets representing the weakly final coalgebras and functions corresponding to those given by the introduction and elimination rules such that the equalities given by the rules hold w.r.t. bisimilarity rather than definitional equality.

Notations and type theory used. In this article we work in standard Martin-Löf type theory, based on the logical framework with both dependent pair and function types. Apart from the sets introduced by rules added to type theory in this article, we use the constructs of the logical framework (including Set) extended by the finite sets, the set of natural numbers, the disjoint union of sets and the set of proofs of identity between a pair of elements of a given set.

Dependent functions We write (x : A) → B for the type of dependent functions f, where f takes for its argument an a : A and returns an element f(a) of type B[x := a]. This type is the logical framework version of the dependent function type denoted by Πx : A.B – the difference is that for (x : A) → B the η-rule is postulated at the level of judgemental equality, whereas for Πx : A.B it holds rather at the level of propositional equality. We write λx.s for the function f taking argument a and returning s[x := a]. If for x : A we have s : B, then λx.s : ((x : A) → B). We write λx, y.s for λx.λy.s. We write f(a) for application of f to a, f(a, b) for the application of f to a and b, and similarly for longer sequences of applications.

Dependent pairs We write (x : A) × B for the dependent product. The elements of this type are pairs ⟨a, b⟩ where a : A and b : B[x := a]. We write π_{0}(a) and π_{1}(a) for the first and second projection of an element of this type. (x : A)×B is the logical framework version of the type Σx : A.B – again the difference is that with (x : A) × B we postulate the η-rule at the level of judgemental equality, whereas with Σx : A.B it holds rather at the level of propositional equality.

If f : A → B and g : A → C, we overload the pairing notation to and define ⟨f, g⟩ : A → B×C as the function such that ⟨f, g⟩(a) = ⟨f(a), g(a)⟩. Furthermore we usually write ⟨a, b, c⟩ for ⟨a, ⟨b, c⟩⟩, and similarly for longer sequences.

Bracketing and variable conventions We write (x : A, y : B) → C for (x : A) → ((y : B) → C), and (x : A) × (y : B) × C for (x : A) × ((y : B) × C)), similarly for longer chains of types. Sometimes we assign a variable to the last set in a product, e.g. (x : A) × (y : B) × (z : C) although z is never used.

We omit variables which are not used from products and function types (e.g. (x : A, B, z : C) → D instead of (x : A, y : B, z : C) → D, where C, D don’t depend on y), and write A → B and A × B instead of (x : A) → B and (x : A) × B, respectively, where B does not depend on x.

Binary disjoint unions If A, B : Set then A + B : Set is the disjoint union of A and B with constructors inl : A → (A + B) and inr : B → (A + B). If f : A → C and g : B → C, then we define [f, g] : (A + B) → C as the function such that [f, g](inl(a)) = f(a), [f, g](inr(b)) = g(b). Furthermore we usually write A_{0} +A_{1} +⋯+A_{m} instead of A_{0} +(A_{1} +⋯+(A_{m−1} +A_{m})). In connection with this type, we write in_{i}^{m} for the injection from A_{i} into A_{0} + ⋯ + A_{m}. If X and Y are predicates over a set S (i.e. X, Y : S → Set), we occasionally use the notation X+_{S}Y for the function with type S → Set defined by (X+_{S}Y)(s) = X(s)+Y (s). For f_{i} : (s : S) → A_{i}(s) → B(s) we define f_{0} +_{S} f_{1} : (s : S) → (A_{0} +_{S} A_{1})(s) → B(s) by (f_{0} +_{S} f_{1})(s, inl(a)) = f_{0}(s, a), (f_{0} +_{S} f_{1})(s, inr(a)) = f_{1}(s, a).

Standard finite sets ∅ : Set denotes the empty set, with elimination rule efq_{A} : (x : ∅) → (A x) for any function A : ∅ → Set. We usually omit the index A of efq. 1 : Set denotes the set with has sole element ∗ : 1. We assume the η-rule for 1, so we have that if x : 1, x = ∗ : 1. 2 denotes the set with the two elements ∗_{0} and ∗_{1}. It can of course be defined to be 1 + 1, where ∗_{0} := inl(∗) and ∗_{1} := inr(∗).

We frequently refer to the set 1 + C (in Haskell called Maybe(C)), and in connection with this set, write inl instead of inl(∗). (See also [23, pp103–104], where another notation is used for the same construct.)

Identity For convenience we usually work in extensional type theory, although many (though not all) proofs can be carried out in intensional type theory. We write Id(A, a, b) for the equality type expressing equality of a : A and b : A. The canonical element of Id(A, a, a) will be called refl_{A}(a). When the overhead is not too great, we make basic definitions in intensional type theory. Then we use J for the transfer principle derived from the elimination rule, where J : (C : A → Set, a : A, b : A, x : Id(A, a, b), C(a)) → C(b), and J(C, a, a, refl_{A}(a), c) = c.

The type of sets Apart from the type constructions above, we have one additional type, the type of small types called Set. Elements of Set are types, a la Russell. The type Set will be closed under all type constructions mentioned in this section (including the function type and product), except for Set itself. It may be that we have (somewhere) defined set-valued functions over a given set by an elimination principle. This can be handled by assuming suitable universe set.

2 Non-dependent Interactive Programs

We have studied two main approaches taken in functional programming languages that allow interactive programs to be written. (For an overview of I/O in functional programming, see [9].)

– Constants whose evaluation has side effects.

– The IO-monad, as used in Haskell.

Constants with side effects are used for instance in ML and Lisp. Gordon draws attention to some of the difficulties of this approach in [9, section 7.1]. However, in dependent type theory there are even more problems. In dependent type theory expressions are evaluated during type checking. For example, if a, a′ : A, then the term λB, x.x is of type (B : A → Set) → B a → B a′ if and only if a and a′ are equal elements of type A, which is to say that a and a′ evaluate to the same normal form. If there were constants with side effects, the evaluation of a might trigger interactions with the real world. The type correctness of the program might (bizarrely) depend on the results of these interactions.

The idea underlying the IO-monad, as it is used in Haskell, is to distinguish a program as a static, mathematical structure from a computation guided by such a structure. The program is used to determine the next interaction, on the basis of previous interactions. Performing an interaction is an external, or extra-mathematical operation, carried out in a loop. Suppose that zero or more interactions have already been performed, and responses to those interactions have been received. Then, using this structure, the next interaction is calculated and performed in the real world. Once a response is obtained the loop is repeated, with a further interaction appended to the history of interactions This idea was the basis for our articles [14, 13, 15], and we repeat the key ideas in the following, following mainly [13]. In this paper, for simplicity we don’t say much about the specifically monadic nature of IO (which pivots around “result types”).

In [13], an atomic interaction starts with the interactive program issuing a command in the real world (e.g. to write a character to the screen, or to return a code of the next key pressed by the user). In response to a command the real world returns an answer. For example if the command was to write a character on the screen, the answer is an acknowledgement message; if the command was to get a key pressed, the answer is a code of the key. Once the answer is obtained, the atomic interaction is finished, and the program continues with the next atomic interaction.

In type theory, we can represent the set of commands as a set C : Set. The set of responses that can be returned to a command c : C is represented as a set R(c) : Set. The interface of an interactive program with the real world is therefore represented by a pair ⟨C, R⟩, which is an element of

Interface^{nondep} := (C : Set) × (R : C → Set)

(In [13] we used the terminology “world” instead of “interface”. We now think that the new terminology is more appropriate.) In the following, when referring to non-dependent programs, we assume a fixed interface ⟨C, R⟩.

The set IO. To run an interactive program p appropriate to the interface ⟨C, R⟩, we need the following ingredients.

– We need to determine from p the command c : C to be issued next, by calculating the normal form of p.

– For every possible response r : R(c) to c we need to determine a continuation program q. When the atomic interaction initiated by issuing the command c is complete, the interactive program should continue with the interactive program q.

Let IO : Set be the set of interactive programs – we will see below how to actually introduce this set and the associated functions elim and Coiter in type theory. Note that we suppress here the dependence of IO on the interface. (The same will apply to other operations like elim.) Then we need a function c : IO → C determining the command to issue and a function next : (p : IO, R(c(p))) → IO that determines the next program from the response. We can combine both ingredients into one function

elim : IO → ((c : C) × (R(c) → IO)) .

Define

F : Set → Set , F(X) := (c : C) × (R(c) → X) .

Then elim : IO → F(IO) .

If we have p : IO, then execution of the program proceeds as follows. First, we compute elim(p) = ⟨c, f⟩, and issue the command c. When we have obtained a response r : R(c) from the real world, we compute the new program f(r) : IO. This cycle with its two phases of computation and interaction is repeated with f(r), i.e. we compute elim(f(r)), issue the relevant command, receive a response which we use to determine the next element of IO to be performed, and so forth.

The process terminates if and when one reaches an element p : IO which has associated with it a command c such that R(c) = ∅. This means that no response by the real world is possible. It can also happen that the program “hangs”, or waits forever for a response because the real world never provides a response to a command, although there are possible responses.

Note that execution of interactive programs need not terminate. Consider for instance an editor or word-processor. There is no a priori bound on the length of an editing session. On the other hand, there are situations in which one wants to enforce termination of interactive programs. Consider for instance a program that writes a file to a disk. There will be several interactions with the disk, during which blocks of data are written to different sectors on the disk and information about their location is stored in the directory structure of the disk. In this case one expects that this process terminates after a certain amount of time, so it is natural to demand that only finitely many interactions are possible. In general many functions of an operating system, especially those controlling interactions with hardware, are of this kind.

Introduction of Elements of IO. One could describe an interactive program as a labelled tree: the nodes are labelled by commands c : C and a node with label c has immediate subtrees indexed by r : R(c). When performing the corresponding program, one would start by issuing the command at the root. Then one would, depending on the response of the real world r, move to the subtree with index r, issue the command which is given as label of that node, and having received response r′, move to the r′th subtree and so forth.

In type theory, it turns out to be technically simpler to omit two properties of trees, firstly that each node is reached at most once, and secondly that each node is reached at least once. If one omits these two conditions, then an interactive program is introduced by

– an X : Set, corresponding to the nodes of the tree, – a function which associates with each node x : X the command c : C to be

issued when control has reached that node and for every r : R(c) the node from which the program should next continue having received the response r,

– the initial node of the tree x : X, with which the program starts.

This means that elements are introduced by a triple ⟨X, f, x⟩ where X : Set, f : X → ((c : C) × (R(c) → X)) and x : X. Note that f : X → F(X). So the introduction rule for IO is that we have a constructor

Coiter : (X : Set, f : X → F(X)) → X → IO

(The name Coiter, which stands for coiteration, will be explained in Sect. 8. The principle of coiteration is well-known in the area of coalgebra theory.)

Bisimilarity. Two programs p, q : IO behave in the same way, if firstly they issue the same command, and secondly when supplied with the same response, they continue with programs which again issue the same command, and so on. The equivalence relation which holds between programs that behave in the same way is (as is well-known) bisimilarity.

In our setting, bisimilarity can be defined as follows: A bisimulation relation is a relation B ⊆ IO × IO, such that for every p, p′ : IO, if B(p, p′) holds and elim(p) = ⟨c, n⟩ and elim(p′) = ⟨c′, n′⟩, then there exists a proof cc′ : Id(C, c, c′) and for r : R(c) we have B(n(r), n′(r′)), where r′ : R(c′) is obtained from r : R(c) using the transfer principle, i.e. r′ = J(λd.R(d), c, c′, cc′, r).

If there is a bisimulation relation between p and p′, then p and p′ obviously exhibit the same behaviour. Conversely, if p and p′ behave in the same way, then one can obtain a bisimulation relation, namely the one which identifies q and q′ if and only if q is a descendant of p and q′ is the corresponding descendant of p′. Therefore two interactive programs p and p′ behave in the same way if and only if there exists a bisimulation relation B such that B(p, p′) holds.

Let B be the union of all bisimulation relations. Then B is called bisimilarity. It is a bisimulation relation, and moreover it is the largest one, since it contains any other bisimulation relation. We write p ≈ p′ for B(p, p′), and will show below how to define ≈ in type theory.

Equalities and weakly final coalgebras. When we introduce IO in type theory, we want the following equality to hold. Assume X : Set, f : X → F(X) and x : X. Assume f(x) = ⟨c, g⟩ where g : R(c) → X. Then elim(Coiter(X, f, x)) = ⟨c, λr.Coiter(X, f, g(r))⟩. In other words, if an element x in X has associated with it a command c and a function that for any r : R(c) returns x_{r}, then the corresponding IO-program should have associated with it the same command c and, depending on r should return the program associated with the next node x_{r} : X, which is Coiter(X, f, x_{r}).

We can extend F to a functor Set → Set, whose action on morphisms f : X → Y gives function F(f) : F(X) → F(Y), where F(f, ⟨c, g⟩) := ⟨c, λr.f(g(r))⟩. The functor laws however hold only with respect to extensional equality.

With this extension, we can see that IO together with elim will be a weakly final coalgebra for F : Set → Set^{1}.

That (IO, elim) is a coalgebra means that elim : IO → F(IO). That it is weakly final means that for every other coalgebra (X, f), where X : Set and f : X → F(X), there exists an arrow Coiter(X, f) : X → IO such that elim ∘ Coiter(X, f) = F(Coiter(X, f)) ∘ f:

X  F(X)

IO  F(IO) Coiter(X, f) elim f F(Coiter(X, f))

We do not demand uniqueness of the arrow Coiter(X, f). If we had uniqueness of this arrow, then (IO, elim) would be a final coalgebra for F. We don’t know whether there are rules which can be considered to formulate the existence of final coalgebras in intensional dependent type theory – the usual principles imply that bisimilarity is equality, which implies extensionality of the equality on N → N.

3 Dependent Interactive Programs

Dependent Interactive Programs. In the preceding section we haven’t fully exploited the power of dependent types. With dependent types, it is possible to vary the set of commands available at different times. A typical example would be a program interacting through several windows. Once the program has opened a new window, it can interact with it (e.g. read input the user input to this window, or write to that window). After closing the window, such interaction is no longer possible. Another example might be the switching on and off of a printer. After switching it on we can print, whereas when the printer is switched off we can no longer print. Sometimes, the commands available depend on responses of the environment to our commands. For instance, if we try to open a network connection, we either get a success message – then we can communicate via the new channel created – or a failure message – then we can’t communicate.

1 Note that IO emerges here as a coalgebra rather than an algebra. This is natural, since what we actually need for running such programs is the function elim. One could introduce instead IO as an F-algebra (which can be introduced by the Petersson-Synek trees [24]) and use the fact that under some weak initiality condition, an F-algebra is as well an F-coalgebra. Then IO is an inductive-recursive definition and therefore part of a standard extension of Martin-Löf type theory. However, unless one uses non-well-founded type theory, one would not be able to introduce non-well-founded elements of IO.

Continuation-passing I/O (see [9], Sect. 7.6 for an excellent description) represents IO as an algebraic type. If one distinguishes between algebras and coalgebras, this could be considered to be a coalgebra. That type is very close to our definition of IO.

A very general situation can be modelled by having a set S : Set of states of the system. Depending on s : S we have a set of commands C(s) : Set. For every s : S and c : C(s) we have a set of responses R(s, c) to this command. After a response to a command is received the system reaches a new state, so we have, depending on s : S, c : C(s) and r : R(s, c) a next state n(s, c, r) of the system. A dependent interface consists of these four components,

S : Set
C : S → Set
R : (s : S, c : C(s)) → Set
n : (s : S, c : C(s), r : R(s, c)) → S

So the set of dependent interfaces is

Interface^{dep} := (S : Set) ×(C : S → Set) ×(R : (s : S, c : C(s)) → Set) ×((s : S, c : C(s), r : R(s, c)) → S)

Programs for dependent interfaces As with non-dependent interfaces, we require for ⟨S, C, R, n⟩ : Interface, that we have a set of interactive programs IO(s) : Set for every s : S. IO(s) should be the set of interactive programs starting in state s. In order to be able to perform an interactive program p : IO(s), we need to determine the command c : C(s) to be issued, and a function which for every r : R(s, c) returns a program to be performed after this response, starting in state n(s, c, r). That program is therefore an element of IO(n(s, c, r)). Let elim be the function which determines c and the next program. If we define

F : (S → Set) → (S → Set)
F(X, s) := (c : C(s)) × ((r : R(s, c)) → X(n(s, c, r)))

then we obtain

IO : S → Set ,
elim : (s : S) → IO(s) → F(IO, s) .

The introduction of elements of IO(s) is similar to the case of non-dependent interfaces. Instead of one set X of nodes, as in the non-dependent case, the introduction of an interactive program now requires for every state s a set of nodes X(s), i.e. an S-indexed set X : S → Set. For every s : S and x : X(s) we need to determine from p : IO(s) the command c : C(s) to be issued and for r : R(s, c) the next node of type X(n(s, c, r)) with which the program continues. As before, these two functions can be incorporated by one function f : (s : S) → X(s) → F(X, s). Further we need an initial node x_{0} : X(s). So we have the following introduction rule for IO (as mentioned before, the name Coiter, which stands for coiteration, will be explained in Sect. 8):

Coiter : (X : S → Set, f : (s : S) → X(s) → F(X, s), s : S) → X(s) → IO(s) .

Weakly final coalgebras on S → Set. As in the case of non-dependent interactive programs, we require an equality rule to hold. Assume X : S → Set, f : (s : S) → X(s) → F(X, s), s : S, and x : X(s). Assume f(s, x) = ⟨c, g⟩ where g : R(s, c) → X(n(s, c, r)). Then

elim(s, Coiter(X, f, s, x)) = ⟨c, λr.Coiter(X, f, n(s, c, r), g(r))⟩

Again we can extend F to an endofunctor on the presheaf category S → Set, by having as morphism part for X, Y : S → Set and f : (s : S) → X(s) → Y (s) the function F(f) : (s : S) → F(X, s) → F(Y, s), where F(f, s, ⟨c, g⟩) := ⟨c, λr.f(n(s, c, r), g(r))⟩. As before the functor laws can be proved only with respect to extensional equality.

With this extension, we can see that IO will be a weakly final coalgebra for F: We have elim : (s : S) → IO(s) → F(IO, s) and for every X : S → Set and f : (s : S) → X(s) → F(X, s) there exists an arrow Coiter(X, f) : (s : S) → X(s) → IO(s) such that elim ∘ Coiter(X, f) = F(Coiter(X, f)) ∘ f holds with respect to composition in the presheaf category (where f ∘ g := λs, x.f(s, g(s, x))):

X  F(X)

IO  F(IO) Coiter(X, f) elim f F(Coiter(X, f))

Bisimilarity. The definition of bisimilarity between non-state-dependent interactive programs extends directly to state-dependent interactive programs. A relation B′ : (s : S) → IO(s) → IO(s) → Set is a bisimulation relation, if for s : S and p, p′ : IO(s) such that B′(s, p, p′) we have that if elim(p) = ⟨c, g⟩ and elim(p′) = ⟨c′, g′⟩, then there exists a cc′ : Id(C(s), c, c′) and for r : R(s, c) we have that B′(n(s, c, r), g(r), g′′(r)) holds, where g′′ : (r : R(s, c)) → IO(n(s, c, r)) is obtained from g′ : (r : R(s, c′)) → IO(n(s, c′, r)) by using the transfer principle and cc′ (this short definition, which can be used with intensional equality, is due to M. Michelbrink). Bisimilarity B is now the largest such relation, i.e. the union of all bisimulation relations, and one can easily see that B is in fact a bisimulation relation. As before one can easily see that two programs p, q : IO(s) behave in the same way if and only if B(s, p, q) holds. We write p ≈_{s} q for B(s, p, q).

4 Server-Side Programs and Generalisation to Polynomial Functors

Server-side Programs. What we have described above are in a sense “clientside” programs: the program issues a command and gets back a response from the other side of the interface. There are as well server-side programs, in which the program receives commands to which it returns responses.

An example is a user interface. Currently, the standard way for defining user interface is that one first places components like buttons, text boxes and labels in the screen. Then one associates with certain components event handlers, which are functions that take as argument an event (e.g. the event of clicking the mouse on a button – the event will encode certain data about this, e.g. the coordinates of the mouse click, or flags indicating whether it was a single or double click). The event handler usually doesn’t return an answer, but when it is executed, a side effect will take place.

This model of a GUI corresponds to a server side program: the program waits for a command, e.g. a mouse click event associated with a button. Depending on that event, it performs one or more interactions with the window manager, the database and possibly other systems. Once these interactions are finished the program is waiting for the next event.

Server side programs correspond to the same definition of the set of interactive programs as above, but with respect to a different functor F, namely in case of non-dependent interfaces

F(X) = (c : C) → ((r : R(c)) × X)

and in case of dependent interfaces

F(X, s) = (c : C(s)) → ((r : R(s, c)) × X(n(s, c, r)))

Let us write in the following F^{∞} for the set of interactive programs corresponding to functor F. In the non-dependent case we need F^{∞} : Set and a function elim : F^{∞} → F(F^{∞}), which, depending on a program and a command c : C from the outside world, determines the response of the interactive program to it and the next interactive program to be performed. In the dependent version, we need an S-indexed set F^{∞} : S → Set of interactive programs, and a function elim : (s : S) → F^{∞}(s) → F(F^{∞}, s), which determines for every s : S, p : F^{∞}(s) and every command c : C(s) from the outside world a response r : R(s, c) and a program p′ : F^{∞}(n(s, c, r)), the program continues with.

Generalisation: Polynomial functors on families of sets. We have seen the need to introduce sets F^{∞} : S → Set such that there exists elim : (s : S) → F^{∞}(s) → F (F^{∞}, s) and constructors

Coiter : (X : S → Set) → ((s : S) → X(s) → F (X, s)) → (s : S) → X(s) → F^{∞}(s)

where we used two kinds of endofunctors on S → Set, namely F = λX, s.(c : C(s))×(R(s, c) → X(n(s, c, r))) and F = λX, s.(c : C(s)) → (R(s, c)×X(n(s, c, r))). Note that endofunctor of the first kind are more general than those of the second kind: functors of the second kind are by the axiom of choice equivalent to functors of the first kind, whereas the other direction does not always hold.

We can generalise the above to general polynomial functors F : (S → Set) → (S → Set), which are essentially of the form λX.(c : C(s)) → ((r : R(s, c)) × ((d : D(s, r, c)) → · · ·. All these functors are strictly positive, and we will in a later article extend the set of polynomial functors to a set of strictly positive ones.

The definition of the set of polynomial functors (which is a dependent form of the usual definition of polynomial functors and extends for instance [4]) is as follows: First we define inductively the set of polynomial functors F : (S → Set) → Set:

– (Projection.) For s : S, λX.X(s) is a polynomial functor.

– (The constant functor.) If A : Set, then λX.A is a polynomial functor.

– If A : Set and for a : A F_{a} : (S → Set) → Set is a polynomial functor, so is λX.(a : A) → F_{a}(X).

– If A : Set and for a : A F_{a} : (S → Set) → Set is a polynomial functor, then λX.(a : A) × F_{a}(X) is a polynomial functor.

– If F, F′ are polynomial functors (S → Set) → Set, so is λX, s.F (X, s) + F′(X, s).

(The last case could be reduced to the previous cases by defining it as λX.s.(x :

2) × G_{x}(X, s) where G_{∗_{0}}(X, s) = F (X, s), G_{∗_{1}}(X, s) = F′(X, s).)

If for s : S, F_{s} : (S → Set) → Set is a polynomial functor, then λX, s.F_{s}(X) is a polynomial functor (S → Set) → S → Set.

Polynomial functors F : Set → Set are inductively defined in the same way as polynomial functors F : (S → Set) → Set, except the clause for projection is replaced by the following:

– (Identity). λX.X is a polynomial functor.

It is an easy exercise to introduce for polynomial functors F the morphism part, i.e. for f : (s : S) → X(s) → Y (s) a function F (f) : (s : S) → F (X, s) → F (Y, s). However to show that the functor-laws hold on the category of presheaves S → Set requires extensional equality.

Equivalents of polynomial functors. In the presence of extensional type theory, one can show that each polynomial functor F : (S → Set) → (S → Set) is equivalent to a functor G of the form G(X, s) = (c : C(s)) × ((r : R(s, c)) → X(n(s, c, r))) for some C, R, n, i.e. there exists a natural equivalence f : F →^{·} G. (A similar result for a weaker (non-dependent) version of polynomial functors was shown in [4].) We show first that every polynomial functor F : (S → Set) → Set is equivalent to a functor λX.(c : C)×((r : R(c)) → X(n(c, r))) for some C : Set, R : C → Set and n : (c : C) → R(c) → S:

– In case of F (X) = X(s) we define C := 1, R(c) := 1, n(c, r) := s. The corresponding functor G = λX.1×(1 → X(s)) is easily seen to be equivalent to F.

– In case of F (X) = A for A : Set we define C := A, R(c) := ∅, n(c, r) := efq(r). Using extensional equality, one can easily see that the corresponding functor G = λX.A × ((r : ∅) → X(efq(r))) is equivalent to F.

– In case of F (X) = (a : A) → F_{a}(X), and F_{a}(X) being equivalent to (c : C′(a)) × ((r : R′(a, c)) → X(n′(a, c, r))), let C := ((a : A) → C′(a)), R(c) := (a : A) × R′(a, c(a)), n(c, ⟨a, r⟩) := n′(a, c(a), r). The corresponding functor G = λX.(c : (a : A) → C′(a)) × ((r′ : (a : A) × (r : R′(a, c(a)))) → X(n(c, r′))) is equivalent to λX.(c : (a : A) → C′(a)) × ((a : A) → (r : R′(a, c(a))) → X(n′(a, c(a), r))), which by the axiom of choice is equivalent to λX.(a : A) → ((c : C′(a)) × ((r : R′(a, c(a))) → X(n′(a, c, r)))), which is equivalent to F.

– In case of F (X) = (a : A) × F_{a}(X) and F_{a}(X) being equivalent to (c : C′(a))×((r : R′(a, c)) → X(n′(a, c, r))), let C := (a : A)×C′(a), R(⟨a, c⟩) := R′(a, c) and n(⟨a, c⟩, r) := n′(a, c, r). The corresponding functor G = λX.(b : ((a : A)×C′(a)))×((r : R(b)) → X(n(b, r))) is equivalent to λX.(a : A)×((c : C′(a)) × ((r : R′(a, c)) → X(n′(a, c, r)))), which is equivalent to F.

– In case of F (X) = F_{0}(X) + F_{1}(X) and F_{i}(X) being equivalent to (c : C_{i}) × ((r : R_{i}(c)) → X(n_{i}(c, r))), let C := C_{0} + C_{1} and R(inl(c)) := R_{0}(c), R(inr(c)) := R_{1}(c), n(inl(c), r) := n_{0}(c, r), n(inr(c), r) := n_{1}(c, r). The corresponding functor G = λX.(c : C) × ((r : R(c)) → X(n(c, r))) is equivalent to λX.((c : C_{0}) × ((r : R_{0}(c)) → X(n_{0}(c, r)))) + ((c : C_{1}) × ((r : R_{1}(c)) → X(n_{1}(c, r)))), which is equivalent to F.

If now F : (S → Set) → (S → Set) is polynomial and F (X, s) = F_{s}(X) where F_{s} is equivalent to G_{s} := λX.(c : C(s)) × ((r : R(s, c) → X(n(s, c, r))), then F is equivalent to λX, s.G_{s}(X), which is of the desired form.

5 Coiteration in Dependent Type Theory

The standard rules for dependent type theory allow us to introduce inductively defined sets, which correspond to (weakly) initial algebras. Coalgebraic types are not represented in a direct way. Markus Michelbrink is working on modelling state-dependent coalgebras in intensional type theory. At the time of writing this article it seems that he has succeeded, although the proof is complex, and has yet to be verified. Even when his approach is finally accepted, it will still be rather complicated to carry out proofs about coalgebras in this way. Furthermore, if one models interactive programs in this way, it would probably be rather inefficient to actually execute such programs.

The usual approach in dependent type theory is to introduce new types directly as first class citizens rather than reducing them using complicated methods to already existing types. That’s what one needs in programming in general: a rich type structure rather than a minimal one, that allows one to program without having to carry out a complicated encoding.

So we think that the right approach is to extend type theory by new rules for weakly final coalgebras. Of course one needs to show that such an extension is consistent, and we will do so in a future article by developing a PER module. (In [17] a set theoretic model for final coalgebras was developed.)

The rules given below depend on a polynomial function F : S → Set, which we do not make explicit. In fact, a derivation is required to show that F is a polynomial functor, which means that the rules have additional premises to the effect that that F is a polynomial functor. A complete set of rules for deriving polynomial functor would require the introduction of a data type of such functors analogous to the data type of inductive-recursive definitions introduced in [5]. However, such a theory would lie outside the scope of the present article. For the moment it suffices to restrict the theory to functors of the form F = λX, s.(c : C(s)) × ((r : R(s, c)) → X(n(s, c, r))). That F is a polynomial functor is guaranteed by ⟨S, C, R, n⟩ : Interface.

From the considerations in the previous section we obtain the following rules for weakly final coalgebras. These rules are reasonably well-known in the theory of coalgebras, but as far as we know they haven’t been investigated in the context of Martin-Löf’s type theory.

Formation Rule:

\begin{matrix}s : S \\ F^{∞}(s) : Set \end{matrix}

Introduction Rule:

A : S → Set  f : (s : S) → A(s) → F(A, s)  s : S  x : A(s)
Coiter(A, f, s, x) : F^{∞}(s)

Elimination Rule:

s : S  p : F^{∞}(s)
elim(s, p) : F(F^{∞}, s)

Equality Rule:

elim(s, Coiter(A, f, s, x)) = F(Coiter(A, f), s, f(x))

Note that in the case F(X, s) = (c : C(s))×((r : R(s, c)) → X(n(s, c, r))) we have that elim(s, Coiter(A, f, s, x)) = ⟨c, λr.Coiter(A, f, s, g(r))⟩ where f(x) = ⟨c, g⟩. So in this case the equation can be rewritten in the following form.

elim(s, Coiter(A, f, s, x)) = case (f(x)) of ⟨c, g⟩ → ⟨c, λr.Coiter(A, f, s, g(r))⟩

Non-dependent version. In the case S = 1 we have by the η-rule that S → Set and Set are isomorphic. Instead of using this isomorphism, it is more convenient to add special rules for non-dependent polynomial functors F : Set → Set, which are as follows:

Formation Rule:

F^{∞} : Set

Introduction Rule:

A : Set  f : A → F(A)  x : A
Coiter(A, f, x) : F^{∞}

Elimination Rule:

\begin{matrix}p : F^{∞} \\ elim(p) : F(F^{∞}) \end{matrix}

Equality Rule:

elim(Coiter(A, f, x)) = F(Coiter(A, f), f(x))

Inductive data types vs. coalgebras. There is a certain duality between the rules we have just given, and the rules for inductive data types such as the natural numbers or the W-type.

– With inductive data types, the introduction rules are “simple”. There is no reference to the totality of sets. On the other hand, the elimination rules are complex and refer universally to all sets. (For example, with induction on N one can have any set as the result type).

– For coalgebras, the elimination rules are “simple”, and don’t refer to arbitrary sets. On the other hand the introduction rules are complex, and can refer existentially to arbitrary sets.

This duality is in the nature of things. In the case of inductive data types, we form the least set closed under various operations. What ‘closed’ means is given by introduction rules, and described in a simple way. The real power of these types lies in the stipulation that we have the least such closed set, and this requires an induction principle referring to all sets.

In the coalgebraic case, we form the largest set which fulfils a certain elimination principle. The elimination principle corresponds to a simple elimination rule. The strength comes from the fact that we have the largest such set and that requires reference to arbitrary sets.

6 Monadic Rules for Coiteration

One can also define a monadic version of F^{∞}, which has an extra argument X : S → Set. In a sense, this parameter plays the rôle of the result type X in Haskell’s IO X. We expect that the monadic form of the coiteration principle will prove more useful in practical programming. For a full explanation of the qualification “monadic”, see [17].

We write in the following leaf(x) for inl(x) and command(x) for inr(x). The rules are then as follows. Formation Rule:

X : S → Set  s : S
F_{mon}^{∞}(X, s) : Set

Introduction Rule: Define F′(X, A, s) := (X(s) + F (A, s)). Then

X : S → Set A : S → Set f : (s : S) → A(s) → F′(X, A, s) s : S a : A(s) Coiter_{mon}(X, A, f, s, a) : F_{mon}^{∞}(X, s)

Elimination Rule:

X : S → Set s : S p : F_{mon}^{∞}(X, s)
elim(X, s, p) : X(s) + F (F_{mon}^{∞}(X), s)

Equality Rule:

elim(X, s, Coiter_{mon}(X, A, f, s, a)) =
[λx.leaf(x), λy.command(F (Coiter_{mon}(X, A, f), s, y))](f(s, a))

Note the following implications of the equality rule.

– If f(a) = leaf(x), then elim(X, s, Coiter_{mon}(X, A, f, s, a)) = leaf(x),

– If f(a) = command(y), then elim(X, s, Coiter_{mon}(X, A, f, s, a)) = command(F (Coiter_{mon}(X, A, f), s, y)).

– In the particular case F (X, s) = (c : C(s)) × ((r : R(s, c)) → X(n(s, c, r))), if f(a) = command(⟨c, g⟩), then elim(X, s, Coiter_{mon}(X, A, f, s, a)) = command(⟨c, λr.Coiter_{mon}(X, A, f, s, g(r))⟩).

One can derive the monadic rules from the nonmonadic rules by defining F_{mon}^{∞}(X, s) := G^{∞}(s) where G(Y) = X(s) + F (Y, s). Then the rules for G^{∞} yield the monadic rules for F_{mon}^{∞}. Conversely, the rules for G^{∞} can be obtained from the rules for F_{mon}^{∞}(X) where X(s) = ∅.

7 Guarded Induction

Coiter and guarded induction. Coiteration can be read as a recursion principle. In clarify what we mean by this, let us consider the weakly final F-coalgebra IO for the functor F = λX.(c : C) × (R(c) → X) : Set → Set. A function f : X → (c : C) × (R(c) → X) can be split into two function c : X → C and next : (x : X) → R(c(x)) → X. Then the rules for Coiter(X, f) express that for functions c and next as above there exists a function g : X → IO (defined as Coiter(X, f)) such that for x : X we have

elim(g(x)) = ⟨c(x), λr.g(next(x, r))⟩ .

If one thinks of C, R as an interface of an interactive system, this can be read as: the interactive program g(x) is defined recursively by determining for every x : X a command c(x) and then the continuation function that handles a response to this command, defined in terms of g itself.

In the theory of coalgebras one often discusses the introduction of coalgebras A by definitions of the form

A = codata C_{0}(⋯) | ⋯ | C_{n}(⋯) ,

where C_{i} are constructors, and the arguments of the constructors may refer to A itself at strictly positive positions, as well as to previously defined sets and set constructors. For example the co-natural numbers N^{∞}, the set of streams of values of type A, and the set of interactive programs can be introduced by the respective definitions

N^{∞} = codata 0 | S(n : N^{∞}) ,
Stream(A) = codata cons(a : A, l : Stream(A)) ,
IO = codata do(c : C, next : R(c) → IO) .

With this point of view, it is tempting reread the above recursion equation for g as

g(x) = do(c(x), λr.g(next(x, r))) .

However, were we to allow definitions of that kind, we would immediately get non-terminating programs. (For example, define g : 1 → IO by g(x) = do(c, λr.g(∗))). With the original equation elim(g(x)) = ⟨c(x), λr.g(next(x, r))⟩, termination is maintained because the elimination constant elim must be applied to g(x) to obtain a reducible expression. (The example just given reads elim(g(x)) = ⟨c, λr.g(∗)⟩, which is unproblematic.)

The principle for defining g(x) = do(c(x), λr.g(next(x, r))) is a simple case of guarded induction [3]. (See also well the work [7] of Gimenéz, related to the current work as discussed in the introduction). The idea of guarded induction is that one can define elements of such a codata set recursively, as long as every reference in the right hand side of the definition to the function we are defining recursively is “guarded” by at least one constructor. So one can define f : 1 → N^{∞} (‘infinity’) by f(x) = S(f(x)), one can define f : N^{∞} → N^{∞} (the successor of a co-natural) by f(x) = S(x) (without recursion), and one can define f : N → Stream(N) by f(n) = cons(n, f(n + 1)). However, one cannot define f : 1 → N^{∞} by f(x) = f(x), since in this equation the recursion is not guarded.

Guarded induction is unproblematic in the context of lazy functional programming, as long as one doesn’t need to test for equality, since there reduction to weak head normal form suffices. In dependent type theory, type checking depends on the decidability of equality of terms (see the example at the beginning of Sect. 2), and we have the following theorem:

Theorem In intensional Martin-Löf type theory extended by the principle of guarded recursion for streams in its original form equality of terms and therefore type checking is undecidable.

Proof: Define, depending on g_{i} : ℕ → ℕ, the functions f_{i} : ℕ → Stream (i = 0, 1) by guarded recursion as f_{i}(n) = cons(g_{i}(n), f_{i}(n + 1)). Then f_{0}(0) = f_{1}(0) if and only if g_{0} and g_{1} are extensionally equal, which is undecidable.

If one instead reads guarded induction as a definition of elim(g(x)) = ⋯ rather than g(x) = ⋯, we obtain an unproblematic principle, and one can see that a restricted form of guarded induction is, when viewed in this form, equivalent to coiteration:

The right-hand side of the codata definition

A = codata C_{0}(x_{0} : A_{0,0}, …, x_{m_{0}} : A_{0,m_{0}}) | ⋯ | C_{l}(x_{l} : A_{l,0}, …, x_{m_{l}} : A_{l,m_{l}})

can be read as a polynomial functor F : Set → Set,

F(X) = F_{0}(X) + ⋯ + F_{l}(X)

where

F_{i}(X) = ((x_{0} : A′_{i,0}(X)) × ⋯ × (x_{m_{0}} : A′_{i,m_{0}}(X)))

and A′_{i,j}(X) is obtained from A_{i,j} by replacing A by X. Note that A_{i,j} either does not depend on X, so the functor A′_{i,j} is constant, or A_{i,j} is of the form (y_{0} : D_{0}) → ⋯ → (y_{k} : D_{k}) → A, in which case

A′_{i,j} = λX.(y_{0} : D_{0}) → ⋯ → (y_{k} : D_{k}) → X ,

which is a polynomial functor.

Let C_{i} be the injection from F_{i}(F^{∞}) into F(F^{∞}). Then for every element of F^{∞} we have elim(a) = C_{i}(a) for some i and a : F_{i}(F^{∞}).

Now the principle of coiteration means that if we have a set A and a function f : A → F(A) then we get a function g : A → F^{∞} such that elim(g(a)) = F(g)(f(a)). This reads: if f(a) = C_{i}(⟨a_{0}, …, a_{k}⟩), then elim(g(a)) = C_{i}(⟨a′_{0}, …, a′_{k}⟩), where a′_{i} = a_{i}, in case A_{i,j}(X) does not depend on X, and a′_{i} = λy_{0}, …, y_{k}.g(a_{i}(y_{0}, …, y_{k})), in case A_{i,j}(X) = (y_{0} : D_{0}) → ⋯ → (y_{k} : D_{k}) → X.

We can reread this as follows. We can define a function f : A → F^{∞} by defining f(a) for a : A as some C_{i}(⟨b_{0}, …, b_{k}⟩) where b_{k} refer, when an element of F^{∞} is needed, to f applied to any other element of A. This corresponds to a restricted form of guarded induction, where the right hand side of the recursion has exactly one constructor, and one never refers to F^{∞} but only to f applied to some other arguments.

Let us consider now the definition of an indexed codata definition, i.e.

A_{0}(x : B_{0}) = codata C_{0,0}(⋯) | ⋯ | C_{0,m_{0}}(⋯)
⋯
A_{l}(x : B_{l}) = codata C_{l,0}(⋯) | ⋯ | C_{l,m_{l}}(⋯) ,

where the arguments of C_{i,j} refer to A_{i} at strictly positive positions. Let B := B_{0} + ⋯ + B_{l}. Then the above can be read as the definition of a B-indexed weakly final coalgebra A = F^{∞} : B → Set for a suitable polynomial functor F, which is introduced in a similar way as before. The analogy between guarded induction and iteration is as before, except that one defines now a function f : (b : B, C(b)) → F^{∞}(b) recursively by defining, in case b = in_{i}^{l}(b′) elim(b′, f(b′, c)) = C_{i,j}(⟨c_{0}, ⋯, c_{k}⟩), where c_{k} can refer (and has to refer), in case an element of F^{∞}(b′′) is needed, to an element f(b′′, c′) for some c′. So dependent coalgebras correspond to indexed codata definitions.

Bisimilarity as a state-dependent coalgebra. Bisimilarity in case of the functor F(X, s) = (c : C(s)) × (R(s, c) → X(n(s, c, r))) can be considered as a weakly final coalgebra over the index set

(s : S) × F^{∞}(s) × F^{∞}(s)

The condition for a bisimulation relation B as introduced above is that, if B(s, p, p′) holds, and elim(p) = ⟨c, g⟩ and elim(p′) = ⟨c′, g′⟩, then we have cc′ : Id(C(s), c(s), c′(s)) and for r : R(s, c(s)) we have B(n(s, c, r), g(r), g′′(r)), where g′′ was obtained from g′ using cc′. We can now define the polynomial functor (we curry the arguments for convenience)

G : ((s : S) → F^{∞}(s) → F^{∞}(s) → Set) → (s : S) → F^{∞}(s) → F^{∞}(s) → Set

G(X, s, p, p′) = case elim(p) of ⟨c, g⟩ → case elim(p′) of ⟨c′, g′⟩ → \begin{matrix}(cc′ : Id(C(s), c, c′))× \\ ((r : R(s, c)) → X(n(s, c, r), g(r), g′′(r))) \end{matrix}

with g′′ defined as above (using cc′). Then

elim : (s : S) → (p, p′ : F^{∞}(s)) → G^{∞}(s, p, p′) → G(G^{∞}, s, p, p′)

expresses that G^{∞}(s, p, p′) is a bisimulation relation. Further the principle of coiteration means that if we have

B : (s : S) → F^{∞}(s) → F^{∞}(s) → Set ,

and

f : (s : S, p, p′ : F^{∞}(s)) → B(s, p, p′) → G(B, s, p, p′) ,

then

Coiter(B, f) : (s : S, p, p′ : F^{∞}(s)) → B(s, p, p′) → G^{∞}(s, p, p′)

The existence of f means that B is a bisimulation relation, and Coiter(B, f) means that B is contained in G^{∞}. So Coiter expresses that G^{∞} contains any bisimulation relation. The introduction and equality rules together express therefore that G^{∞} is the largest bisimulation relation, i.e. bisimilarity. So the above rules allow to introduce bisimulation in type theory in a direct way, and one can use guarded induction as a proof principle for carrying out proofs about properties of bisimulation.

Normalisation. It seems that the normalisation proof by Geuvers [6] carries over to the intensional version of type theory used in this paper, and that therefore intensional type theory with the rules for state-dependent coalgebras is normalising. If one had guarded induction, normalisation would fail. A simple counter example is f : 1 → N^{∞}, f(∗) = S(f(∗)). Translating the guarded induction principle used here back into our rules, we obtain a function f := Coiter(1, g), where g := λx.inr(x) : 1 → (1 + 1). Note that f(∗) is already in normal form. The recursion is carried out only when one applies elim to f(∗), and we then obtain elim(f(∗)) = S(f(∗)), where the right hand side is again in normal form. So evaluation of full recursion is inhibited, since one needs to supply one application of elim in order to trigger a one step reduction of f.

8 Coiteration vs. Corecursion

The rules introduced in Sect. 5 and 6 correspond to coiteration, which is the dual of iteration. In the following we will show that although these rules are sufficient for introducing weakly final algebras, they are not very efficient. To overcome the inefficiency, we need corecursion, which is the dual of structural recursion. To illustrate the point, we begin by recalling the principles of iteration, recursion and induction on the natural numbers.

Iteration. The natural numbers can be introduced as the initial algebra of the polynomial functor F : Set → Set, where F(X) := 1+X. That N is an F-algebra means that we have a constructor intro : F(N) → N. This function is related to the usual constructors 0 and S of the natural numbers by the equations intro(inl) = 0, intro(inr(n)) = S(n). That N is a weakly initial algebra with respect to F means that if A : Set and f : A → (1 + A), then there exists a function Iter′(A, f) : N → A such that the following diagram commutes, i.e. Iter′(A, f) ∘ intro = f ∘ F(Iter′(A, f)).

1 + N  N

1 + A  A 1 + Iter′(A, f) f intro Iter′(A, f)

If one specialises the equalities for Iter′(A, f) to inl = 0 and inr(n) = S(n) one obtains Iter′(A, f, 0) = f(inl) and Iter′(A, f, S(n)) = f(inr(Iter′(A, f, n))). If one replaces the argument f in Iter′ by n := f(inl) and g := f ∘inr, one obtains a function Iter : (A : Set) → A → (A → A) → N → A such that Iter(A, a, g, 0) = a and Iter(A, a, g, S(n)) = g(Iter(A, a, g, n)), i.e. Iter(A, a, g, n) = g^{n}(a). Therefore Iter is the principle of iteration.

N is not only a weakly initial algebra but an initial algebra, which means that Iter′(a, f) (or equivalently Iter(a, f)) is the only function fulfilling the above mentioned equation. This is not guaranteed by the principle of iteration alone. In type theory it is guaranteed by the principle of induction – using induction one can show that if g is any other function s.t. g ∘ intro = f ∘ F(g), then (n : N) → Id(A, g(n), Iter′(a, f, n)).

There are many ways to define the predecessor function pred using iteration. One definition can be extracted from the reduction of recursion to iteration given below. Another is as follows. First define a function predaux : N → (1 + N) such that predaux(0) = inl, predaux(S(n)) = inr(n). predaux(n) = g^{n}(inl) = Iter(1 + N, inl, g, n) where g : (1 + N) → (1 + N), g(inl) = inr(0) and g(inr(n)) = inr(S(n)). Defining h : (1 + N) → N, h(inl) = 0, h(inr(m)) = m, we obtain pred(n) = h(predaux(n)).

Since pred(m) = h(g^{m}(c)), one needs m steps in order compute pred(m). Of course, this is drastically less efficient then the usual definition of pred(m) given by the equations pred(0) = 0 and pred(S(m)) = m, which can be computed in constant time. It seems inevitable that any definition of the predecessor function which uses iteration rather than recursion cannot be evaluated in constant time, though as far as the authors know, this has never been proved. (For some results in this direction, see [26].)

Recursion. The standard efficient definition of pred is obtained by using the principle of recursion. Recursion means that we can use the value of n when computing f(S(n)). It can be expressed by the principle that for C : Set and f : (1 + (N × C)) → C, there exists a function Rec(C, f) : N → C such that the following diagram commutes:

1 + N  N

1 + (N × C)  C 1 + ⟨id, Rec(C, f)⟩ f intro Rec(C, f)

The commutativity of the diagram means that f∘(1+⟨id, Rec(C, f)⟩) = Rec(C, f)∘ Coiter. Applied to 0 = inl and S(m) = inr(m) we obtain the equations Rec(C, f, 0) = f(inl) and Rec(C, f, S(m)) = f(inr(⟨Rec(C, f, m), m⟩)). If we divide again f into f(inl) and λn, c.f(inr(⟨n, c⟩)) we obtain the more convenient variant Rec′ : (C : Set) → C → (N → C → C) → N → C, with the equalities Rec(C, c, g, 0) = c, Rec(C, c, g, S(m)) = g(m, Rec(C, c, g, m)).

Using recursion, the predecessor can be defined as pred := Rec(N, 0, λm, c.m). It is easily verified that pred(0) = 0 and pred(S(m)) = m. This computation can be carried out in constant time.

Rec′(C, c, f) can be defined interms of the operator Iter as π_{1} ∘ g, where g := Iter(N × C, ⟨0, c⟩, λa.⟨S(π_{0}(a)), f(π_{0}(a), π_{1}(a))⟩). One can then show by induction on n that g(n) = ⟨n, Rec′(C, c, f, n)⟩.

Induction. Induction is the principle one obtains from recursion by letting the set C depend on n : N. This means that if we have a C : N → Set, a function f : (x : 1 + N) → C(Coiter(x)) then there exists a function Ind(C, f) : (n : N) → C(n) such that Ind(C, f, Coiter(x)) = f(Coiter(x), (1 + Ind(C, f))(x)). Splitting f again into its components, we obtain Ind′ : (C : N → Set) → C(0) → ((n : N) → C(n) → C(S(n))) → (n : N) → C(n) together with the equalities Ind′(C, c, d, 0) = c, Ind′(C, c, d, S(m)) = d(m, Ind′(C, c, d, m)).

We now show that the induction principle is equivalent to the uniqueness of the arrow in the diagram from iteration.

First, we use the induction principle to show the uniqueness of the arrow h in the commutative diagram for iteration. Suppose that f : (1 + D) → D, and assume that h_{0}, h_{1} : N → D are two functions which make the diagram corresponding to iteration with respect to the function f : (1+D) → D commute, i.e. f ∘ (1 + h_{i}) = h_{i} ∘ intro.Then one can use C(n) := Id(N, h_{0}(n), h_{1}(n)) (where Id(N, k, l) is the identity type between k : N and l : N) and the induction principle in order to compute a function g : (n : N) → C(n), which proves that h_{0}(n) and h_{1}(n) coincide for all n : N.

In the other direction, Ind′(C, c, d) can be derived from the uniqueness of the arrow by first introducing a function h : N → ((n : N) × C(n)) as h := Iter((n : N) × C(n), ⟨0, c⟩, g) with g(a) := ⟨S(π_{0}(a)), d(π_{0}(a), π_{1}(a))⟩. One can extend the resulting diagram by a second one using π_{0} : ((n : N) × C(n)) → N as follows.

1 + N  N

1 + ((n : N) × C(n))  (n : N) × C(n)

1 + N  N intro 1 + h h g 1 + π_{0} π_{0} intro

It follows now that the lower square commutes as well. Therefore π_{0} ∘ h is a function N → N which gives rise to an arrow from the algebra intro : (1 + N) → N to itself. The identity function λx.x is another such function. Using the uniqueness of the arrow from an initial algebra into another algebra, we obtain that h ∘ π_{0} and λx.x coincide. Therefore π_{0}(h(n)) = n and we can take Ind′(C, c, d) to be the function λn.π_{1}(h(n)) : (n : N) → C(n).

Coiteration. Coiteration is obtained by reversing the arrows in the diagram for iteration. We consider the special case of the co-natural numbers N^{∞}, which are the weakly final coalgebra of the function F := λX.(1 + X) : Set → Set. That N^{∞} is a coalgebra for F means that there exists a function elim : N^{∞} → 1+N^{∞}. Let us write 0_{A} for inl : 1 + A, S_{A}(a) for inr(a) : 1 + A, where a : A, and let us omit the subscript A in case A = N^{∞}. Then the elimination rule means that for every element of n : N^{∞} either elim(n) = 0 or elim(n) = S(m) for some m : N^{∞}.

As regards bisimularity, if elim(n) = 0 and elim(n′) = 0 then n ≈ n′. Further if elim(n) = S(m), elim(n′) = S(m′) and m ≈ m′ then n ≈ n′. This can be shown by defining R(x, y) :⇔ x ≈ y ∨ (elim(x) = 0 ∧ elim(y) = 0) ∨ (∃x′, y′.elim(x) = S(x′) ∧ elim(x′) = y′ ∧ x′ ≈ y′). It follows that R is a bisimulation relation, therefore R(x, y) → x ≈ y and therefore the claim holds.

The principle of coiteration is that if we have A : Set and g : A → (1+A), then there exists a function Coiter(A, g) : A → N^{∞} such that elim ∘ Coiter(A, g) = F(Coiter(A, g)) ∘ g. In other words, the following diagram should commute.

A  1 + A

N^{∞}  1 + N^{∞} Coiter(A, g) elim g 1 + Coiter(A, g)

So if a : A and g(a) = 0_{A} then elim(Coiter(A, g, a)) = 0, and if g(a) = S_{A}(a′) then elim(Coiter(A, g, a)) = S(Coiter(A, g, a′)). This priis the principle of coiteration.

In other words:

if f = Coiter(A, g) then elim(f(a)) = case g(a) of ; \begin{aligned}0_{A} & → & 0 \\ S_{A}(a′) & → & S(f(a′)) \end{aligned}

Note that if one defines n := Coiter(1, λx.inr(∗)), we get elim(n) = S(n), so N^{∞} contains infinite co-natural numbers.

With iteration the definition of pred is computational expensive, and similarly, with coiteration the definition of the successor function is expensive (however we don’t show this here). The problem is that when introducing an element n using Coiter one has to define a set C which contains representatives of n, its predecessor, the predecessor of its predecessor and so on.

A definition of the successor using coiteration is as follows: Let C := 1+N^{∞}. Define f : C → 1 + C, by:

f(inl) = 0_{C}
f(inr(n)) = case elim(n) of 0 → S_{C}(inl) S(m) → S_{C}(inr(m))

Define g := Coiter(C, f) : C → N^{∞}, zero := g(inl) and succ : N^{∞} → N^{∞}, succ(n) = g(inr(n)). Then we get

\begin{matrix}elim(zero) & = & 0 \\ elim(succ(n)) & = & case elim(n) of 0 → S(zero) S(m) → S(succ(m)) \end{matrix} (∗)

Now one can show that elim(succ(n)) = S(m) for some m such that m ≈ n, which means that succ is a successor operation up to bisimulation:

Define

R(n, m) :⇔ (n = zero ∧ elim(m) = 0) ∨ ∃k.(n = succ(k) ∧ elim(m) = S(k)) .

R is a bisimulation: Assume R(n, m). Show elim(n) = 0 ↔ elim(m) = 0 and if elim(n) = S(m) and elim(n) = S(m′) then R(m, m′).

– Case n = zero, elim(m) = 0. Then elim(n) = 0.

– Case n = succ(k). Then elim(m) = S(k) and we have to show that elim(n) = S(n′) for some n′ such that R(n′, k):

• If elim(k) = 0, then elim(n) = S(zero) and we have R(zero, k).

• If elim(k) = S(k′) then elim(n) = S(succ(k′)), and R(succ(k′), k).

Therefore R(n, m) implies n ≈ m.

Now we show that elim(succ(n)) = S(m) for some m such that m ≈ n:

– If elim(n) = 0 then elim(succ(n)) = S(zero) where zero ≈ n.

– If elim(n) = S(n′) then we have elim(succ(n)) = S(succ(n′)), further R(succ(n′), n), therefore succ(n′) ≈ n.

Corecursion. The reason we were unable to define a constant-time predecessor function using iteration is that one cannot make use of the argument n in the definition of h(S(n)) where h := Iter(C, c, g). In case of coiteration, the problem is that we cannot escape to an element of N^{∞} directly when defining g : C → (1+C) in Coiter(C, g). If one allows this one obtains a new principle guaranteeing the existence of functions Corec(C, g) : C → N^{∞} for every g : C → (1+(C+N^{∞})) such that the following diagram commutes:

C  1 + (C + N^{∞})

N^{∞}  1 + N^{∞} Corec(C, g) elim g 1 + [Corec(C, g), id_{N^{∞}}]

Define continue := inl : C → (C + N^{∞}) and return := inr : N^{∞} → (C + N^{∞}). Then we have:

if f = Corec(C, g) then elim(f(c)) = case g(c) of 0_{C} → 0 S_{C}(c′) → case c′ of continue(c′′) → S(f(c′′)) return(n) → S(n)

Now we can define succ′(n) := Corec(1, λx.S(return(n)), ∗). It follows that elim(succ′(n)) = S(n), so succ′ is the successor operation.

The function succ′ is much more efficient then succ, as elim(succ′^{k+1}(zero)) computes in one step to S(succ′^{k}(zero)). In contrast, the evaluation of elim(succ^{k+1}(zero)) requires the evaluation first of elim(succ^{k}(zero)), then of elim(succ^{k−1}(zero)), and so forth.

9 Corecursion in Dependent Type Theory

As discussed in the previous section, it does not seem possible to define the successor function on the co-natural numbers in an efficient way, merely on the basis of coiteration. Instead we need a corecursion principle. For the same reasons, in the general situation of a coinductively defined set

A = codata C_{0}(⋯) | ⋯ | C_{l}(⋯)

it is inefficient to compute the analogue of the constructors C_{i} on the corresponding coalgebras merely on the basis of the coiteration operator Coiter, introduced in section 5. In particular, when dealing with interactive programs, it will be inefficient to compute from a command c : C(s) and a family of programs g : (r : R(c)) → F^{∞}(n(s, c, r)) a new program p such that elim(p) = ⟨c, g⟩, which means to form a program with one additional initial interaction from a family existing programs.

If one follows the analogy with guarded induction, one sees that the problem is that when defining a function g : A → F^{∞} by determining elim(g(a)), one would like to refer to elements of F^{∞} itself, besides the function g.

This leads us to a new operator Corec which takes a predicate A : S → Set, a function f : (s : S) → A(s) → F (A +_{S} F^{∞}, s), and elements s : S and x : A(s) and returns an element of F^{∞}. The rules for this new operator are as follows.

Formation and elimination rules are as before.

Introduction Rule:

A : S → Set  f : (s : S) → A(s) → F (A +_{S} F^{∞}, s)  s : S  a : A(s)
Corec(A, f, s, a) : F^{∞}(s)

Equality Rule:

elim(s, Corec(A, f, s, x)) = F ([Corec(A, f), id]_{S}, s)(f(x))

We cannot derive these rules from the rules for coiteration, or at least it doesn’t seem possible to achieve definitional equality in the equality rule. However, under the assumptions of the introduction rule based on Corec we can define a function g : (s : S, A(s)) → F^{∞}(s) such that the two sides of the conclusion of the equality rule are equal modulo bisimulation. To show this, we will work in extensional type theory, and restrict ourselves to the special case of a functor F (X, s) = (c : C(s)) × ((r : R(s, c)) → X(n(s, c, r))). It seems likely that the result can also be proved in intensional type theory, at least if we restrict ourselves to the simple functor corresponding to state dependent IO. (Note that in extensional type theory, polynomial functors in general can be reduced to this particular case.)

Assume A : S → Set and f : (s : S, A(s)) → F (A +_{S} F^{∞}, s). Define f′ : (s : S, (A +_{S} F^{∞})(s)) → F (A +_{S} F^{∞}, s) by f′(s, inl(a)) = f(s, a) and f′(s, inr(x)) = F (λs, x.inr(x))(elim(s, x)). We now define our substitute for Corec as follows: Corec′(A, f, s, a) := Coiter(A +_{S} F^{∞}, f′, s, inl(a)).

We next show that, if f(a) = ⟨c, g⟩ then elim(Corec′(A, f, s, a)) = ⟨c, g′⟩ where for r : R(s, c) we have that, in the case g(r) = inl(b) then g′(r) ≈ Corec′(A, f, s, b) and in the case g(r) = inr(b) then g′(r) ≈ b. This means that elim(s, Corec′(A, f, s, a)) is equal to F (Corec(A, f) +_{S} id, s, f(a)) up to bisimilarity.

First one shows that for h : (s : S) → F^{∞}(s) → F^{∞}(s) defined by h(s, a) := Coiter(A+_{S}F^{∞}, f′s, inr(a)) we have h(s, a) ≈ a. To this end, we define a relation Q for s : S and a, a′ : F^{∞}(s) by Q(s, a, a′) :⇔ Id(F^{∞}(s), a, h(s, a′)). From this it follows if Q(s, a, a′) and elim(a′) = ⟨c, g⟩, then elim(h(s, a′)) = ⟨c, g′⟩ where g′(r) = h(n(s, c, r), g(r)), therefore Q(n(s, c, r), g(r), g′(r)). So Q is a bisimulation relation and thus h(s, a) ≈ a.

The equality rule for corecursion, but with = replaced by ≈ follows directly.

Extended principle. In section 5 we introduced a coiteration principle for dependent polynomial functors, and in section 6 a monadic extension of this principle, that we expect to be more useful in practise. Above, we have introduced a corecursion principle for dependent polynomial functors. How about a monadic extension of corecursion? We now propose just such an extension. The reader may find it helpful to refer back to section 6. Again we write in the following leaf(x) for inl(x) and command(x) for inr(x).

Formation and elimination rules: (as in the monadic version) Introduction Rule: Define F′(X, A, s) := (X(s) + F (A +_{S} F_{mon}^{∞}(X), s)). Then

X : S → Set A : S → Set f : (s : S) → A(s) → F′(X, A, s) s : S a : A(s) Corec_{mon}(X, A, f, s, a) : F_{mon}^{∞}(X, s)

Equality Rule:

elim(X, s, Corec_{mon}(X, A, f, s, a)) = [λx.leaf(x), λy.command(F (Corec_{mon}(X, A, f) +_{S} id, s, y))](f(s, a))

We conjecture that the functor F^{∞} satisfies the laws of a monad, and that this can be established by an adaption of the proof in [17]. However further exploration of these rules is required.

A yet further extension that may prove more flexible in practical programming is motivated by guarded induction. In guarded induction, the idea is that the function being defined may occur on the right-hand side of the definition provided that these occurrences are guarded by at least one application of a constructor. The principles we have described so far are less general, and correspond to the idea of guarding by exactly one occurrence of a constructor. We are currently considering therefore principles of the following extended form. For simplicity we give only the introduction rule.

(Extended) Introduction Rule: Define F′(X, A, s) := (X(s) +_{S} F (F_{mon}^{∞}(A +_{S} X), s)). Then

X : S → Set A : S → Set f : (s : S) → A(s) → F′(X, A, s) s : S a : A(s) Corec_{mon}(A, f, s, a) : F_{mon}^{∞}(X, s)

The presence of the functor F_{mon}^{∞} nested inside F in the premise of this rule reflects the possibility of guarding occurrences of the function being defined by more than one application of a constructor.

There are however many essentially equivalent forms in which the same idea can be formulated. These require further exploration. In particular, it needs to be verified that they indeed determine functors that are monads.

10 Conclusion

We have explored one approach to the representation of interactive programs in dependent type theory, and seen that it gives rise to weakly final coalgebras for polynomial functors. We have investigated rules for final coalgebras that correspond to coiteration and shown that they correspond to a certain form of guarded induction, namely the definition of functions g : A → F^{∞} by equations elim(g(x)) = C_{i}(t_{0}, …, t_{k}) where the terms t_{i} can (and in fact have to) refer, if an element of F^{∞} is required, to g itself.

Interactive Programs and Weakly Final Coalgebras 29

We have also introduced rules that correspond to a more general form of guarded induction in which reference can be made directly to previously introduced elements of F^{∞} in the terms t_{i}, where an element of F^{∞} is required. Those rules express a form corecursion, rather than merely coiteration. We have formulated a further extension that allows further uses of the constructors for the coalgebra in the terms t_{i}. This would allow for instance the definition of a function from N into streams of natural numbers such that elim(f(n)) = cons(n, cons(n, f(n + 1))). The extension depends in a crucial way on formulating the rules for coiteration and recursion as rules for monadic functors.

This is work in progress. Something that remains is to construct a PER model for our rules, although in [17] a set theoretic model is given. We haven’t fully investigated the relationship between guarded induction and the monadic forms of our rules, although in [17] it is shown that what we have called the monadic form of coiteration indeed determines a monadic functor. Further we haven’t yet interpreted non-state-dependent coalgebras in ordinary type theory. We hope to repair these deficiencies in the future.

References

1. Achten, P., Plasmeijer, M.J.: The ins and outs of Clean I/O. Journal of Functional Programming 5 (1995) 81–110

2. Bertot, Y., Castéran, P.: Interactive Theorem Proving and Program Development. Springer (2004)

3. Coquand, T.: Infinite objects in type theory. In Barendregt, H., Nipkow, T., eds.: Types for Proofs and Programs, International Workshop TYPES’93, Nijmegen, The Netherlands, May 24-28, 1993, Selected Papers. Volume 806 of Lecture Notes in Computer Science., Springer (1994) 62–78

4. Dybjer, P.: Representing inductively defined sets by wellorderings in Martin-Löf’s type theory. Theoret. Comput. Sci. 176 (1997) 329–335

5. Dybjer, P., Setzer, A.: Induction-recursion and initial algebras. Annals of Pure and Applied Logic 124 (2003) 1 – 47

6. Geuvers, H.: Inductive and coinductive types with iteration and recursion. In Nordström, B., Petersson, K., Plotkin, G., eds.: Informal proceedings of the 1992 workshop on Types for Proofs and Programs, Bastad 1992, Sweden. (1992) 183 – 207

7. Gimenéz, E.: Codifying guarded definitions with recursive schemes. In: Proceedings of the 1994 Workshop on Types for Proofs and Programs, LNCS No. 996 (1994) 39–59

8. Goguen, H., Luo, Z.: Inductive data types: Well-ordering types revisited. In Huet, G., Plotkin, G., eds.: Logical Environments. Cambridge University Press, Cambridge (1993) 198–218

9. Gordon, A.: Functional programming and Input/Output. Distinguished Dissertations in Computer Science. Cambridge University Press (1994)

10. Hallnäs, L.: An intensional characterization of the largest bisimulation. Theoretical Computer Science 53 (1987) 335–343

11. Hancock, P.: Ordinals and interactive programs. PhD thesis, LFCS, University of Edinburgh (2000)

30 A. Setzer, P. Hancock

12. Hancock, P., Hyvernat, P.: Programming as applied basic topology. Submitted, available via http://iml.univ-mrs.fr/ hyvernat/Files/giovanni.ps.gz (2004)

13. Hancock, P., Setzer, A.: Interactive programs in dependent type theory. In Clote, P., Schwichtenberg, H., eds.: Computer Science Logic. 14th international workshop, CSL 2000. Volume 1862 of Springer lecture notes in computer science. (2000) 317– 331

14. Hancock, P., Setzer, A.: The IO monad in dependent type theory. In: Electronic proceedings of the workshop on dependent types in programming, Göteborg, 27-28 March 1999. (1999) Available via http://www.md.chalmers.se/Cs/Research/Semantics/APPSEM/dtp99.html.

15. Hancock, P., Setzer, A.: Specifying interactions with dependent types. In: Workshop on subtyping and dependent types in programming, Portugal, 7 July 2000. (2000) Electronic proceedings, available via http://wwwsop.inria.fr/oasis/DTP00/Proceedings/proceedings.html.

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

17. Michelbrink, M., Setzer, A.: State dependent IO-monads in type theory. To appear in the proceedings of the CTCS’04, Electronic Notes in Theoretical Computer Science, Elsevier (2004)

18. Milner, R.: Communication and Concurrency. Prentice Hall (1989)

19. Martin-Löf, P.: Constructive mathematics and computer programming. In Cohen, Los, Pfeiffer, Podewski, eds.: Logic, Methodology and Philosophy of Science, VI, 1979, Amsterdam, North-Holland (1982) 153–175

20. Martin-Löf, P.: Intuitionistic Type Theory. Volume 1 of Studies in Proof Theory: Lecture Notes. Bibliopolis, Napoli (1984)

21. Moggi, E.: Computational lambda-calculus and monads. In: Proceedings of the Logic in Computer Science Conference. (1989)

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

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

24. Petersson, K., Synek, D.: A set constructor for inductive sets in Martin-Löf’s type theory. In: Category theory and computer science (Manchester, 1989), LNCS 389, Springer (1989) 128 – 140

25. Peyton Jones, S.L., Wadler, P.: Imperative functional programming. In: 20’th ACM Symposium on Principles of Programming Languages, Charlotte, North Carolina (1993)

26. Spławski, Z., Urzyczyn, P.: Type fixpoints: iteration vs. recursion. In: Proceedings of the fourth ACM SIGPLAN international conference on Functional programming. (1999) 102–113

27. Wadler, P.: Monads for functional programming. In Broy, M., ed.: Program Design Calculi. Volume 118 of NATO ASI series, Series F: Computer and System Sciences. Springer Verlag (1994)

28. Wadler, P.: How to declare an imperative. ACM Comput. Surv. 29 (1997) 240–263