# 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

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