Absurdity

absurd-haskell.hs

module Absurd where

import Data.Void

-- Void is an empty type; there are values of type Void.

-- Example with incomplete pattern matching, which we should avoid on principle, and which
-- we can configure the compiler to yell about:
missingCase :: Either Void x -> x
missingCase eVR = case eVR of
    Right x = x
    -- missing Left case – *we* know Left is impossible, but we should get the compiler to prove that for us!

-- Example with complete pattern matching, but by cheating in an unsafe way via `undefined`
fakeCase :: Either Void x -> x
fakeCase eVR = case eVR of
    Right x = x
    Left _ = undefined -- compiler accepts `undefined` anywhere, because it is a member of every type. So… fixed?

-- Q: What's wrong with `undefined`?
-- A: It is TOO powerful, we can accidentally end up with partial functions:
mistake :: Either Void x -> x
mistake eVR = case eVR of
    Right x = undefined -- oops! Mistake, but the compiler doesn't catch it. `undefined` is dangerous!
    Left _ = undefined

-- Example by Harry Garrood: safe, typechecks; no wielding the dangerous footgun of `undefined`
safe :: Either Void x -> x
safe eVR = case eVR of
    Right x = x
    Left v = absurd v -- absurd :: Void -> x
    -- the left path above can never happen, which our use of `absurd` *confirms*
    -- (because compiler proves that to use `absurd`, we would need a Void value, which we cannot make)

-- Q: why would you end up with a Void value somewhere anyway?
-- A: see https://www.fpcomplete.com/blog/2017/07/to-void-or-to-void for "real-world" examples