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**