Proof of the Pipes Laws
This is a formalization in Coq of the Haskell pipes library. Nearly all its functions have been implemented, and the laws mentioned in the documentation proven. It relies on the coq-haskell project, whose aim is to simplify both the transcoding of Haskell types and functions into Coq, and the extraction of proven algorithms back into Haskell.
Much gratitude is given to Gabriel Gonzalez for dialoging with me about this project over the long months of its inception, and for his manual proofs of the laws, which were an excellent reference. Thanks are also due to Paolo Capriotti and Dan Burton, with whom I never interacted, but who where the spiritual fathers of this formalization effort.
Laws proven
43 laws were proven, with 7 requiring a compromise documented below. These
are indicated with bolded leaders in the following list (all of those
are proofs involving either of the functions push or pull).
Klesli category
-
Obligation
functor_1 -
Obligation
functor_2 -
Obligation
applicative_1 -
Obligation
applicative_2(* 3-5 proven by inference *) -
Obligation
monad_1 -
Obligation
monad_2 -
Obligation
monad_4(* 3 proven by inference *)
Respond category
-
Theorem
respond_distrib:(f >=> g) />/ h = (f />/ h) >=> (g />/ h) -
Obligation
(* Right identity: Respond *) -
Obligation
(* Left identity: Respond *) -
Obligation
(* Associativity: Respond *) -
Corollary
respond_zero:pure />/ f = pure
Request category
-
Theorem
request_distrib:h \>\ (f >=> g) = (h \>\ f) >=> (h \>\ g) -
Obligation
(* Right identity: Request *) -
Obligation
(* Left identity: Request *) -
Obligation
(* Associativity: Request *) -
Corollary
request_zero:f \>\ pure = pure
Push category
-
Lemma
push_request:Request x g >>~ f = Request x (g >~> f) -
Lemma
push_m:M g h >>~ f = M (g >~> f) h -
Obligation
(* Right identity: Push *) -
Obligation
(* Left identity: Push *) -
Obligation
(* Associativity: Push *)
Pull category
-
Lemma
pull_respond:f +>> Respond x g = Respond x (f >+> g) -
Lemma
pull_m:f +>> M g h = M (f >+> g) h -
Obligation
(* Right identity: Pull *) -
Obligation
(* Left identity: Pull *) -
Obligation
(* Associativity: Pull *) -
Theorem
push_pull_assoc:(f >+> g) >~> h = f >+> (g >~> h)
Duals
- Theorem
request_id:reflect \o request = respond - Theorem
reflect_distrib:reflect (f x >>= g) = reflect (f x) >>= (reflect \o g) - Theorem
request_comp:reflect \o (f \>\ g) = (reflect \o g) />/ (reflect \o f) - Theorem
respond_id:reflect \o respond = request - Theorem
respond_comp:reflect \o (f />/ g) = (reflect \o g) \>\ (reflect \o f) - Corollary
distributivity:reflect \o (f >=> g) = (reflect \o f) >=> (reflect \o g) - Theorem
zero_law:reflect \o pure = pure - Theorem
involution:reflect \o reflect = id
General theorems
- Theorem
for_yield_f:forP (yield x) f = f x - Theorem
for_yield:forP s yield = s - Theorem
nested_for_a:forP s (fun a => forP (f a) g) = forP (forP s f) g - Theorem
nested_for_b:forP (forP s f) g = forP s (f />/ g)
Prelude functions
-
Theorem
map_id:map id = cat -
Theorem
map_compose:map (g \o f) = map f >-> map g -
Theorem
toListM_each_id:toListM \o each = pure
The Compromise
push and pull are necessarily infinite functions. However, representing
them as co-fixpoints makes some other things impossible (for example,
runEffect must be a fixpoint). So rather than splitting up the development,
a balance was struck. This compromise is three-fold:
-
pushandpullare implemented in terms of "fuel". When fuel is exhausted, they returnPure someDefault. -
An axiom is added such that there is always fuel (i.e.,
fuel > 0). -
A second axiom is added to assert that a "step" of
pushorpullat fuelNbehaves identically to that at fuelN+1. (i.e.,forall n, n > 0 -> push (fuel:=n) = push (fuel:=n.+1))
This allows push and pull to be defined inductively, but used in a context
where the "base case" cannot be reached, making them infinite for the purposes
of proof.
History of this work
2013 Oct 6, Gabriel made his hand-written proofs of the pipes laws
public. Dan Burton commented that someone should mechanize them in Agda.
Gabriel mentioned he had started down that road already, with help from Paolo
Capriotti.
2013 Oct 7, I also began trying to encode the laws in Agda, so Gabriel and
I began discussing the problems of strict positivity regarding the Proxy
type.
2014 Nov 16, after letting the project lie for a while, I started playing
around with teasing Proxy into a functor ProxyF under the free monad.
Gabriel tells me this is exactly what pipes 2.4.0 did, so with that
confirmation I started down the road of how to encode free monads in Coq. I
made the switch to Coq after being inspired by talks at
OPLSS 2014,
and because I was using it for a large project at work.
Over the next few months I read several papers by Conor McBride suggesting the use of container types, even formalizing most of his paper Kleisli Arrows of Outrageous Fortune. This, plus comments made by Paolo Capriotti, gave me much food for thought, although little code was written.
Around 2015 Mar 1 I read an old paper by Venanzio Capretta on Universal Algebra in Type Theory which made container types far more comprehensible to me, thus energizing me to consider this project again.
2015 May 30, After a few weeks of trying various free monad encodings based on container types and universal algebra, I stumbled across a trick Edward Kmett used for his Boehm-Berarducci encoding of the free monad transformer. It turns out that although he did this to improve GHC roles for an applied functor, it also solves the strict positivity issue in Coq!
2015 May 31, With this trick in hand, I was able to transcode most of the
pipes library directly from Haskell, requiring only minor syntactic
variations to adapt it to the Gallina language. With those done, the laws were
relatively easy, falling into place over a two week period.
2015 Jun 12, all of the laws are complete.
So in all it took 1.5 years to learn Coq well enough and to find the right abstraction, and 2 weeks to do the actual work.