pipesis the only that does not have a test suite. This is because I prefer to use equational reasoning to prove the correctness of
pipes. For those new to Haskell, equational reasoning is the use of equations to prove code is correct without ever running it. Haskell makes this possible by strictly enforcing purity.
Equational reasoning works well for a library like
pipesbecause most properties of interest can easily be specified as category theory laws. If you are unfamiliar with category theory, you can read this short primer to learn how it relates to programming.
Every primitive in the
pipeslibrary is related to a category in some way:
(~>)are the identity and composition operator of a category
(>~)are the identity and composition operator of a category
(>->)are the identity and composition operator of a category
-- Left Identity yield ~> f = f -- Right Identity f ~> yield = f -- Associativity (f ~> g) ~> h = f ~> (g ~> h) -- Left Identity await >~ f = f -- Right Identity f ~> await = f -- Associativity (f >~ g) >~ h = f >~ (g >~ h) -- Left Identity cat >-> f = f -- Right Identity f >-> cat = f -- Associativity (f >-> g) >-> h = f >-> (g >-> h)Category theory laws are like tests: they are properties that we expect our code to obey if we wrote it correctly. These kinds of laws tend to have the nice property that they tend to uncannily summarize many useful properties we would like to know in a remarkably small set of equations. For example,
(~>)is defined in terms of
(f ~> g) x = for (f x) gWhen you restate the category laws for
(~>)in terms of
for, you get the "for loop laws":
-- Looping over a single yield simplifies to function -- application for (yield x) $ \e -> do f e = f x -- Re-yielding every element of a generator returns the -- original generator for gen $ \e -> do yield e = gen -- Nested for loops can become a sequential for loops if the -- inner loop body ignores the outer loop variable for gen0 $ \i -> do for (f i) $ \j -> do g j = for gen1 $ \j -> do g j where gen1 = for gen0 $ \i -> do f iThese are common sense laws that we would expect any language with generators and for loops to obey. Amazingly, the for loop laws emerge naturally from category laws, almost as if they were handed down to us on stone tablets.
For a while I've been writing these proofs out by hand informally in notebooks, but now that I'm writing up my thesis I needed to organize my notes and fill in all the little steps that I would previously skip over. You can find the full set of my notes as an organized markdown file that I've committed to the
pipesrepository that contains all my manual proofs of the pipe laws.
There are several caveats that I need to state about these proofs:
First, there is the obvious caveat that these proofs are still not machine-checked, but that's the next step. Paolo Capriotti has been patiently teaching me how to encode my reasoning into Agda. However, I believe this should be possible and that the proofs are very close to sound, taking into account the following caveats below.
Second, these proofs do not account for bottom (i.e.
_|_). My intuition is that the
pipeslaws do hold even in the presence of bottom, by I am still new to reasoning about bottom, so I omitted that for now. If anybody can point me to a good reference on this I would be grateful.
Third, these proofs use a non-standard coinductive reasoning. To explain why, it's important to note that typical coinductive reasoning in Haskell requires the result to be productive and to guard coinduction behind the production of a constructor. However, not all pipelines are productive, as the following examples illustrate:
infinite = forever $ yield () infinite >-> forever await = _|_ for infinite discard = _|_So instead of using productivity to impose a total ordering on coinductive reasoning I use "consuming" to order my coinductive proofs, meaning that all uses of coinduction are guarded behind the consumption of a constructor. In other words, my proofs do not guarantee that pipe composition makes progress in production, but they do guarantee that pipe composition makes progress in consumption.
Fourth, another departure from typical coinductive proofs is notation. Coinductive reasoning uses bisimilarity to prove "equality". I also use bisimilarity, but notationally I just write it down as a single chain of equations that is bisected by a reference to coinduction. The two halves of the equation chain, above and below the bisection, constitute the two bisimilar halves.
Fifth, proofs notationally discharge other proofs using headers as the namespace. If you see a reference like
[Kleisli Category - Left Identity Law - Pointful], that means you should look under top-level header
Kleisli Categoryfor sub-header
Left Identity Lawand sub-sub-header
Sixth, I've only proven the laws for the bidirectional API in the
Pipes.Coremodule. However, the category laws for the unidirectional API are very easy to derive from the laws for the bidirectional API, so I leave those as an exercise until I have time to add them myself.
My goal is to eventually machine-check these proofs so that
pipeswill be a practical and instructive example of a library with a statically verified kernel. Moreover, I hope that these proofs will allow other people to equationally reason about even more sophisticated systems built on top of
pipesand prove higher-level properties by discharging the proofs that I have assembled for them.