Hi Streaming Haskellers,
In both pipes, and conduit, a closed output is Void and a closed input is (), where there are just dummy values supplied whenever there is an Await / NeedInput constructor.
I think it is an error to have an Await constructor in a closed input pipe. Likewise for closed output pipes, but supplying a Yield / HaveOutput constructor without a specimen of the output is not possible (ignoring bottom here).
My suggestion is demanding a proof of non-emptiness with the Await constructor:
type NonEmpty a = (a -> Void) -> Void
-- just the Await constructor here, of course part of the whole PipeF / Conduit type
Await :: NonEmpty a -> (a -> x) -> PipeF a b x
absurdlyVoid :: NonEmpty Void -> a
absurdlyVoid f = absurd (f id)
It isn't really important to be able to actually prove that a type is NonEmpty, because you can just supply a bottom, what matters is that you don't lie. :)
Cheers,
Aristid