State Dependent IO-Monads in Type Theory

Markus Michelbrink^{∗} Anton Setzer^{†} Department of Computer Science University of Wales Swansea Singleton Park Swansea SA2 8PP United Kingdom {m.michelbrink,a.g.setzer}@swansea.ac.uk

May 18, 2004

Abstract

We introduce the notion of state dependent interactive programs for Martin-Löf Type Theory. These programs are elements of coalgebras of an endofunctor on the presheaf category S → Set. We prove the existence of final coalgebras for these functors. This shows as well the consistency of type theory plus rules expressing the existence of weakly final coalgebras for these functors, which represents the type of interactive programs. We define in this type theory the bisimulation relation, and give some simple examples for interactive programs. A generalised monad operation is defined by corecursion on interactive programs with return value, and a generalised version of the monad laws for this operation is proved. All results have been verified in the theorem prover Agda which is based on intensional type theory.

1 Introduction

Martin-Löf’s type theory [7] can be seen as a programming logic for a functional programming language. The judgement a ∈ A can especially be read as:

1. a is a program with type A

2. a is a program which satisfies the specification A

3. a is an implementation of the abstract data type specification A.

The above relies on the identification of sets, proposition, and specifications. With this identification dependent type theory gives us the ability to express with full precision any extensional property of a program, which can be defined mathematically. We can check the type of a program mechanically, and type correctness carries full assurance that it satisfies its specification. Versions of type theory have been implemented e.g. in Göteborg [10], Cornell [3], Cambridge [9], Edinburgh [6, 11], and INRIA [2]. In type theory running a program means normalising an expression. Every program terminates, and there is no interaction with the environment. This model is adequate for a large class of programs which, when given a value, execute and give back another value. It is however not adequate for the whole class of programs, which interact with their environment and possibly never terminate. In this article we continue work of Peter Hancock and Anton Setzer [4, 5]. We generalise the notion of interfaces (worlds) and IO-programs to state dependent interfaces and state dependent programs. In [5] a world is a pair (C, R), where C : Set and R : C → Set. c : C is interpreted as a command, and Rc is the set of possible responses (from a user, a device or another program) to the command c. For every set A the set of programs IO A : Set (we keep the world fixed) has constructors leaf : A → IO A and do : (c : C, p : Rc → IO A) → IO A. The program leaf a terminates and returns value a, whereas do (c, p) executes c, and after receiving response r : Rc continues as p r : IO A. We generalise this by giving every program a state s : S. Now the set of executable commands, the responses, as well as the function giving us the next program depend on the state s : S. The resulting notion suits better to real world applications. One of our key examples is a windowing system. The client may request a server to open a window. The states now represent the open windows. The generalisation leads us naturally to an endofunctor F on the presheaf category S → Set. We show that this functor has a final coalgebra elim : F^{∞} → F (F^{∞}). We enrich type theory by rules for a weakly version of this final coalgebra (weakly because we do not demand uniqueness of μ(α). See below.). The elimination rule corresponds to the morphism elim, the introduction rules to the requirement that there is a morphism μ(α) : A → F^{∞} for every coalgebra α : A → F A, and the equality rule expresses that the associated diagram commutes. The formation rule simply reflects the fact that there is a coalgebra F^{∞}. We define bisimulation for interactive programs. After introducing rules for interactive programs with return value, we define a monad operation ∗ by corecursion, and show that the monad laws for this operation hold with respect to bisimulation. We work in extensional Type Theory. However the results can be achieved in intensional Type Theory as well. Intensional versions of the results of Sect. 6 are verified in Agda [10]. The code is available under http://www.cs.swan.ac.uk/∼csmichel/. Overview. In Sect. 2 we motivate our settings. In Sect. 3 we relate our basic ideas from Sect. 2 to an endofunctor on S → Set, and show that this functor has a final coalgebra. In Sect. 4 we introduce the new rules for IO-programs, and define bisimulation. In Sect. 5 we give some simple examples for IO-programs. In Sect. 6 we introduce the rules for IO-programs with return values, define a monad operation for this programs, and show the monad laws with respect to bisimulation. Besides Sect. 3 we work in a standard dependent type theory (e.g. [8]) with the usual formation, introduction, elimination, and equality rules, extended by our rules. Acknowledgements. Many ideas for this article are due to P. Hancock, Edinburgh. He could well have been a third author for this article, but preferred to publish his slightly different point of view separately.

∗Supported by EPSRC grant GR/S30450/01.

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

2 Interfaces, Programs

An interface is a quadruple (S, C, R, n) s.t.

• S : Set

• C : S → Set

• R : ∏ s : S.C(s) → Set

• n : ∏ s : S. ∏ c : C(s).R(s, c) → S

S is the set of states, C(s) the set of commands in state s : S, R(s, c) the set of responses to a command c : C(s) in state s : S, and n(s, c, r) the next state of the system after this interaction. Continuing our example above, in X windows the X server performs the requests (commands) for its clients, and sends them back replies (responses). The possible requests depend on the state of the client, the replies depend on the state of the server and the state of the shared resources: the drawing area and the input channel.

We can view an interface as a generalised transition system, where we have a transition (s, c, r) between states s : S and s′ : S iff c : C(s), r : R(s, c) and s′ = n(s, c, r). There are two canonical ways to view an ordinary transition system as interface:

• Take C(s) = {T ransition starting from s} and R(s, t) as singletons.

• Take C(s) as singletons and R(s, ∗) = {T ransition starting from s}.

The picture visualises a part of an interface:

[figure: s; c_{0}; c_{1}; c_{2}; •; r_{00}; r_{01}; r_{02}; •; •; …; s′_{00}; s′_{01}; s′_{02}]

Let (S, C, R, n) be an interface. A program for this interface starting in state s : S is a quadruple (A, c, next, a) s.t.

• A : S → Set

• c : ∏ s : S.A(s) → C(s)

• next : ∏ s : S. ∏ a : A(s). ∏ r : R(s, c(s, a)).A(n(s, c(s, a), r))

• a : A(s)

A(s) is the set of programs starting in state s, c(s, a) the command issued by the program a : A(s), and next(s, a, r) is the program that will be executed, after having obtained for command c(s, a) the response r : R(s, c(s, a)). In the example the program would be an X client. It should be noted, that this is the client version of a program. If we interchange in the functor below products and sums, we get server side programs. The picture visualises a part of a program in relation to its interface. Dashed lines belong

to the program: [figure: s; c_{0}; c_{1}; c_{2}; •; •; r_{00}; r_{01}; r_{02}; •; s′_{00}; s′_{01}; s′_{02}]

3 IO as Final Coalgebra

If we view the set S as a discrete category (with only arrows id_{s} for s : S), the presheaf category S → Set has objects X : S → Set and morphism f : ∏ s : S.X(s) → Y (s), where X, Y : S → Set. The composition g ∘ f : ∏ s : S.X(s) → Z(s) of two morphism f : ∏ s : S.X(s) → Y (s) and g : ∏ s : S.Y (s) → Z(s) is defined by

(g ∘ f)(s, x) = g(s)(f(s, x))

for s : S, x : X(s). id_{X} : ∏ s : S.X(s) → X(s) is given by id_{X}(s) = id_{X(s)}.

We look at the functor F : (S → Set) → (S → Set) defined by • F X(s) = ∑ c : C(s). ∏ r : R(s, c).X(n(s, c, r)) for X : S → Set and

• for f : ∏ s : S.X(s) → Y (s)

F f(s) : F (X, s) → F (Y, s) ,
F f(s)(c, g) = (c, λr.f(n(s, c, r), g(r))) .

One easily sees that F is a Functor. A final coalgebra in a category C for an endofunctor F : C → C is an object F^{∞} together with a morphism elim : F^{∞} → F (F^{∞}) s.t. for any object A and morphism g : A → F A there is exactly one morphism f : A → F^{∞} making the following diagram commute:

\xymatrix{F^{∞} \ar[r]^{elim} & F (F^{∞}) \\ A \ar@{-->}[u]^{f} \ar[r]_{g} & F A \ar@{-->}[u]_{F f}}

We will show in this section, that the previous defined functor has a final coalgebra. This is not surprising. However the proof gives a hint how to internalize the notions in Martin-Löf Type Theory. This will be done in a forthcoming paper. For simplicity, we argue in ZF for the rest of this section. Essentially we just use induction on the natural numbers. To get the final coalgebra we first define by induction sets CT_{0}(s) and functions first_{S}, last_{S} : CT_{0}(s) → S, first_{C}, last_{C} : CT_{0}(s) → C(s) and length : CT_{0}(s) → N for s : S. In this section ∗ denotes the concatenation of two lists.

Definition 1 CT_{0}(s) has as elements lists

(s_{0}, c_{0}, r_{1}, ..., r_{n}, s_{n}, c_{n})

for 0 ≤ n with s_{0} = s, c_{i} ∈ C(s_{i}), r_{i+1} ∈ R(s_{i}, c_{i}) and s_{i+1} = n(s_{i}, c_{i}, r_{i+1}), and we define

length((s, c))  := 1
length(l′ ∗ (r, s, c))  := length(l′) + 1
first_{S}((s_{0}, c_{0}, r_{1}, ..., r_{n}, s_{n}, c_{n})) := s_{0}
last_{S}((s_{0}, c_{0}, r_{1}, ..., r_{n}, s_{n}, c_{n})) := s_{n}
first_{C}((s_{0}, c_{0}, r_{1}, ..., r_{n}, s_{n}, c_{n})) := c_{0}
last_{C}((s_{0}, c_{0}, r_{1}, ..., r_{n}, s_{n}, c_{n})) := c_{n}
pd((s, c))  := (s, c)
pd(l′ ∗ (r, s, c))  := l′

We write R(l) for R(last_{S}(l), last_{C}(l)), l ∈ CT_{0}(s), n(l, r) for n(last_{S}(l), last_{C}(l), r), r ∈ R(l). We are now able to define the domain of the final coalgebra:

Definition 2 For s ∈ S and T ⊆ CT_{0}(s) let

φ(T, s) := ∃!c ∈ C(s).(s, c) ∈ T &  (1)
∀l ∈ T.∀r ∈ R(l).∃!c ∈ C(n(l, r)).
l ∗ (r, n(l, r), c) ∈ T &  (2)
∀l ∈ T.pd(l) ∈ T  (3)

We define for s ∈ S:

CT (s) := {T ⊆ CT_{0}(s)|φ(T, s)}.

CT : S → Set. That means CT is an object of S → Set. We can interpret the elements of CT (s) as computation trees for a program p : IO(s). Part (1) of φ(T, s) says that there is exactly one root (s, c) in each T ∈ CT (s). Part (2) of φ(T, s) ensures that for l ∈ T and every r ∈ R(l) there is exactly on successor l ∗ (r, s′, c′) in T and part (3) of φ(T, s) says that T is closed against predecessors. Note that

first_{C}(l) = first_{C}(l′) for l, l′ ∈ T ∈ CT (s) .

Sets T, T′ ∈ CT (s) have a nice property:

Lemma 1 For T, T′ ∈ CT (s)

T ⊆ T′ ⇔ T = T′ .

Proof: Induction on length(l). Let l ∈ T′. If l = (s′, c′), then s′ = first_{S}(l) = s because T′ ⊆ CT_{0}(s). By Definition of CT (s) there is exactly one c ∈ C(s) with (s, c) ∈ T ⊆ T′. Again by Definition of CT (s) follows c = c′ and therefore l = (s, c) ∈ T. If l = l′ ∗ (r′, s′, c′), then l′ = pd(l) ∈ T′. By I.H. is l′ ∈ T. Since l′ ∈ T ⊆ CT_{0}(s) is r′ ∈ R(l′), s′ = n(l′, r′) and c′ ∈ C(s′)). By Definition of CT (s) there is again exactly one c′′ ∈ C(s′) with l′∗(r′, s′, c′′) ∈ T ⊆ T′. T′ ∈ CT (s) implies c′ = c′′ and so l ∈ T. □

Definition 3 For T ∈ CT (s) let

elim(s, T) = (c, h) ,

where for some l ∈ T

c = first_{C}(l)
h : ∏ r : R(s, c) → C(n(s, c, r))
h(r) = {l ∈ CT_{0}(n(s, c, r))|(s, c, r) ∗ l ∈ T }.

The equations define a morphism elim : CT → F (CT). h(r) gives us the subtree of T on position r.

Theorem 1 The previous defined Functor F : (S → Set) → (S → Set) has a final coalgebra in the category S → Set.

Proof: We claim that (CT, elim) is a final coalgebra for F. Let g(s) : A(s) → F A(s) for s : S. We write g = (g_{0}, g_{1}), where g_{0}(s) = π_{0}(g(s)) ∈ C(s), and g_{1}(s) = π_{1}(g(s)) ∈ ∏ r : R(s, g_{0}(s)).A(n(s, g_{0}(s), r)). We have to show that there is a unique morphism T : A → CT such that the diagram on page 4 with F^{∞} = CT and f = T commutes. For this purpose, we define simultaneously sets T (s, a) ∈ CT (s) for s ∈ S, a ∈ A(s) and elements next_{S}(l, r) ∈ S, next_{A}(l, r) ∈ A(next_{S}(l, r)) for l ∈ T (s, a), r ∈ R(l) by

T^{0}(s, a)  := {(s, g_{0}(s, a))}
next_{S}((s, g_{0}(s, a)), r) := n(s, g_{0}(s, a), r)
next_{A}((s, g_{0}(s, a)), r) := g_{1}(s, a, r)
T^{i+1}(s, a)  := {l ∗ (r, s′, c′)| l ∈ T^{i}(s, a)

& r ∈ R(l) & s′ = n(l, r) & c′ = g_{0}(s′, next_{A}(l, r))}

next_{S}(l ∗ (r, s′, c′), r′):= n(s′, c′, r′)
next_{A}(l ∗ (r, s′, c′), r′):= g_{1}(s′, next_{A}(l, r), r′)
T (s, a)  := ⋃_{i∈N} T^{i}(s, a)

We show by induction on i that

T^{i}(n(s, c, r), g_{1}(s, a, r)) =
{l ∈ CT_{0}(n(s, c, r))|(s, c, r) ∗ l ∈ T^{i+1}(s, a)} (∗)

for i ∈ N, s ∈ S, a ∈ A(s), c = g_{0}(s, a), r ∈ R(s, c): Let A_{i} := T^{i}(n(s, c, r), g_{1}(s, a, r)) and B_{i} := {l ∈ CT^{0}(n(s, c, r))|(s, c, r) ∗ l ∈ T^{i+1}(s, a)}.

(s′, c′) ∈ A_{0} ⇒ s′ = n(s, c, r) &
c′ = g_{0}(n(s, c, r), g_{1}(s, a, r))
= g_{0}(s′, next_{A}((s, c), r))
⇒ (s, c, r) ∗ (s′, c′) ∈ T^{1}(s, a)
⇒ (s′, c′) ∈ B_{0}
l ∗ (r′, s′, c′) ∈ A_{i+1} ⇒ l ∈ A_{i} ⊆ B_{i} & r′ ∈ R(l) &
s′ = n(l, r′) &
c′ = g_{0}(s′, next_{A}(l, r′))
⇒ (s, c, r) ∗ l ∗ (r′, s′, c′)
∈ T^{i+2}(s, a)
⇒ l ∗ (r′, s′, c′) ∈ B_{i+1}

It follows easily by induction on i that T (s, a) ∈ CT (s) for s ∈ S, a ∈ A(s). T : A → CT makes the diagram commute:

π_{0}(elim(s, T (s, a))) = g_{0}(s, a) =: c
π_{1}(elim(s, T (s, a)))(r) = {l ∈ CT_{0}(n(s, c, r))|(s, c, r) ∗ l ∈ T (s, a)}
= T (n(s, c, r), g_{1}(s, a, r)) ,

where the last equation follows by (∗). It remains to show that T is unique. Let T′ : A → CT a morphism making the diagram commute. We show T^{i}(s, a) ⊆ T′(s, a) for all i ∈ N by induction: i = 0 : We have

π_{0}(elim(s, T′(s, a))) = π_{0}(g(s, a)) = g_{0}(s, a) ,

and so T^{0}(s, a) ⊆ T′(s, a). Let T^{i}(s, a) ⊆ T′(s, a) for all s ∈ S, a ∈ A(s) and (s, c, r) ∗ l ∈ T^{i+1}(s, a). Then

c = g_{0}(s, a) = π_{0}(elim(s, T′(s, a))) ,

and

l ∈ T^{i}(n(s, c, r), g_{1}(s, a, r))
⊆ T′(n(s, c, r), g_{1}(s, a, r))
= π_{1}(elim(s, T′(s, a)))(r)
= {l ∈ CT_{0}(n(s, c, r))|(s, c, r) ∗ l ∈ T′(s, a)} ,

and therefore (s, c, r) ∗ l ∈ T′(s, a). By the previous Lemma follows the claim. □

4 Rules for IO-programs

Let elim : ∏ s : S.IO(s) → F (IO)(s) be a final coalgebra for F in the category S → Set. We can now define c : ∏ s : S.IO(s) → C(s) and next : ∏ s : S. ∏ c : IO(s). ∏ r : R(s, c(s, p)).IO(n(s, c(s, p), r)) by

c(s, p) = π_{0}(elim(s, p))
next(s, r) = π_{1}(elim(s, p))(r).

We enrich our type theory by the following rules:

Formation Rule

\begin{matrix}S : Set & s : S \\ IO(s) : Set \end{matrix}

Elimination Rule

S : Set  s : S  p : IO(s)

elim(s, p) : \underbrace{Σc : C(s). ∏ r : R(s, c).IO(n(s, c, r))}_{F (IO,s)}

Introduction Rule

\begin{matrix}S : Set \\ A : S → Set \end{matrix} ; g : ∏ s : S.A(s) → F (A, s) ; μ(A, g) : ∏ s : S.A(s) → IO(s)

Equality Rule

\begin{matrix}S : Set \\ A : S → Set \end{matrix} ; g : ∏ s : S.A(s) → F (A, s) ; s : S ; a : A(s)

elim(s, μ(A, g)(s, a)) = onestep(g(s, a)) : F (IO, s)

where

onestep((c, h)) = (c, λr.μ(A, g)(n(s, c, r), h(r))) .

Furthermore, we define

∼ : (n : N, S : Set, s : S, p, q : IO(s)) → Set
≈ := (S : Set, s : S, p, q : IO(s)) → Set

by the following equations:

p ∼_{0} q := ⊤
p ∼_{n+1} q := Id(C(s), c, c′)
∧∀r ∈ R(s, c).
π_{1}(elim(s, p))(r) ∼_{n} π_{1}(elim(s, q))(r)
p ≈ q : ∀n ∈ N.p ∼_{n} q ,

where

c := π_{0}(elim(s, p))
c′ := π_{0}(elim(s, q)) .

Note that the introduction rule for the IO-Sets looks more complicated than the elimination rule. Like for inductive defined sets the introduction rule says what our canonical elements are. However, whereas for inductive sets in the premises of the introduction rule only appear certain sets here we can have any family of sets to introduce a new element in IO(s). Otherwise the elimination rules say how to define a function on these sets. However, whereas for inductive sets the range can be any set here it is the fixed set Σc : C(s). ∏ r : R(s, c).IO(n(s, c, r)).

5 Examples

Console I/O can be seen as state dependent IO.

• The states are n : N representing the number of characters written on console.

• The commands C(n) are

– C(0) = {readchar, writechar(n : OutputChar)} If we have not written anything, we can read a character from keyboard, or write a character to the console.

– C(S n) = C(0) ∪ {delete}.

If we have written something, we can additionally delete the last character.

• The response sets are

– R(n, readchar) = InputChar,

  – R(n, writechar n) = {Ok},

– R(S n, delete) = {Ok}.

If we read a character, we obtain the character read. Otherwise we obtain a confirmation that the action was carried out.

– n(n, readchar, c) = n,

– n(n, writechar n, Ok) = S n,

– n(S n, delete, Ok) = n.

If we read a character, we do not do anything (the idea is that characters not automatically reflected on the console input). If we write a character, then the length of the output increases by one. If we delete the last character, the last character is deleted.

5.1 Example Programs

• l : readchar
     goto l

A(s) = {l}, g(s, l) = (readchar, λn.l), p = μ(A, g, (), l).

• Assume InputChar = OutputChar

char c
l0: readchar(c)
l1: writechar(c)
     goto l0

A(n) = {l_{0}, l_{1}(k : N)}, g(n, l_{0}) = (readchar, λk.l_{1}(n)), g(n, l_{1}(n)) = (writechar n, λ .l_{0}), p = μ(A, g, (), l_{0}).

• Assume InputChar = Char∪{delete}, OutputChar = Char∪{beep}. delete stands for the delete button, and beep means to signal a beep.

lengthOfInput : N
l0 : readchar (c)
l1 : if c == delete then{
        if lengthOfInput == 0 then {
          beep
          goto l0}
        else {
          backspace
          goto l0}
      else{
        writechar c
        goto l0}

A(0) = {l_{0}, l_{1}, l_{2}}, A(S n) = {l_{0}, l_{1}(c : InputChar), l_{3}}, g(n, l_{0}) = (readchar, λc.l_{1} c), g(0, l_{1} delete) = (beep, λ .l_{0}), g(S n, l_{1} delete) = (delete, λ .l_{0}), and for x ≠ delete, g(n, l_{1} x) = (writechar n, λ .l_{0}), p = μ(A, g, (), l_{0}).

5.2 Railway System

A railway control system is a state dependent interactive system.

• The states encode the segments of the railway system, which are blocked.

• Commands allow us to change the state of signals, but only in such a way that a green signal does not grant access to a blocked segment.

• In response to such a command, we get information about trains entering and leaving blocks.

• The next state is obtained from the response set.

• Any program written for this interface fulfils the safety requirement that one never sets a signal leading into a blocked segment to green.

6 IO Programs with Return Value

Until now the only way to terminate for our programs is that R(s, c) is empty for some s, c. If a program reaches this situation, there is never any response, and the program is locked up. We want our programs to terminate and to give back some value, which we can see as value for the function calculated by the program. Therefore, we give our programs the ability to terminate in a state s with a certain value a from a set A(s). For X : ∏ s : S.Set and A : ∏ s : S.Set, let F_{A}(X, s) be

A(s) + Σc : C(s). ∏ r : R(s, c).X(n(s, c, r)) .

Formation Rule

S : Set s : S A : S → Set
IO_{A}(s) : Set

Elimination Rule

\begin{matrix}S : Set & s : S & p : IO_{A}(s) \\ elim_{A}(s, p) : F_{A}(IO_{A}, s) \end{matrix}

Introduction Rule

\begin{matrix}S : Set \\ A, B : S → Set \end{matrix} ; g : ∏ s : S.B(s) → F_{A}(B, s) ; μ(B, g) : ∏ s : S.B(s) → IO_{A}(s)

Equality Rule

\begin{matrix}S : Set \\ A, B : S → Set \end{matrix} ; g : ∏ s : S.B(s) → F_{A}(B, s) ; s : S ; b : B(s)

elim_{A}(s, μ(B, g)(s, b)) = onestep(g(s, b)): F_{A}(IO_{A}, s)

where onestep(inl a) = inl a ,

onestep(inr (c, h)) = inr (c, λr.μ(B, g)(n(s, c, r), h(r))) .

Furthermore, we define

∼ : (n : N, S : Set, s : S, p, q : IO(s)) → Set
≈ : (S : Set, s : S, p, q : IO(s)) → Set

by the equations p ∼_{0} q := ⊤ p ∼_{n+1} q := Case elim(s, p) of

inl a : Case elim(s, q) of

inl b : Id(A(s), a, b)
inr (c′, h′) : ⊥
inr (c, h) : Case elim(s, q) of
inl b : ⊥
inr (c′, h′) : Id(C(s), c, c′) ∧ ∀r ∈ R(s, c).h(r) ∼_{n} h′(r)

p ≈ q = ∀n ∈ N.p ∼_{n} q

We also write coit_{g} for μ(A, g), p ⇝ a for elim(s, p) = inl a, p ⇝ (c, h) for elim(s, p) = inr (c, h), and sometimes omit indices and superscripts. Note that ≈ gives us bisimulation since our programs are image finite processes in terms of process algebra: If p ⇝ (c, h), then p →^{r} q exactly if q = h(r).

The concept of a monad also originates from category theory, and generalises the notion of a monoid (see e.g. [1]). It plays an important role in functional programming (e.g. [12]). We are going to define a monad operation

∗_{s} : IO_{A}(s) → (∏ s : S.A(s) → IO_{B}(s)) → IO_{B}(s)

Assume p : IO_{A}(s) and q : ∏ s : S.A(s) → IO_{B}(s), then (we suppress s) p ∗ q : IO_{B}(s) is the program, which runs as p, until it terminates with a value a : A(s′), and then continues as q(a) : IO_{B}(s′). We start by defining a canonical translations can_{l}:

Definition 4 Let X, Y, A : ∏ s : S.Set. can_{l}(s) : F_{A}(X, s) → F_{A}(X + Y, s) be given by

can_{l} = F_{A}(inl) ,

i.e.

can_{l}(s, inl a)  = inl a
can_{l}(s, inr (c, h)) = inr (c, λr.inl h(r))

In category theory, if elim : F^{∞} → F F^{∞} is a final coalgebra, then exists for every f : A → F (F^{∞} + A) a unique arrow corec_{f} such that the following diagram commutes:

\xymatrix{F^{∞} \ar[r]^{elim} & F (F^{∞}) \\ A \ar@{-->}[u]^{_{corec_{f}}} \ar[r]_{f} & F (F^{∞} + A) \ar@{-->}[u]_{F [id_{F^{∞}} ,corec_{f}]}}

This motivates the following definitions in type theory:

Definition 5 For g : ∏ s : S.A(s) → C(s) and h : ∏ s : S.B(s) → C(s) we define

[g, h] : ∏ s : S.(A(s) + B(s)) → C(s)

by

[g, h](s, o) := [g(s), h(s)](o) := when(o, g(s), h(s)) .

For f : ∏ s : S.A(s) → F_{B}(IO_{B} + A, s) let

\overline{coit}_{f} := coit_{[can_{l}∘elim,f]}
= μ(IO_{B} + A, [can_{l} ∘ elim, f])
∈ ∏ s : S.(IO_{B}(s) + A(s)) → IO_{B}(s) ,

and corec_{f} : ∏ s : S.A(s) → IO_{B}(s) with

corec_{f}(s, p) = \overline{coit}_{f}(s, inr p) .

Definition 6 For q : ∏ s : S.A(s) → IO_{B}(s) let q^{∗} : ∏ s : S.IO_{A}(s) → F_{B}(IO_{B} + IO_{A}, s) be defined by

q^{∗}(s, p) = Case elim(s, p) of
inl a  : can_{l}(s, elim(s, q(s, a)))
inr (c, h) : inr (c, λr.inr h(r))

We define now ∗ : IO_{A}(s) → (∏ s : S.A(s) → IO_{B}(s)) → IO_{B}(s) by

p ∗ q := ∗(p, q) := corec_{q^{∗}}(s, p) ,

and

η_{A} := coitη̆ : ∏ s : S.A(s) → IO_{A}(s) ,

where η̆: ∏ s : S.A(s) → F_{A}(A, s) with η̆(s, a) = inl a.

If h : ∏ r : R(s, c).IO_{A}(n(s, c, r)) and q(s) : A(s) → IO_{B}(s) for s : S, define

h ∗ q = λr.h(r) ∗ q : ∏ r : R(s, c).IO_{B}(n(s, c, r)) .

Lemma 2 Let o : IO_{A_{1}}(s), p(s) : A_{0}(s) → IO_{A_{1}}(s) for s : S. Then

\overline{coit}_{p^{∗}}(s, inl o) ≈ o .

Proof: Let p̄ = \overline{coit}_{p^{∗}}. We show p̄(s, inl o) ∼_{n} o by induction on n. We have p̄(s, inl o) ∼_{0} o. Assume p̄(s, inl o) ∼_{n} o for all o. First case: elim(s, o) = inl a. Then we have

[can_{l} ∘ elim, p^{∗}](s, inl o) = can_{l}(s, elim(s, o)) = inl a ,

and so by equality

elim(s, p̄(s, inl o)) = inl a = elim(s, o) .

Therefore, p̄(s, inl o) ∼_{n+1} o. Second case: elim(s, o) = inr (c, h). Then we have

[can_{l} ∘ elim, p^{∗}](s, inl o) = can_{l}(s, elim(s, o))
= inr (c, λr.inl h(r)) ,

so by equality

elim(s, p̄(s, inl o)) = inr (c, λr.inl p̄(n(s, c, r), inl h(r))) .

Then by I.H. p̄(s, inl h(r)) ∼_{n} h(r) and the claim. □

We are now able to prove the first monad law:

Theorem 2 Let p : IO_{A}(s) and q : ∏ s : S.A(s) → IO_{B}(s). Then by elim_{A}(s, p) = inl a follows

p ∗ q ≈ q(s, a) .

Proof: I. elim_{B}(s, q(s, a)) = inl b. Then we get can_{l}(s, elim(s, q(s, a)) = inl b , and therefore by elim_{A}(s, p) = inl a

[can_{l} ∘ elim, q^{∗}](s, inr p) = q^{∗}(s, p) = inl b .

And by the equality rule

elim_{B}(s, \underbrace{\overline{coit}_{q^{∗}}(s, inr p)}_{=p∗q}) = inl b = elim_{B}(s, q(s, a)) .

II. elim_{B}(s, q(s, a)) = inr (c, h). Then we get can_{l}(s, elim(s, q(s, a))) = inr (c, λr.inl h(r)) , and therefore by elim_{A}(s, p) = inl a

[can_{l} ∘ elim, q^{∗}](s, inr p) = q^{∗}(s, p) = inr (c, λr.inl h(r)) .

By the equality rule,

elim_{B}(s, \underbrace{\overline{coit}_{q^{∗}}(s, inr p)}_{=p∗q}) = inr (c, λr.\overline{coit}_{q^{∗}}(n(s, c, r), inl h(r))).

By Lemma 2 follows

h(r) ≈ \overline{coit}_{q^{∗}}(n(s, c, r), inl h(r))

for r : R(s, c), and therefore p ∗ q ≈ q(s, a) . □

Corollary 1 If q : ∏ s : S.A(s) → IO_{B}(s), then

η(s, a) ∗ q ≈ q(s, a) .

Unless otherwise noted, let

o : IO_{A_{0}}(s)
p(s) : A_{0}(s) → IO_{A_{1}}(s)
q(s) : A_{1}(s) → IO_{A_{2}}(s)
p̄ = \overline{coit}_{p^{∗}}

for s : S for the rest of the article. Lemma 3 If o ⇝ (c, h), then

o ∗ p ⇝ (c, h ∗ p) .

Proof: By elim(s, o) = inr (c, h) follows p^{∗}(s, o) = inr (c, λr.inr h(r)) . By equality, we get

elim(s, p̄(s, inr o)) = inr(c, λr.p̄(n(s, c, r), inr h(r))) .

We have o ∗ p = corec_{p^{∗}}(s, o) = p̄(s, inr o), and

h(r) ∗ p = corec_{p^{∗}}(n(s, c, r), h(r)) = p̄(n(s, c, r), inr h(r))

for r : R(s, c). Therefore, elim(s, o ∗ p) = inr(c, λr.h(r) ∗ p) . □

Theorem 3 If p : IO_{A}(s), then p ∗ η ≈ p .

Proof: We show p ∗ η ∼_{n} p by induction on n. I. elim_{A}(s, p) = inl a. Then we have

elim_{A}(s, p ∗ η) = elim_{A}(s, η(s, a)) = inl a = elim_{A}(s, p)

II. elim_{A}(s, p) = inr (c, h). By Lemma 3 we get

elim_{A}(s, p ∗ η) = inr (c, λr.h(r) ∗ η) ,

and by I.H. follows the claim. □

Lemma 4 If o ⇝ (c, h), then (o ∗ p) ∗ q ⇝ (c, (h ∗ p) ∗ q) .

Proof: By Lemma 3. □

Lemma 5 If o ⇝ (c, h), then o ∗ (λs, a.p(s, a) ∗ q) ⇝ (c, h ∗ (λs, a.p(s, a) ∗ q)) .

Proof: By Lemma 3. □

Lemma 6 If o ⇝ a_{0} and p(s, a_{0}) ⇝ a_{1}, then o ∗ p ⇝ a_{1} .

Proof: By elim(s, o) = inl a_{0} follows

p^{∗}(s, a_{0}) = can_{l}(s, elim(s, p(s, a_{0}))) = can_{l}(s, inl a_{1}) = inl a_{1}.

Therefore, [can_{l} ∘ elim, p^{∗}](s, inr o) = p^{∗}(s, a_{0}) = inl a_{1} . By equality we get

elim(s, p̄(s, inr o)) = inl a_{1} .

o ∗ p = corec_{p^{∗}}(s, o) = p̄(s, inr o), and therefore elim(s, o ∗ p) = inl a_{1} . □

Lemma 7 If o ⇝ a and p(s, a) ⇝ (c, h), then o ∗ p ⇝ (c, h′) . with h′(r) = p̄(n(s, c, r), inl h(r)).

Proof: By elim(s, o) = inl a follows

p^{∗}(s, o) = can_{l}(s, elim(s, p(s, a))) = can_{l}(s, inr (c, h)) = inr (c, λr.inl h(r)).

Therefore, [can_{l} ∘ elim, p^{∗}](s, inr o) = p^{∗}(s, a) = inr (c, λr.inl h(r)) . By equality we get elim(s, o ∗ p) = elim(s, p̄(s, inr o)) = inr (c, λr.p̄(n(s, c, r), inl h(r))). □

Lemma 8 Let o′ = p̄(s, inl o). Then o ∗ q ≈ o′ ∗ q .

Proof: We show o ∗ q ∼_{n} o′ ∗ q by induction on n. First case: elim(s, o) = inl a First subcase: elim(s, g(s, a)) = inl b. We have [can_{l} ∘ elim, p^{∗}](s, inl o) = inl a , and therefore elim(s, p̄(s, inl o)) = inl a . By Lemma 6 we get elim(s, o′ ∗ q) = inl b = elim(s, o ∗ q) . Second subcase: elim(s, g(s, a)) = inr (c, h) By Lemma 7 we get elim(s, o ∗ q) = inr (c, h′) = elim(s, o′ ∗ q) , where h′(r) = q̄(n(s, c, r), inl h(r)). Second case: elim(s, o) = inr (c, h). By Lemma 3 we get

elim(s, o ∗ q) = inr (c, λr.h(r) ∗ q) .

We have [can_{l} ∘ elim, p^{∗}](s, inl o) = inr (c, λr.inl h(r)) , and therefore elim(s, o′) = inr (c, h′) , where h′(r) = p̄(n(s, c, r), inl h(r)). By Lemma 3 we get

elim(s, o′ ∗ q) = inr (c, λr.h′(r) ∗ q) ,

and by I.H. the claim. □

Lemma 9 If o ⇝ a and p(s, a)) ⇝ (c, h), then

(o ∗ p) ∗ q ≈ o ∗ (λs, a.p(s, a) ∗ q) .

Proof: By Lemma 7 follows elim(s, o∗p) = inr (c, h′) , where h′(r) = p̄(n(s, c, r), inl h(r)). By Lemma 3 follows

elim(s, (o ∗ p) ∗ q) = inr (c, λr.h′(r) ∗ q) .

By elim(s, p(s, a)) = inr (c, h) and Lemma 3 we get

elim(s, p(s, a) ∗ q) = inr (c, λr.h(r) ∗ q) .

By Lemma 7 we get

elim(s, o ∗ (λs, a.p(s, a) ∗ q)) = inr (c, λr.h′′(r)) ,

where h′′(r) = f̄(n(s, c, r), inl h(r) ∗ q), f̄ = \overline{coit}_{f^{∗}}, f = λs, a.p(s, a) ∗ q. By Lemma 2 follows h′′(r) ≈ h(r) ∗ q , and by Lemma 8 h(r) ∗ q ≈ h′(r) ∗ q . □

Lemma 10 If o ⇝ a_{0}, p(s, a_{0}) ⇝ a_{1} and q(s, a_{1}) ⇝ (c, h), then

(o ∗ p) ∗ q ≈ o ∗ (λs, a.p(s, a) ∗ q) .

Proof: By Lemma 6 and Lemma 7 we get elim(s, o ∗ p) = inl a_{1} , elim(s, (o ∗ p) ∗ q) = inr (c, h′) , where h′(r) = q̄(n(s, c, r), inl h(r)). Furthermore, by Lemma 7

elim(s, p(s, a_{0}) ∗ q) = inr(c, h′) ,

and again

elim(s, o ∗ (λs, a.p(s, a) ∗ q)) = inr (c, h′′) ,

where h′′(r) = f̄(n(s, c, r), inl h′(r)), f̄ = \overline{coit}_{f^{∗}}, f = λs, a.p(s, a) ∗ q. By Lemma 2 follows h′′(r) ≈ h′(r) ≈ h(r) . □

Theorem 4

(o ∗ p) ∗ q ≈ o ∗ (λs, a.p(s, a) ∗ q) .

Proof: We show (o ∗ p) ∗ q ∼_{n} o ∗ (λs, a.p(s, a) ∗ q) by induction on n. Case I: elim(s, o) = inr (c, h). Then by Lemma 4

elim(s, (o ∗ p) ∗ q) = inr (c, λr.(h(r) ∗ p) ∗ q) ,

and by Lemma 5

elim(s, o ∗ (λs, a.p(s, a) ∗ q)) = inr (c, λr.h(r) ∗ (λs, a.p(s, a) ∗ q)) .

By I.H. follows the claim. Case II: elim(s, o) = inl a_{0} . This case follows by Lemmata 6, 10, and 9. □

7 Conclusion

We have introduced state dependent interactive programs in Martin-Löf type theory. We have given a model of the corresponding final coalgebras in set theory, and added corresponding rules introducing operations IO : (S → Set) → (S → Set) to Martin-Löf type theory. Using these rules we have introduced the bisimulation relation ≈, and operations ∗, η, and have shown that (IO, ∗, η) is a state-dependent monad w.r.t. ≈.

References

[1] Andrea Asperti, Guiseppe Longo. Categories, Types and Structures. An Introduction to Category Theory for the working computer scientist. Foundations of Computing Series. M.I.T. Press, 1991.

[2] C. D. Team. The Coq proof assistant. reference manual. Available from http://coq.inria.fr/doc/main.html, 2003.

[3] Robert L. Constable et. al. Implementing Mathematics with the Nuprl Proof Development System. Prentice-Hall, Englewood Cliffs, NJ, 1986.

[4] P. Hancock and A. Setzer. The IO monad in dependent type theory. In Electronic proceedings of the workshop on dependent types in programming, Göteborg, 27-28 March 1999, 2000. Available via http://www-sop.inria.fr/oasis/DTP00/Proceedings/ proceedings.html.

[5] Peter Hancock, Anton Setzer. Interactive programs in dependent type theory. In: P. Clote, H. Schwichtenberg: Computer Science Logic. 14th international workshop, CSL 2000. Springer Lecture Notes in Computer Science, Vol. 1862, pp. 317 - 331, 2000.

[6] Z. Luo. Computation and reasoning. Clarendon Press, Oxford, 1994.

[7] Per Martin-Löf. Intuitionistic Type Theory. Bibliopolis, Napoli, 1984.

[8] Bengt Nordström, Kent Peterson, Jan M. Smith. Programming in Martin-Löf’s Type Theory: An Introduction. Clarendon Press, Oxford, 1990.

[9] Lawrence C. Paulson. Natural Deduction Proof as Higher-Order Resolution. technical report 82, University of Cambridge Computer Laboratory, Cambridge, 1985.

[10] Kent Peterson. A Programming System for Type Theory. PMG Memo 21, Chalmers University of Technology, S-412 96 Göteborg, 1982.

[11] R. Pollack. The theory of LEGO. A proof checker for the extended calculus of constructions. PhD thesis, LFCS, Edinburgh, 1994.

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