The IO Monad in Dependent Type Theory

Peter Hancock, Edinburgh, Scotland

              pgh@dcs.ed.ac.uk

Anton Setzer, Uppsala, Sweden

              setzer@math.uu.se

April 13, 1999

1. Definition of the IO Monad in type theory.

2. While, redirect and equality.

3. Normalizing version.

4. State-dependent IO.

5. Parallelism, Nondeterminism.

1. Definition of the IO Monad in Type Theory

Direction in Functional Programming

Design of programming languages based on dependent types.

Theoretical Problems:

- Equality. Hard.

- Practical structuring of programs. ∗ Local variables.

∗ Record types. Unproblematic.

- Polymorphism, subtyping.

- Input/output.

Models for input/output:

- Streams.

Difficulties with infinitely many input/output

devices Timing between input/output depends

on evaluation strategy.

- The IO-monad.

Monad

A monad is a triple (M, η, ∗), where

- M : Set → Set ,

- η : (A : Set , a : A) → M(A),

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

with abbreviations η_{a} := η_{a}^{A} := η(A, a), p ∗ q := p ∗_{A,B} q := ∗(A, B, p, q),

s.t. for A, B, C : Set , a : A, p : M(A),

q : A → M(B), r : B → M(C):

- η_{a} ∗ q = q(a).

- p ∗ λx.η_{x} = p.

- (p ∗ q) ∗ r = p ∗ λx.(q(x) ∗ r).

IO-Monad

IO-Monad = monad (IO, η, ∗) with interpretation:

- IO(A) = set of interactive programs which, if terminating, return an element a : A.

- η_{a} = program with no interaction, returns a.

- ∗ = composition of programs.

Additional elements added like input (d, A) : IO(A)

input from device d an element a : A and return a.

output (d, A) : A → IO(1)

for a : A output a on device d

and return <> : 1.

IO-Monad in Haskell: Small part of the program interactive. Large part purely functional.

Problems of the IO-Monad:

- ∗ cannot be a constructor.

⇒ Monads do not fit into the conceptual framework of Martin-Löf type theory.

- Equalities can hold only extensionally.

The IO-tree

A world w is a pair (C, R) s.t.

- C : Set (Commands).

- R : C → Set (responses to a command).

Assume w = (C, R) a world.

IO_{w}(A) or shorter IO(A) is the set of (possibly non-well-founded) trees with

- leaves in A.

- nodes marked with elements of C.

- nodes marked with c have branching degree R(c).

\frac{A : Set}{IO_{w}(A) : Set}

\frac{a : A}{leaf (a) : IO_{w}(A)}

\frac{c : C p : R(c) → IO_{w}(A)}{do(c, p) : IO_{w}(A)}

Note: IO_{w}(A) now parametrized w.r.t. w.

New operation execute :

Status:

- Like function “reduce to canonical form”.

- No construction inside type theory.

Let w_{0} be a fixed world (real commands).

execute applied to p : IO_{w_{0}}(A) does the following:

- It reduces p to canonical form.

- If p = leaf (a) it terminates and returns a.

- If p = do(c, q), then it - carries out command c;

- interprets the result as an element r : R(c);

- then continues with q(r).

Essentially normalization of p but with interaction with the real world.

Definition of η, ∗

η_{a} = leaf (a). leaf (a) ∗ q = q(a). do(c, p) ∗ q = do(c, λx.(p(x) ∗ q)). For well-founded trees monad laws provable w.r.t. extensional equality. Additional function interact : interact : (c : C) → IO(R(c)). interact (c) = do(c, λx.leaf (x)). interact (c) executes command c and returns the result.

2. While, Redirect, Equality

2.1. While

Problem:

- Interactive programs should possibly have infinitely many interactions (no termination after finite amount of time).

Add while-loop:

Assume:

- a set B

- an initial value b : B

- q : B → (IO(A) + IO(B)).

while _{B}(b, q) : IO(A) does the following:

- If q(b) is in IO(B) then it runs this program. If it terminates with leaf b′, it continues with while _{B}(b′, q).

- If q(b) is in IO(A) then it run this program. When it stops it returns the result.

Problem: Black hole recursion for trees which consist of leaves.

Therefore define set of trees which have at least one command at the root:

\frac{A : Set}{IO^{+} (A) : Set}  \frac{a : IO^{+} (A)}{a^{−} : IO(A)}

\frac{c : C p : R(c) → IO(A)}{do^{+} (c, p) : IO^{+} (A)}

do^{+} (c, p)^{−} = do(c, p)

Definition of while

Assume A, B : Set .

\frac{b : B p : B → (IO(A) + IO^{+} (B))}{while _{B}(b, p) : IO(A)}

• If p(b) = i(q) then while (b, p) = q

• If q(b) = j(q) then while (b, p) = q^{−} ∗ λb′.while (b′, p)

2.2. Redirect

Assume

- w = (C, R), w′ = (C′, R′) are worlds.

- A : Set ,

- p : IO_{w}(A).

- q : (c : C) → IO _{w′}^{+}(R(c)).

Define redirect (p, q) : IO_{w′}(A):

redirect (leaf (a), q) = leaf (a). redirect (do(c, p), q) = q(c)^{−}∗λr.redirect (p(r), q).

2.3. Equality

Equality corresponding to extensional equality on non-well-founded trees: Bisimulation (definition according I. Lindström):

\frac{p : IO(A) q : IO(A)}{Eq(p, q) : Set}

\frac{p : IO(A)  q : IO(A)  n : N}{Eq′(n, p, q) : Set}

Eq(p, q) = ∀n : N.Eq′(n, p, q). Eq′(n, leaf (a), do(c, p)) = Eq′(n, do(c, p), leaf (a)) = ⊥ Eq′(n, leaf (a), leaf (a′)) = I(A, a, a′). Eq′(0, do(c, p), do(c′, p′)) = I(C, c, c′). Eq′(S(n), do(c, p), do(c′, p′)) =

Σq : I(C, c, c′).∀r : R(c).Eq(n, p(r), p′(⋯ r ⋯)).

• Eq is the natural extension of extensional equality to non-well-founded trees (if we take for I extensional equality).

• Monad laws w.r.t. Eq are provable.

• Two programs are equal w.r.t. Eq, if their IO-behaviour is identical. ⇒ Extensionally, for every IO-behaviour there

is exactly one program. ⇒ IO-tree = suitable model of IO.

Problem: No normalization

Let A = B = C = N, R(c) arbitrary. Assume f : N → N. p := λn.do(f(n), λx.leaf (n + 1)) : N → IO(B) q := λp.j(p^{+} ) : N → (IO(A) + IO^{+} (B)).

while (0, q)

⟶ while ′(p(0), q)
⟶ do(f(0), λx.while ′(leaf (1), q))
⟶ do(f(0), λx.while ′(p(1), q))
⟶ do(f(0), λx.do(f(1), λy.while ′(leaf (2), q)))
⟶ ⋯
⟶ do(f(0), λx.do(f(1), λy.do(f(2), λz. · · ·)))

Consequence: with intensional equality typechecking undecidable.

3. Normalizing version

Add while as a constructor. Problem: while refers to IO(A) + IO^{+} (B). Therefore while needs to be defined simultaneously for all sets. Restrict A, B to be elements of a universe. (Restriction of B would suffice). Assume U : Set , T : U → Set . Assume w = (C, R) is a world. For Â : U let A := T(Â) similarly for B̂, Ĉ.

\frac{Â : U}{IO_{w}(Â) : Set}  \frac{Â : U}{IO _{w}^{+} (Â) : Set}

\frac{p : IO^{+} (Â)}{p^{−} : IO(Â)}

\frac{a : A}{leaf (a) : IO(Â)}

\frac{c : C p : R(c) → IO(Â)}{do^{(+)} (c, p) : IO^{(+)} (Â)}

do^{+} (c, p)^{−} = do(c, p)

\frac{B̂ : U  b : B  p : B → (IO(Â) + IO^{+} (B̂))}{while B̂(b, p) : IO(Â)}

(The rule with occurrences of (+) denotes two rules: One where everywhere (+) is replaced by + and one where (+) is omitted).

Let IO _{wf}^{(+)} (A) be the set IO^{(+)} (A) as defined in this section.

Let IO _{nonwf}^{(+)} (A) be IO^{(+)} (A) as defined before.

Define emb (+) ; Â : IO _{wf}^{(+)} (Â) → IO _{nonwf}^{(+)} (A):

• emb (leaf (a)) = leaf (a).

• emb ^{(+)} (do^{(+)} (c, p)) = do^{(+)} (c, λx.emb (p(x))).

• emb (while B̂(b, p)) =

while _{B}(b, λx.emb ′(p(x))) with emb ′(i(p)) = i(emb (p)),

emb ′(j(p)) = j(emb ^{+} (p)).

Now η, ∗, redirect , Eq on IO_{nonwf} (A) can be mimiced by corresponding operations on IO_{wf} (A).

Decompose:

Define decompose : IO_{wf} (A) →

A + Σc : C.(R(c) → IO_{wf} (A))

s.t.

If emb (p) = leaf (a),

decompose (p) = i(a). If emb (p) = do(c, q),

then decompose (p) = j(c, q′) where q′ s.t. emb (q′(x)) = q(x).

Execute(p) does now the following:

- If decompose (p) = i(a), then terminate with result a.

- If decompose (p) = j(<c, q>), then carry out command c, get response r and continue with q(r).

Result:

• All derivable terms are strongly normalizing.

• Therefore in the beginning and after every IO-command execute will terminate either completely or carry out the next IOcommand.

• However, execute might carry out infinitely many IO-commands.

• Notion of “strongly-normalizing IO-programs”.

4. State-dependent IO

For simplicity we will work with non-well-founded trees.

Now let set of commands depend on the state of knowledge.

States = “objective knowledge” about the devices.

The state is influenced by commands, e.g.

- open a new window.

- switch on a printer.

- test whether the printer is switched on.

A world is now a quadruple (S, C, R, ns) s.t.

- S : Set (set of states).

- C : S → Set (set of commands).

- R : (s : S, C(s)) → Set (set of responses).

- ns : (s : S, c : C(s), r : R(c, s)) → S (next state).

Let w = (S, C, R, ns) be a world.

\frac{A : S → Set s : S}{IO(A, s) : Set}

Assume A : S → Set .

\frac{s : S a : A(s)}{leaf (a) : IO(A, s)}

s : S c : C(s)

p : (r : R(s, c)) → IO(A, ns(s, c, r)) do(c, p) : IO(A, s)

\frac{s : S a : A(s)}{η̃_{a}^{A}(s) : IO(A, s)}

η̃_{a}^{A}(s) = leaf (a).

s : S
p : IO(A, s)
B : S → Set

q : (s : S, a : A(s)) → IO(B, s) p ˜∗_{s}^{A,B} q : IO(B, s)

do(c, p) ˜∗ q = do(c, λr.(p(r) ˜∗ q)). leaf (a) ˜∗ q = q(s, a).

Corresponding monad

Consider IO : (S → Set ) → (S → Set ). η : (A : S → Set , a : (s : S) → A(s)) → IO(A), η_{a}^{A} := λs.η̃_{a(s)}^{A}(s). μ : (A : S → Set , p : IO(IO(A)) → IO(A), μ^{A}(p) := λs.(p(s) ˜∗_{s}^{IO(A),A} (λs, q.q)). map : (A, B : S → Set ,

f : (s : S, a : A(s)) → B(s),

p : IO(A))
→ IO(B),

map ^{A,B}(f, p) := λs.(p(s)˜∗_{s}^{A,B}λs, a.leaf (f(s, a))). This yields a monad on presheaves over the discrete category S.

Corresponding ∗-operation:

∗ : (A, B : S → Set , p : IO(A), q : (s : S, A(s)) → IO(B(s))) → IO(B),

(p ∗^{A,B} q)(s) = p(s) ˜∗_{s}^{A,B} q.

While

IO^{+} (A, s) defined as before.

B : S → Set

s : S
b : B(s)

q : (s : S, b : B(s)) → (IO(A, s) + IO^{+} (B, s))

while _{B,s}(b, q) : IO(A, s)

If q(s, b) = i(p) then

while _{B,s}(b, q) = p. If q(s, b) = j(p) then

while _{B,s}(b, q) = p^{−} ∗ λs′, b′.while _{B,s′}(b′, q).

Redirect

Assume

- w = (S, C, R, ns), w′ = (S′, C′, R′, ns′) are worlds.

- A : S → Set ,

- Rel : S → S′ → Set ,

- q : (s : S, c : C(s), s′ : S′, Rel(s, s′)) → IO _{w′}^{+}(λs′′.(Σr : R(s, c).Rel(ns(s, c, r), s′′)), s′),

- s : S,

- s′ : S′,

- rel : Rel(s, s′),

- p : IO_{w}(A, s).

Define redirect _{w,w′}(A, Rel, q, s, s′, rel, p)

: IO_{w′}(λs′′.Σs : S.(Rel(s, s′′) ∧ A(s))) by redirect _{w,w′}(A, Rel, q, s, s′, rel, leaf (a)) =

leaf (<s, rel, a>).

redirect _{w,w′}(A, Rel, q, s, s′, rel, do(c, p)) = q(s, c, s′, rel)^{−}∗

λs′′, <r, rel′>.

redirect _{w,w′}(A, Rel, q, ns(s, c, r), s′′, rel′, p(r)).

execute

Let w_{0} = (S_{0}, C_{0}, R_{0}, ns_{0}) be a standard world, s_{0} : S be a state which corresponds to the existence of knowledge about the environment. Assume p : IO_{w_{0}}(A, s_{0}).

execute applied to p normalizes p by carrying out commands as before.

(If one has a program which requires a certain state s of the environment, compose before it a program, which starts from the initial state, and making tests of the environment tries to move to state s; if it fails it terminates. Execute the result).

5. Parallelism, Non-determinism

Non-determinism Additional constructor of IO, of the same form as do. R(s, c) is now the answer of the oracle, which does non-deterministic choice. Modify IO^{+} (A, s) s.t. every execution has at least one “real” command.

Parallelism Add to our world: A set of parallel commands

NC : S → Set , an index set of processes for every command

ND : (s : S, c : NC(s)) → Set , a world for every process

Nw : (s : S, c : NC(s), d : ND(s, c))

→ world

a result type of each process

NR : (s : S, c : NC(s), d : ND(s, c),

s′ : Nw(s, c, d).S)
→ Set ,

a next state depending on the final states of all processes,

Nns : (s : S,

c : NC(s),

s′ : (d : ND(s, c)) → NW (s, c, d).S, r : (d : ND(s, c)) → NR(s, c, d, s′(d)))

→ S.

Processes can communicate via commands in their worlds.

New constructor

parallel : (s : S, c : NC(s), p : (d : ND(s, c)) → IO_{w(s,c,d)}(NR(s, c, d)), np : (s′ : (d : ND(s, c)) → w(s, c, d).S,

r : (d : ND(s, c)) → NR(s, c, d, s′(d))) → IO_{w}(A, ns(s, c, s′, r)))

→ IO_{w}(A, s).

Further construction: Parallelism with dependency only on the first process which stops.

(Then Nns will have type: Nns : (s : S, c : NC(s), d : ND(s, c),

s′ : NW (s, c, d).S, r : NR(s, c, d, s′))

→ S).

and parallel is defined accordingly).

Conclusion

• Inductive definition of the IO-monad by IOtrees.

• Parameterized over worlds (over input/output).

• New constructions: run, redirect.

• Extensions to state-dependent command sets.

• Nondeterminism, parallelism.