I thought I might report a bit about what I’ve been up to with coinduction. Headline: we can set up propositional equality so that every coprogram equals its unfolding, even though that had jolly well better not hold definitionally if we want decidable anything.

What I’ve got is an Agda universe with inductive and coinductive Petersson-Synek trees (also known as Hancock-Setzer interaction structures). Actually, it’s a pair of universes—PROP and SET. Equality is a proposition computed recursively over the structure of sets and elements.

### The underlying sets

Let’s have Zero : Set; _ : One : Set; tt, ff : Two : Set. Let’s have (x : S) -> T. Let’s have record-style Sigma-types Sg S T, with projections fst and snd, handy split functional sp0 (eliminating over Set, sp0 f p = f (fst p) (snd p)) and defined constructor _,_. Let’s have

record Cont (S : Set) : Set1 where

field

Comm : S -> Set

Resp : (s : S) -> Comm s -> Set

next : (s : S) -> (c : Comm s) -> Resp s c -> S

open module Cont’ {S : Set} = Cont {S}

Fun : {S : Set} -> Cont S -> (S -> Set) -> S -> Set

Fun F X s = Sg (Comm F s) \ c -> (r : Resp F s c) -> X (next F s c r)

That’s yer state-indexed interaction structure kit. Now there’s

data IMu {S : Set}(F : Cont S)(s : S) : Set where

con : (c : Comm F s)-> ((r : Resp F s c)-> IMu F (next F s c r)) -> IMu F s

induction : forall {S}(F : Cont S)(P : Sg S (IMu F) -> Set) ->

((s : S)(c : Comm F s)(f : (r : Resp F s c) -> IMu F (next F s c r))->

((r : Resp F s c) -> P (next F s c r , f r)) -> P (s , con c f)) ->

{s : S}(x : IMu F s) -> P (s , x)

induction {S} F P p {s} (con c f) = p s c f \ r -> induction F P p (f r)

Exercise: define the plain fold instead of dependent induction; find out what else you need to reconstruct induction on IMu F from the plain fold on IMu BoxF, where BoxF : Cont (Sg S (IMu F)), a suitably constructed container for inductive hypotheses. But I digress.

Let’s have general codata, with a coconstructor…

codata INu {S : Set}(F : Cont S)(s : S) : Set where

con : (c : Comm F s)-> ((r : Resp F s c)-> INu F (next F s c r)) -> INu F s

…and yer final coalgebra…

out : forall {S}{F : Cont S}{s} -> INu F s -> Fun F (INu F) s

out (con c f) = c , f

…cut into pieces for ease of reference. A coprogram, or interaction structure (client-view) has an initial *command* which it issues…

command : forall {S}{F : Cont S}{s} -> INu F s -> Comm F s

command d = fst (out d)

…and a strategy to *continue* after a response is delivered.

continue : forall {S}{F : Cont S}{s}(d : INu F s)

(r : Resp F s (command d)) -> INu F (next F s (command d) r)

continue d = snd (out d)

Here’s how to write coprograms. First of all, we’ll need the appropriate notion of morphism between indexed sets—the index-respecting functions.

_->>_ : {S : Set} -> (S -> Set) -> (S -> Set) -> Set

A ->> B = (s : _) -> A s -> B s

Then we can say that if F defines a command-response structure, any F-coalgebra gives a way to construct F-coprograms.

unfold : forall {S}{F : Cont S}(A : S -> Set) ->

(A ->> Fun F A) -> A ->> INu F

unfold A g s a = con (fst x) \ r -> unfold A g _ (snd x r) where x = g s a

What’s an F-coalgebra? It’s a choice of *carrier* A : S -> Set, being a kitbag of whatever we need to make progress in a given state, and a function of type A ->> Fun F A, showing how the kit can be used to handle one interaction, leaving the right kit to continue in whatever state results. Such is the basis of sustainable progress: if we have an F-coalgebra, and we have a startup kit, we can manage whatever interaction we’re prompted for.

Note that the above ‘equation’ does *not* hold definitionally, nor can it in a theory with decidable definitional equality—it can **unfold** forever. Rather, it computes only when triggered by **out**. Even so, one should be able to prove this equation. It ain’t gonna happen with the intensional identity type (whose canonical values reflect only the definitional equality).

### A universe of propositions and sets

Or two universes, mutually defined. Or something. I have two sorts…

data Sort : Set where

PROP SET : Sort

…and I give you…

mutual

data Ty : Sort -> Set where

`0′ `1′ : Ty PROP

`2′ : Ty SET

`Pi’ : {K : Sort}(S : Ty SET) (T : [ S ] -> Ty K) -> Ty K

`Sg’ : {K : Sort}(S : Ty K) (T : [ S ] -> Ty K) -> Ty K

`IMu’ : (S : Ty SET)(C : [ S ] -> Ty SET)

(R : (s : [ S ])(c : [ C s ]) -> Ty SET)

(n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->

(s : [ S ]) -> Ty SET

`INu’ : {K : Sort}(S : Ty SET)(C : [ S ] -> Ty K)

(R : (s : [ S ])(c : [ C s ]) -> Ty SET)

(n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->

(s : [ S ]) -> Ty K

`Prf’ : Ty PROP -> Ty SET

[_] : {K : Sort} -> Ty K -> Set

[ `0' ] = Zero

[ `1' ] = One

[ `2' ] = Two

[ `Pi' S T ] = (s : [ S ]) -> [ T s ]

[ `Sg' S T ] = Sg [ S ] \ s -> [ T s ]

[ `IMu' S C R n s ] = IMu {[ S ]}

(record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s

[ `INu' S C R n s ] = INu {[ S ]}

(record {Comm = \ s -> [ C s ]; Resp = \ s c -> [ R s c ]; next = n}) s

[ `Prf' P ] = [ P ]

Philosophy and Software Engineering live in PROP. Electronic Engineering and Computer Science live in SET. Big clue: things in contravariant positions (cruel devils) are always SETs, but covariant positions (polite angels) preserve sort. I could add inductive relations, but I want all prop-based computation to be lazy. We have 0, 1, Pi, Sigma, and lazy coinductive predicates.

I think of these coinductive predicates as being a bit like Mickey Mouse costumes at Disneyland. Their inhabitants are obliged to radiate relentless cheerfulness, no matter how horrid the world’s responses.

### Equality for sets and values

Here’s another steaming mutual definition for your doorstep. It’s SET equality _<->_ and heterogeneous value equality, ASCIIly depicted ! S > s == T > t ! so you can see all the pieces. Intuitively SET equality means ‘accepts the same values as’, which is a rather tighter notion than isomorphism. The value equality has my usual conditional interpretation: values exchangeable if sets equal, otherwise no information.

mutual

Kick off with some handy abbreviations. Here’s ‘given equal values in these sets…’…

funQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP

funQ S T R = `Pi’ S \ s -> `Pi’ T \ t -> ! S > s == T > t ! => R s t

…and here’s ‘these sets are equal, and given equal values in them…’.

DFunQ : (S T : Ty SET) -> ([ S ] -> [ T ] -> Ty PROP) -> Ty PROP

DFunQ S T R = (S <-> T) & funQ S T R

Now, set equality is relentlessly structural with the notable exception of proof sets (which are equal by mutual implication). Keep your eyes peeled for swappings in contravariant positions.

_<->_ : Ty SET -> Ty SET -> Ty PROP

`2′ <-> `2′ = `1′

`Pi’ Sl Tl <-> `Pi’ Sr Tr = DFunQ Sr Sl \ sr sl -> Tl sl <-> Tr sr

`Sg’ Sl Tl <-> `Sg’ Sr Tr = DFunQ Sl Sr \ sl sr -> Tl sl <-> Tr sr

`IMu’ Sl Cl Rl nl sl <-> `IMu’ Sr Cr Rr nr sr =

! Sl > sl == Sr > sr ! &

DFunQ Sl Sr \ sl sr ->

DFunQ (Cl sl) (Cr sr) \ cl cr ->

DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->

! Sl > nl sl cl rl == Sr > nr sr cr rr !

`INu’ Sl Cl Rl nl sl <-> `INu’ Sr Cr Rr nr sr =

! Sl > sl == Sr > sr ! &

DFunQ Sl Sr \ sl sr ->

DFunQ (Cl sl) (Cr sr) \ cl cr ->

DFunQ (Rr sr cr) (Rl sl cl) \ rr rl ->

! Sl > nl sl cl rl == Sr > nr sr cr rr !

`Prf’ Pl <-> `Prf’ Pr = (Pl => Pr) & (Pr => Pl)

_ <-> _ = `0′

Value equality is as tested for 2, extensional for functions, componentwise for pairs, computed recursively for inductive data, defined as bisimulation for codata, and trivial for proofs. It’s also trivial when the types are obviously different.

!_>_==_>_! : (S : Ty SET) -> [ S ] -> (T : Ty SET) -> [ T ] -> Ty PROP

! `2′ > tt == `2′ > tt ! = `1′

! `2′ > tt == `2′ > ff ! = `0′

! `2′ > ff == `2′ > tt ! = `0′

! `2′ > ff == `2′ > ff ! = `1′

! `Pi’ Sl Tl > fl == `Pi’ Sr Tr > fr ! =

funQ Sl Sr \ sl sr -> ! Tl sl > fl sl == Tr sr > fr sr !

! `Sg’ Sl Tl > pl == `Sg’ Sr Tr > pr ! =

! Sl > fst pl == Sr > fst pr ! &

! Tl (fst pl) > snd pl == Tr (fst pr) > snd pr !

! `IMu’ Sl Cl Rl nl sl > dl == `IMu’ Sr Cr Rr nr sr > dr ! = muQ sl dl sr dr where

muQ : (sl : [ Sl ]) -> [ `IMu' Sl Cl Rl nl sl ] ->

(sr : [ Sr ]) -> [ `IMu' Sr Cr Rr nr sr ] -> Ty PROP

muQ sl (con cl fl) sr (con cr fr) =

! Cl sl > cl == Cr sr > cr ! &

`Pi’ (Rl sl cl) \ rl -> `Pi’ (Rr sr cr) \ rr ->

! Rl sl cl > rl == Rr sr cr > rr ! =>

muQ (nl sl cl rl) (fl rl) (nr sr cr rr) (fr rr)

Let’s do this one slowly. Equality between coprograms…

! `INu’ Sl Cl Rl nl sl > dl == `INu’ Sr Cr Rr nr sr > dr ! =

…is a simulation relation, indexed by both state-of-world-and-configuration-of-coprogram pairs.

`INu’ (`Sg’ Sl (`INu’ Sl Cl Rl nl) & `Sg’ Sr (`INu’ Sr Cr Rr nr))

We’re *cheerful* if the coprograms issue equal commands.

(sp0 (sp0 \ sl dl -> sp0 \ sr dr ->

! Cl sl > command dl == Cr sr > command dr !))

A response is a pair of equal responses for each coprogram. If some little b**tard kicks Mickey in the shin, his sister has to kick Minnie in the corresponding shin.

(sp0 (sp0 \ sl dl -> sp0 \ sr dr q ->

`Sg’ (Rl sl (command dl)) \ rl -> `Sg’ (Rr sr (command dr)) \ rr ->

`Prf’ ! Rl sl (command dl) > rl == Rr sr (command dr) > rr !))

The simulation evolves by evolving both processes.

(sp0 (sp0 \ sl dl -> sp0 \ sr dr cq -> sp0 \ rl -> sp0 \ rr rq ->

(nl sl (command dl) rl , continue dl rl) ,

(nr sr (command dr) rr , continue dr rr) ))

And the simulation starts in the initial configuration for both.

((sl , dl) , (sr , dr))

Phew!

! `Prf’ y > s == `Prf’ y’ > t ! = `1′

! _ > _ == _ > _ ! = `1′

As ever, I postulate the reflexivity of these things, safe in the knowledge that I’m only making extensionally valid assumptions, and that computation on proofs is lazy.

postulate Resp : (S : Ty SET)(P : [ S ] -> Ty SET) ->

[ `Prf' (funQ S S \ x y -> P x <-> P y) ]

postulate refl : (S : Ty SET)(s : [ S ]) -> [ `Prf' ! S > s == S > s ! ]

### Coercion?

What I ought to do now is show how to transport values between equal sets. Given that equality of sets is structural, with covariant twists reflecting the flow of information, we’ve got everything we need. It’s an interesting exercise!

### Unfolding

But what I really want to check is that we can see how things unfold. I need a quick helper just to give the code for the set delivered by the **out** function.

Guts : (S : Ty SET)

(C : [ S ] -> Ty SET)

(R : (s : [ S ])(c : [ C s ]) -> Ty SET)

(n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->

(s : [ S ]) -> Ty SET

Guts S C R n s = `Sg’ (C s) \ c -> `Pi’ (R s c) \ r -> `INu’ S C R n (n s c r)

And now let’s prove…

conOutLaw : (S : Ty SET)(C : [ S ] -> Ty SET)

(R : (s : [ S ])(c : [ C s ]) -> Ty SET)

(n : (s : [ S ])(c : [ C s ])(r : [ R s c ]) -> [ S ]) ->

(s : [ S ])(x : [ `INu' S C R n s ]) ->

[ `Prf'

! `INu' S C R n s > x ==

`INu' S C R n s > con (command x) (continue x) ! ]

…that everything equals its unfolding. Deep breath.

conOutLaw S C R n s x = unfold

Gosh! What’s the carrier? We need that both sides are in the same state *and identified by out*.

(\ sxsx ->

let sx0 = fst sxsx ; s0 = fst sx0 ; x0 = snd sx0 ;

sx1 = snd sxsx ; s1 = fst sx1 ; x1 = snd sx1

in [ `Prf' (! S > s0 == S > s1 ! &

! Guts S C R n s0 > out x0 == Guts S C R n s1 > out x1 !) ])

Now, how do we show that this happy situation persists forthwith? First, we get state-configuration pairs, in equal states, and identified by out, so they have equal commands and continues. I get to do a lot of unpacking.

(\ sxsx scfq ->

let sx0 = fst sxsx ; s0 = fst sx0 ; x0 = snd sx0

sx1 = snd sxsx ; s1 = fst sx1 ; x1 = snd sx1

sq = fst scfq ; cfq = snd scfq

c0 = command x0 ; c1 = command x1 ; cq = fst cfq

f0 = continue x0 ; f1 = continue x1 ; fq = snd cfq

in

The commands are indeed the same!

cq ,

And given equal responses…

sp0 \ r0 -> sp0 \ r1 rq ->

…we get equal next-states-of-the-world…

let n0 = n s0 c0 r0 ; n1 = n s1 c1 r1

nq = refl (`Pi’ S \ s -> `Pi’ (C s) \ c -> `Pi’ (R s c) \ _ -> S) n

s0 s1 sq c0 c1 cq r0 r1 rq

in nq ,

…and equal continuing processes, as shown by **out**

refl (`Pi’ S \ s -> `Pi’ (`INu’ S C R n s) \ _ -> Guts S C R n s)

(\ s x -> out x)

n0 n1 nq (f0 r0) (f1 r1) (fq r0 r1 rq))

We know our starting situation, and it’s easy to show that our initial conditions are satisfied.

_ (refl S s , refl (Guts S C R n s) (out x))

Thank goodness for that.

Exercise: use this result to establish a dependent case analysis principle for codata, eliminating over Ty SET.

### So what?

So the observational equality setup means that we can work with bisimulation as our substitutive equality for codata. Although our computational presentation of coinduction is weak (plain old unfold, plain old out), reasoning up to bisimulation is enough to recover (and give a suitable evidence language to) the dependent reasoning principles we need. We can plug the gap left by Agda without suffering the subject reduction issue inherent in Coq’s overly intensional presentation. Or, in other words, it works.

### Requiem

Would we even be thinking these thoughts without Robin Milner? Rest in peace.

What does

`Sg’ Sl (`INu’ Sl Cl Rl nl) & `Sg’ Sr (`INu’ Sr Cr Rr nr)

mean?

I can not define _=>_ and _&_.

For _=>_ I got to

_=>_ : Ty PROP -> Ty PROP -> Ty PROP

`0′ => b = `1′

`1′ => b = b

`Pi’ S T => b = {!!}

`Sg’ S T => b = {!!}

`INu’ S C R n s => b = {!!}

OK, Maybe I have got it:

_=>_ : Ty PROP -> Ty PROP -> Ty PROP

`0′ => b = `1′ — is this useful?

`1′ => b = b — is this useful?

a => b = `Pi’ (`Prf’ a) \ _ -> b

_&_ : {k : Sort} -> Ty k -> Ty k -> Ty k

`0′ & _ = `0′ — is this useful?

`1′ & x = x — is this useful?

a & b = `Pi’ `2′ (pp a b)

pp : {X : Set} -> X -> X -> Two -> X

pp a b tt = a

pp a b ff = b

Now I have

_=>_ : Ty PROP -> Ty PROP -> Ty PROP

a => b = `Pi’ (`Prf’ a) \ _ -> b

_&_ : {k : Sort} -> Ty k -> Ty k -> Ty k

a & b = `Sg’ a \ n2 -> b

Still I am not sure that it is right.

I realised I need a deeper insight…

Oh. I found the sources in the Agda mailing list archives:

https://lists.chalmers.se/pipermail/agda/2010/001696.html

I apologize for the disturbance.

Hi divip. I’m sorry I took my eye off the blog. You seem to have found your way in the end. => and & are, as you found, just a notational convenience for nondependent special cases of Pi and Sg.