Skip to content

Category laws for pipes

Paolo Capriotti edited this page Jul 8, 2012 · 3 revisions

Equality of Pipes

Consider the equivalence relation on the initial algebra identified by the Pipe ADT, generated by the following equation:

Await k j1 h1 w == Await k j2 h2 w

where h1 and h2 are such that, for all exceptions e,

throwP e >+> h1 e == throwP e >+> h2 e

recursively. Similarly, j1 and j2 must satisfy, for each u,

return u >+> j1 u == return u >+> j2 u

Two such handlers h1 and h2 (or continuations j1 and j2) are said to be equivalent.

In the following, we work in the quotient set of pipes modulo this equivalence relation.

Note that equivalent handlers are not always identified, since, in general,

M s m h1 /= M s m h2

even if h1 and h2 are equivalent.

Preliminary lemmas

Lemma 1: protect [] p == p

Proof: immediate, by induction on p.

Lemma 2: Await k j h w == Await k (\u -> return u >+> j u) (\e -> throwP e >+> h e) w

Proof: we need to prove that h and \e -> throwP e >+> h e are equivalent handlers, and that j and \u -> return u >+> j u are equivalent continuations.

By definition of equivalence, we need to show that, for all e, u:

throwP e >+> h e == throwP e >+> (throwP e >+> h e)
return u >+> j u == return u >+> (return u >+> j u)

Proceeding by induction on h e, the only interesting cases are

h e = Await k0 j0 h0 w
j u = Await k0 j0 h0 w

where we get

throwP e >+> (throwP e >+> Await k0 j0 h0 w)
== (composition)
throwP e >+> (throwP e >+> protect [] (h0 e))
== (lemma 1)
throwP e >+> (throwP e >+> h0 e)
== (induction)
throwP e >+> h0 e
== (lemma 1)
throwP e >+> protect [] (h0 e)
== (composition)
throwP e >+> Await k0 j0 h0 w

return u >+> (return u >+> Await k0 j0 h0 w)
== (composition)
return u >+> (return u >+> protect [] (j0 u))
== (lemma 1)
return u >+> (return u >+> j0 u)
== (induction)
return u >+> j0 u
== (lemma 1)
return u >+> protect [] (j0 u)
== composition)
return u >+> Await k0 j0 h0 w

Lemma 3: protect w idP == idP

Proof:

protect w idP
== (definition of idP)
protect w (Await (\x -> Yield x idP []) return throwP [])
== (definition of protect)
Await (\x -> Yield x idP []) return throwP []
== (definition of idP)
idP

Lemma 4: protect w (p1 >+> p2) == protect w p1 >+> protect w p2

Identity laws

Left identity law: p >+> idP == p

Proof: by cases:

Pure r w >+> idP
== (composition)
Pure r w >+> protect w (return r)
== (definition of protect)
Pure r w >+> Pure r w
== (composition)
Pure r w

Throw e w >+> idP
== (composition)
Throw e w >+> protect w (throwP e)
== (definition of protect)
Throw e w >+> Throw e w
== (composition)
Throw e w

Await k j h w >+> idP
== (composition)
Await (\a -> k a >+> idP)
      (\u -> j u >+> idP)
      (\e -> h e >+> idP) w
== (induction)
Await (\a -> k a) (\u -> j u) (\e -> h e) w
== (extensionality)
Await k j h w

Yield x p' w >+> idP
== (definition of idP)
Yield x p' w >+> Await (\x -> Yield x idP []) return throwP []
== (composition)
p' >+> protect w (Yield x idP [])
== (definition of protect)
p' >+> Yield x (protect w idP) w
== (lemma 3)
p' >+> Yield x idP w
== (composition)
Yield x (p' >+> idP) w
== (induction)
Yield x p' w

M s m h >+> idP
== (composition)
M s (m >>= \p' -> return (p' >+> idP)) (\e -> h e >+> idP)
== (induction)
M s (m >>= \p' -> return p') (\e -> h e)
== (extensionality)
M s (m >>= return) h
== (monad law 2)
M s m h

Right identity law: idP >+> p == p

Proof: by cases:

idP >+> Pure r w
== (composition)
Pure r w

idP >+> Throw e w
== (composition)
Throw e w

idP >+> Await k j h w
== (definition of idP)
Await (\x -> Yield x idP []) return throwP [] >+> Await k j h w
== (composition)
Await (\x -> Yield x idP [] >+> Await k j h w)
      (\u -> return u >+> Await k j h w)
      (\e -> throwP e >+> Await k j h w) w
== (composition + lemma 1)
Await (\x -> idP >+> k x)
      (\u -> return u >+> j u)
      (\e -> throwP e >+> h e) w
== (induction + lemma 2)
Await (\x -> k x) (\u -> j u) (\e -> h e) w
== (extensionality)
Await k j h w

idP >+> Yield x p' w
== (composition)
Yield x (idP >+> p') w
== (induction)
Yield x p' w

idP >+> M s m h
== (composition)
M s (m >>= \p' -> return (idP >+> p')) (\e -> idP >+> h e)
== (induction)
M s (m >>= \p' -> return p') (\e -> h e)
== (extensionality)
M s (m >>= return) h
== (monad law 2)
M s m h

Associativity of composition

Associativity: p1 >+> (p2 >+> p3) == (p1 >+> p2) >+> p3

Proof: by cases:

last pipe /= Await.

p1 >+> (p2 >+> Pure r w)
== (composition)
p1 >+> Pure r w
== (composition)
Pure r w
== (composition)
(p1 >+> p2) >+> Pure r w

p1 >+> (p2 >+> Throw e w)
== (composition)
p1 >+> Throw e w
== (composition)
Throw e w
== (composition)
(p1 >+> p2) >+> Throw e w

p1 >+> (p2 >+> Yield x p3' w)
== (composition)
p1 >+> Yield x (p2 >+> p3') w
== (composition)
Yield x (p1 >+> (p2 >+> p3')) w
== (induction)
Yield x ((p1 >+> p2) >+> p3') w
== (composition)
(p1 >+> p2) >+> Yield x p3' w

p1 >+> (p2 >+> M s m h)
== (composition)
p1 >+> (M s (m >>= \p3' -> return (p2 >+> p3')) (\e -> p2 >+> h e))
== (composition)
M s (m >>= \p3' -> return (p2 >+> p3') >>= \p3'' -> return (p1 >+> p3''))
    (\e -> p1 >+> (p2 >+> h e))
== (monad laws + induction)
M s (m >>= return ((p1 >+> p2) >+> p3')) (\e -> (p1 >+> p2) >+> h e)
== (composition)
(p1 >+> p2) >+> M s m h

last pipe p3 = Await { }, middle pipe /= Await:

p1 >+> (Pure r w >+> Await k j h w')
== (composition)
p1 >+> (Pure r w >+> protect w (j r))
== (induction)
(p1 >+> Pure r w) >+> protect w (j r)
== (composition)
Pure r w >+> protect w (j r)
== (composition)
Pure r w >+> Await k j h w'
== (composition)
(p1 >+> Pure r w) >+> Await k j h w'

p1 >+> (Throw e w >+> Await k j h w')
== (composition)
p1 >+> (Throw e w >+> protect w (h e))
== (induction)
(p1 >+> Throw e w) >+> protect w (h e)
== (composition)
Throw e w >+> protect w (h e)
== (composition)
Throw e w >+> Await k j h w'
== (composition)
(p1 >+> Throw e w) >+> Await k j h w'

p1 >+> (Yield x p2' w >+> Await k j h w')
== (composition)
p1 >+> (p2' >+> protect w (k x))
== (induction)
(p1 >+> p2') >+> protect w (k x)
== (composition)
Yield x (p1 >+> p2') w >+> Await k j h w'
== (composition)
(p1 >+> Yield x p2' w) >+> Await k j h w'

p1 >+> (M s m h >+> p3)
== (composition)
p1 >+> M s (m >>= \p2' -> return (p2' >+> p3))
           (\e -> h e >+> p3)
== (composition)
M s (m >>= \p2' -> return (p2' >+> p3) >>= \p2'' -> return (p1 >+> p2''))
    (\e -> p1 >+> (h e >+> p3))
== (monad laws + induction)
M s (m >>= \p2' -> return ((p1 >+> p2') >+> p3))
    (\e -> (p1 >+> h e) >+> p3)
== (monad laws)
M s (m >>= \p2' -> return (p1 >+> p2') >>= \p2'' -> return (p2'' >+> p3))
    (\e -> (p1 >+> h e) >+> p3)
== (composition)
M s (m >>= \p2' -> return (p1 >+> p2')) (\e -> (p1 >+> h e)) >+> p3
== (composition)
(p1 >+> M s m h) >+> p3

last pipe p3 = Await _ _ _ w'', middle pipe p2 = Await { }:

Pure r w >+> (Await k j h w' >+> p3)
== (composition)
Pure r w >+> Await (\x -> k x >+> p3)
                   (\u -> j u >+> p3)
                   (\e -> h e >+> p3)
                   (w' ++ w'')
== (composition)
Pure r w >+> protect w (j r >+> p3)
== (lemma 4)
Pure r w >+> (protect w (j r) >+> protect w p3)
== (induction + definitions of protect)
(Pure r w >+> protect w (j r)) >+> p3
== (composition)
(Pure r w >+> Await k j h w') >+> p3

Throw e w >+> (Await k j h w' >+> p3)
== (composition)
Throw e w >+> Await (\x -> k x >+> p3)
                    (\u -> j u >+> p3)
                    (\e -> h e >+> p3)
                    (w' ++ w'')
== (composition)
Throw e w >+> protect w (h e >+> p3)
== (lemma 4)
Throw e w >+> (protect w (h e) >+> protect w p3)
== (induction + definition of protect)
(Throw e w >+> protect w (h e)) >+> p3
== (composition)
(Throw e w >+> Await k j h w') >+> p3

Yield x p1' w >+> (Await k j h w' >+> p3)
== (composition)
Yield x p1' w >+> Await (\x -> k x >+> p3)
                        (\u -> j u >+> p3)
                        (\e -> h e >+> p3)
                        (w' ++ w'')
== (composition)
p1' >+> protect w (k x >+> p3)
== (lemma 4)
p1' >+> (protect w (k x) >+> p3)
== (induction)
(p1' >+> protect w (k x)) >+> p3
== (composition)
(Yield x p1' w >+> Await k j h w') >+> p3

Await k1 j1 h1 w >+> (p2 >+> p3)
== (composition)
Await (\x -> k1 x >+> (p2 >+> p3))
      (\u -> j1 u >+> (p2 >+> p3))
      (\e -> h1 e >+> (p2 >+> p3))
      (w ++ w' ++ w'')
== (induction)
Await (\x -> (k1 x >+> p2) >+> p3)
      (\u -> (j1 u >+> p2) >+> p3)
      (\e -> (h1 e >+> p2) >+> p3)
      (w ++ w' ++ w'')
== (composition)
Await (\x -> k1 x >+> p2)
      (\u -> j1 u >+> p2)
      (\e -> h1 e >+> p2) 
      (w ++ w') >+> p3
== (composition)
(Await k1 j1 h1 w >+> p2) >+> p3
Something went wrong with that request. Please try again.