Practical examples of using Void

Question

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.

Villainy

are you talking about a unit type with just one value (mod. undefined) or a real void type (no values beside the usual undefined)? – Uncommercial

Void has no inhabitants so how can you return something of type Void. – Emf

@Emf well many languages uses void as a special replacement for a unit-type (C,Java,...) – Uncommercial

@Carsten right, but this question was tagged as Haskell so I assume the author is talking about Haskell's Void. – Emf

I'm confused s well - anyway: I suspect this one will be closed rather quickly - I don't think it's a good fit for SO – Uncommercial

I'm talking about Haskell's Void type. Discussion is whether to replace function's noreturn attribute (for functions like fatalError) with this Void return type. In Swift, it will be called NoReturn or something like this, but in this context it does not really matter. But to do so, - and then read the question. – Villainy

@Villainy can you give an example? Because it just does not make any sense to use values of type Void - no matter if you call them NoReturn or anything else - a function a -> Void in Haskell cannot be meaningful defined – Uncommercial

@Villainy take a look at how OCaml uses the unit type (unit) and its only value (()), that would be of better use. – Emf

f# uses exactly this - it translates .net void results into Unit – Uncommercial

@Carsten If function in Haskell returns Void, then it must return undefined. Then it must crash before returning. So basically, noreturn attribute from C-family is equivlent to returning Void. – Villainy

it does not have to crash (example let f :: a -> Void; f x = f x) - as I said it's a pointless function - totally useless (how is crashing your program the same as having a void function in C???) – Uncommercial

@Villainy sorry, are you claiming that 'returning undefined' in Haskell crashes the program (not necessarily true by itself) and that you want a way to tag functions in Swift which crash the program? – Emf

well I don't think this will get any fitting answer here - I would recommend you visit the haskell IRC or reddit channels instead – Uncommercial

@Carsten I had to add a clarification to the question that by Void I always mean Haskell's Void, an empty type, and never void type from C family. – Villainy

anyway if you ask my opinion: if swift wants to be functional then you should either go the Unit route or just stick with what you have – Uncommercial

@Emf Yes, but that use case is not enough, so I want other examples of using Void. For examples, Maybe Void is equivalent to () (without undefined), but how can that be used? Either a Void is equivalent to a, but I again can't think of an example where that would really help. – Villainy

see also stackoverflow.com/questions/11968789 – Avogadro

Answer 1

(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.

Eiland

Thank you, that really helps! Can't upvote, but accepted. – Villainy

@Villainy Another way of saying that a producer doesn't stop is to leave the return type polymorphic (it can be of any type, because it is never actually returned). – Eiland

Thats simply because a polymorphic (independent) return type is isomorphic to Void. – Dracaena