Pipe input Void, a suggestion

[Aristid Breitkreuz]

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

[Paolo Capriotti]

I considered something like this (although without the double
negation), but the problem is that with the modified `Await`
constructor, many perfectly valid pipes require a proof term, even
though the pipe would make sense regardless. In particular, you lose
the identity pipe. In other words, Pipe won't be a category over
Haskell types anymore, but over inhabited ones (or, in your version,
not-uninhabited).

Paolo

[Aristid Breitkreuz]

That's a very good point. Basically my goal is to have Pipeline be Pipe Void Void m a, and runPipe run on that. (All this applies equally to conduits, I'm just using the vocabulary from Gabriel's pipes library because it's far simpler than conduits. Ultimately what I'm using is conduits however.)

The problem with runPipe :: Pipe Void Void m a -> m a is that it's suddenly partial, and that bothers me. However it kind of makes sense, because waiting for a Void to materialise is something you end up waiting forever on, right? So bottom makes sense there.

Just having the input type be trivially satisfiable feels a bit like a deal with the devil to me, but maybe it's just the pragmatic choice. Ultimately both solutions are a bit evil (one is partial, the other introduces artificial input on request), are there other reasons for preferring one or the other that I'm missing?

Aristid

2012/8/14 Paolo Capriotti <p.cap...@gmail.com>

--
You received this message because you are subscribed to the Google Groups "streaming-haskell" group.
To post to this group, send email to streamin...@googlegroups.com.
To unsubscribe from this group, send email to streaming-hask...@googlegroups.com.

For more options, visit https://groups.google.com/groups/opt_out.

[Dan Burton]

Rather than using Void on the input end, what about leveraging GADTs, sort of like Frame did?

    data Open a
    data Closed

    data Pipe i o u m r where
      Yield :: o -> Pipe i (Open o) u m r -> Pipe i (Open o) u m r

    type Pipeline m r = Pipe Closed Void () m r

That way if you write runPipe :: Pipeline m r -> m r, the GADT magic will relieve you of the need to handle the Yield case, since it is impossible to construct a Closed-input pipe out of a Yield.

I know that in older versions of Conduit, the Pipe type was split up into several types, which allowed them to make stronger guarantees about closed ends.

-- Dan Burton

[Dan Burton]

    data Open a
    data Closed

    data Pipe i o u m r where
      Yield :: o -> Pipe i (Open o) u m r -> Pipe i (Open o) u m r

    type Pipeline m r = Pipe Closed Void () m r

Whoops, s/Yield/Await

data Pipe i o m r where
   Await :: (i -> Pipe (Open i) o m r) ->
            Pipe (Open i) o m r

I'm not quite sure how this would interact with upstream results, though.

[Aristid Breitkreuz]

How much harder would it be to write idP this way?

Michael has indicated that he tried using GADTs but found the added complexity not worth it. Perhaps it's worth investigating different GADT approaches though.

2012/8/14 Dan Burton <danburt...@gmail.com>

--