8

In the Pipes Tutorial, it says that:

The concrete type synonyms use () to close unused inputs and X (the uninhabited type) to close unused outputs:

I'd like to understand why () and X are used the way they are. Why not X or () for both inputs and outputs?

duplode
  • 33,731
  • 7
  • 79
  • 150
  • You might want to look at this question as well as the excellent answers: ["What's the `absurd` function in `Data.Void` useful for?"](http://stackoverflow.com/questions/14131856/whats-the-absurd-function-in-data-void-useful-for) – Luis Casillas Feb 02 '16 at 20:03

2 Answers2

6

X in pipes is normally spelled Void in the rest of the Haskell ecosystem, so let's pretend X = Void. It's defined like this:

data Void

And it has an "eliminator"

absurd :: Void -> a
absurd x = case x of {}

If you have something of type Void (and force it), then something has gone wrong. Your program has produced an error, or it's stuck in an infinite loop.

Making a pipe produce things of type Void bars it from ever producing anything (legitimate). Making it produce things of type () allows it to produce things, but things that carry no information. They're basically clock ticks.

On the input side, a pipe that consumes things of type Void can await input, but as soon as it does so it is stuck--no one will be able to feed it anything. A pipe that consumes things of type () can await, but only gets clock ticks.

All of these options are reasonable. I suspect Gonzalez wanted the type system to prohibit users from accidentally hooking up a pure producer to a pure consumer the wrong way around, and getting an error that could be hard to track down. By making a pure producer consume (), and a pure consumer produce Void, he makes it impossible to hook them up the wrong way.

dfeuer
  • 48,079
  • 5
  • 63
  • 167
  • `Pipes.X` is more like the `Void` of the `void` package, `newtype X = X X`, with `closed (X x) = closed x` for `absurd`, but the point is basically the same. – Michael Feb 02 '16 at 19:20
  • @Michael, that's probably because it's an evolutionary remnant that might be too hard to get rid of now. The `Void` package actually only compiles that code for old versions of `base`--otherwise most of the package is gutted by Cabal in favor of the `base` versions. – dfeuer Feb 02 '16 at 19:25
  • So, it would've been just as valid if the library used `data X = X` and `data Y = Y` for input and output since X /= Y and it is also not possible to hook them up ? –  Feb 02 '16 at 20:28
  • @Ana, I believe all sorts of such things would be valid. Of course, Gonzalez may have some deeper reasoning behind this--he knows a while lot more about category theory and pipes than I do! – dfeuer Feb 02 '16 at 20:33
3

It's actually a more general thing than just for pipes. () and X are the initial and terminal objects of the Hask category (and of categories derived from Hask), meaning that for all Haskell types a,

  • there exists exactly one morphism a -> () (namely const ())
  • there exists exactly one morphism X -> a (namely absurd).

As a consequence, any chain of functions a -> ()>>>() -> b can't actually depend on the left part (since a -> () carries no information), and any chain a -> X>>>X -> b can't depend on the right part. In that sense, a () -> b input is closed, and so is an a -> X output.

leftaroundabout
  • 117,950
  • 5
  • 174
  • 319
  • 2
    But pipes aren't functions. A pipe can consume without producing, produce without consuming, or even sit around effecting without doing either. I don't think the category of pipes over a non-identity monad is likely to have initial or final objects at all. – dfeuer Feb 02 '16 at 20:03
  • For any two types `a` and `b`, there will be "more" pipes that consume `a` and produce `b` than functions `a -> b`. – dfeuer Feb 02 '16 at 20:06