I often find that violations of type-class laws almost invariably lead to subtle bugs, which is why I go to so much effort to ground my

`pipes`library in theoretically-derived type-classes and enforce their corresponding laws very strictly. In this post I'm going to illustrate the importance of this for

`conduit`by showing several conduit bugs and demonstrating how they stem directly from type-class law violations. I based these bugs on

`conduit-0.4.2`.

#### Conduits violate the Monad laws

... specifically, associativity:

printer = NeedInput (\a -> lift (print a) >> printer) (return ()) residue x = Done (Just x) ()

>>> yield 1 $$ printer 1 >>> yield 1 $$ (residue 2 >> residue 3) >> printer 2 1 >>> yield 1 $$ residue 2 >> (residue 3 >> printer) 3 2 1The left-associative grouping accidentally drops residual input. There are two cases where conduits suffer from data loss, and one of them corresponds to violating the associativity law for monads.

The next example is a bigger problem:

mySink = NeedInput (\_ -> return ()) (lift $ putStrLn "Finalize Resource)

>>> yield 1 $$ (yield 1 >> (residue 3 >> mySink)) =$ return () -- No output >>> yield 1 $$ ((yield >> residue 3) >> mySink) =$ return () Finalize ResourceThe right-associative grouping accidentally drops the finalizer. Conduits don't guarantee deterministic finalization in certain corner cases, again because they violate the monad laws.

More generally, any conduit that sequences two buffered conduits is prone to the above two bugs. The source of both violations is the attempt to "push back" input by attaching residual input to the

`Done`constructor. I can't yet offer a solution for this because I have not yet tackled the parsing problem, however removing this feature will at least prevent the above case of dropped finalizers.

#### Conduits violate the Category laws

I know that conduits do not advertise being a

`Category`, but I investigated where conduits deviated from a

`Category`and found more bugs in the process.

For example, conduits lack an identity conduit. This is apparent from the type of conduit composition:

(=$=) :: Monad m => Pipe a b m () <-- This needs to be fixed -> Pipe b c m r -> Pipe a c m rThe upstream conduit is constrained to return

`()`, so you immediately lose the ability to return values from upstream like you can with pipes and you cannot form a proper upstream identity pipe. However, we could type-restrict composition to only return

`()`and see if that forms a category, even if not necessarily as powerful as the pipes category:

(=$=) :: Monad m => Pipe a b m () -> Pipe b c m () -> Pipe a c m ()The closest this composition comes to an identity conduit is:

idC = await >>= maybe (return ()) (\a -> yield a >> idC)Unfortunately,

`idC`does not serve as an identity conduit when you place it upstream of a conduit:

inject x p = case p of NeedInput _ p' -> yield x =$= p'; p' -> p' print2 = replicateM_ 2 (await >>= lift . print)

>>> yield 1 $$ inject 2 print2 Nothing Just 2 >>> yield 1 $$ inject 2 (idC $= print2) Nothing NothingThis seemingly innocuous identity law violation actually represents a known subtle bug in conduits where if they are fed a

`Nothing`followed by a

`Just x`they break. Some conduit library code depends on this scenario never happening in order to guarantee safety and correctness. Michael already knows this, because he notes this in the comments of composition:

-- [...] However, it is not -- recommended to give input to a pipe after it has -- been told there is no more input. [...]I find it interesting that despite not attempting to make conduits a category, the invariant Michael requires is precisely the invariant necessary to make the identity law work. This exemplifies how even when we don't program using theoretical constructs, our intuition for correct behavior exactly matches the laws for the theoretically-grounded classes.

The lack of a proper upstream identity is also a source of data loss. When you compose two pipes, the residual input for the downstream pipe is discarded under all circumstances, and there is no way to solve this without introducing a proper upstream identity conduit.

`pipes`has solved this issue, but the solution is precisely what necessitated the parametrized monad and I can discuss this with Michael if he is interested because I think he would not be as reluctant to use extensions to allow

`do`notation for parametrized monads. The other advantage of switching to the

`pipes`solution is that you gain the ability to finalize upstream early without terminating, which

`conduit`does not presently have.

#### Conduits violate Monad Transformer laws

This is my fault. The first release of my library violated the monad transformer laws and while I've fixed it in version 2.0,

`conduit`still has the original version found in pipes.

The original version violates both the identity and composition laws of monad transformers. You can see this if you just count the number of

`PipeM`constructors generated:

count' n c = case c of Done i _ -> Done i n PipeM m h -> PipeM (liftM (count (n + 1)) m) h HaveOutput c' h o -> HaveOutput (count n c') h o NeedInput f c' -> NeedInput (fmap (count n) f) (count n c') count = count' 0

-- lift (return x) /= return x >>> runPipe $ count $ lift $ return (-99) 1 >>> runPipe $ count $ return (-99) 0 -- lift (m1 >> m2) /= lift m1 >> lift m2 >>> runPipe $ count $ lift $ return (-99) >> return (-99) 1 >>> runPipe $ count $ lift (return (-99)) >> lift (return (-99)) 2This is the reason I switched to using an approach based on a free monad transformer (i.e. FreeT), instead of using an ordinary free monad.

This makes the monad bind mandatory at each step, which actually leads to very little degradation of performance, so I had no problem making the switch. More importantly, though, it allows more powerful optimizations using rewrite rules than are currently possible when the monad is optional. For example, the following rewrite rule is safe once you have a correct instance for

`MonadTrans`:

{-# RULES "forever alone" forall m. forever (lift m) = lift (forever m) #-}I will discuss rewrite rules later in a post about optimizing pipes and frames, but one of my big motivations for strictly enforcing all the class laws as strong as possible is that it then permits rewrites so powerful that all the pipe code completely disappears, leaving behind the hand-written loop code (think: stream fusion on steroids).

#### Other bugs

There are other bugs in conduits that I found in the process, mainly associated with registering finalizers.

`ResourceT`machinery which ignores duplicate resource release requests

However, this is quite easy for conduits to fix. All you do is remove the finalizer field from the

`PipeM`constructor and have

`pipeClose`ignore

`PipeM`actions completely, only associating finalizers with

`HaveOutput`. This fixes the issue of multiple finalizations and also fixes the issue of accidentally drawing one last chunk of data before finalizing if you aren't careful about writing the source.

Even if you fix that, though, there are still other finalization problems. For example, while Michael provides a mechanism for bidirectionally-safe finalization, he never uses it for sources and sinks, meaning that if you elevate them to conduits they won't finalize correctly, however this is easy to fix and he will know how to do it. He also never exposes any utility functions for bidirectionally-safe finalization that is an equivalent to the

`finallyP`in

`pipes`.

#### Discussion

This post presents some examples where if you are close to a theoretically-grounded type-class but not quite there, the difference is most likely a bug. This means that you can identify bugs in a library rapidly just by examining where it approximates theoretical type-classes and then studying where they fail to observe the corresponding class laws.

## No comments:

## Post a Comment