Halloween

there are functions out there more scary than unsafePerformIO and this is the tale of one of them: absurd.
This powerful spell allows evil warlocks to conjure anything they want from the Void:

data Void

absurd :: forall a . Void -> a

but what does that mean? Is this even possible without using the powers of the abyss (bottom) and why the heck would a chaotic-good programmer even want to use this?

Logic

As you might have heard there exists an interesting connection between programming and logic.
Basically types are a claim (a proposition) and if you can give a value of said type you have proven the claim.
If you have a type-checker worth it’s name it will check your proofs for you (BTW: I’ll ignore undefined and things like f a = f a as those are clearly a devil’s pact we should never sign – evil or not).

Now as logic goes there are implications and those are just function-types in this translation. And as you might know False implies everything in logic.

The Void type (a type without any inhabitant) is a natural fit for a False value as you should never be able to prove False and proving means giving a value .. nice huh?

Now you might hopefully see that the absurd function is just another way of stating that you can proof everything from False – as there should be no way to construct a Void value you will never be able
to call this function anyway.

How can we implement it

In Haskell if you allow the use of the EmptyCase extension it’s quite easy

{-# LANGUAGE EmptyCase #-}

-- ...

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

if not it’s a bit more involved and basically just a Haskell version of the following.

Languages like Elm or F# don’t allow things like empty data definitions so you have to get a bit creative.
Basically the trick is to make it impossible to create a value without hitting a infinite loop:

type Void = Void Void

As you can see there is no way to define a value of type Void without using another value of it – so you can only use bottom and we don’t want to do that.

You can probably guess the definition of absurd by now:

absurd : Void -> a
absurd (Void v) = absurd v

So why is this useful

It actually is a really nice way to give some indication or hint of what your code cannot do.
For example this type in Elm

staticView : Model -> Html Void

clearly states that this piece of HTML representation will not raise any events. It’s already in Core – you just have to use Never instead of Void
as Elm is more concerned about readability than about logic (strange people those programmers).

staticView : Model -> Html Never

Now the trouble starts when you want to use this nice function inside your actual view:

view : Model -> Html Msg
view model =
    ...
    staticView model

here the type-checker will complain about you using Html Never where Html Msg was expected.

This is one scenario where the Html.map : (a -> msg) -> Html a -> Html msg
should be used … if only you had a function that could conjure a Msg out of Void

view : Model -> Html Msg
view model =
    ...
    staticView model |> Html.map never

(yeah absurd is called never …)

and again math saved the day