Life is a little bit hard, since Haskell is non strict. The general use case is to handle impossible paths. For example
simple :: Either Void a -> a
simple (Left x) = absurd x
simple (Right y) = y
This turns out to be somewhat useful. Consider a simple type for Pipes
data Pipe a b r
= Pure r
| Await (a -> Pipe a b r)
| Yield !b (Pipe a b r)
this is a strict-ified and simplified version of the standard pipes type from Gabriel Gonzales’ Pipes library. Now, we can encode a pipe that never yields (ie, a consumer) as
type Consumer a r = Pipe a Void r
this really never yields. The implication of this is that the proper fold rule for a Consumer is
foldConsumer :: (r -> s) -> ((a -> s) -> s) -> Consumer a r -> s
foldConsumer onPure onAwait p
= case p of
Pure x -> onPure x
Await f -> onAwait $ \x -> foldConsumer onPure onAwait (f x)
Yield x _ -> absurd x
or alternatively, that you can ignore the yield case when dealing with consumers. This is the general version of this design pattern: use polymorphic data types and Void to get rid of possibilities when you need to.
Probably the most classic use of Void is in CPS.
type Continuation a = a -> Void
that is, a Continuation is a function which never returns. Continuation is the type version of “not.” From this we get a monad of CPS (corresponding to classical logic)
newtype CPS a = Continuation (Continuation a)
since Haskell is pure, we can’t get anything out of this type.