Logo Questions Linux Laravel Mysql Ubuntu Git Menu
 

Why does Haskell Pipes "use () to close unused inputs and X (the uninhabited type) to close unused outputs"?

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?

like image 845
Ana Avatar asked Feb 02 '16 18:02

Ana


2 Answers

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.

like image 124
dfeuer Avatar answered Nov 09 '22 09:11

dfeuer


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.

like image 3
leftaroundabout Avatar answered Nov 09 '22 08:11

leftaroundabout