haskelltypestype-systemscurry-howard

Practical examples of using Void


Edit: By Void, I mean Haskell's Void type, i.e. empty type that cannot have values but undefined.

There is an ongoing discussion on Swift Evolution whether to replace noreturn function attribute with an actual Void type. To do so, we must be sure that this will bring real benefit to the platform. Using Void as return type is just not enough.

So I ask you to provide very practical examples, where usage of Void adds clarity, brevity, genericity to the code. Maybe it will use classes (in Haskell sense), maybe generics, maybe it will incorporate Void in an ADT.

But please, don't go too far into HKT, Monads, all that high-level stuff. An utility function from standard library is also a bad example. A perfect example would be part of an arcade game or something like that.


Solution

  • (Speaking of Void as the type with no values, which is different to the type with just one value, usually called Unit.)

    In Haskell streaming libraries like streaming or pipes, there are data types that represent "a source of values of type a that, once exhausted, returns a value of type r". Something like Producer a m r (The m is a base monad but that's not relevant here.)

    Having producers return with a value (of a type unrelated to the type of values they emit while running) is actually quite useful. For example, you can define a "streaming splitter" as a function with type:

    streamingSplit :: Producer a m r -> Producer a m (Producer a m r)
    

    This function segments the producer without having to accumulate in memory all the elements preceding the split.

    Now, what if we want to express at the type level that a producer never stops producing stuff? We can make it return a value of type Void, like Producer a m Void.

    Another possible use-case. Suppose you have a higher-order function that takes a callback that might fail. Something like:

    -- does something with the wrapped callback, maybe emit a log message or whatever
    takesACallback :: (a -> IO (Either e r)) -> a -> IO (Either e r)
    

    What if we want to define a version of takesACallback for functions a -> IO r that never fail? Getting into and out of the Either is a hassle, and incurs in an spurious pattern-match when getting the value out.

    Using Void we can start by turning the a -> IO r into a a -> IO (Either Void r), pass it into takesACallback, and then remove the "fake" error branch on the Either using the absurd :: Void -> a function.

    takesACallback':: (a -> IO r) -> a -> IO r
    takesACallback' callback = fmap (either absurd id) 
                             . takesACallback (fmap Right . callback) 
    

    Here's an example of this trick on Hackage.