Russell’s Paradox in Haskell (and Purescript, and Elm, ...)
Essentially from Impredicativity Bites
-- Empty datatype (contradiction)
data Empty
-- nb. In Purescript and Elm, which don't allow for
-- empty `data` declarations, this can be encoded as
-- data Empty = Empty Empty
-- which works due to strict evaluation
-- We can turn a value of type Empty into any
-- other type, since no value of type Empty
-- exists. (principle of explosion)
explode :: Empty -> a
explode x = case x of
-- A value of type 'No a' is a function
-- that can turn an 'a' into an 'Empty'. Since
-- the 'Empty' type is empty, this is only
-- possible if the 'a' type is also empty.
-- So, a value of type 'No a' contains a
-- witness that 'a' is empty. In other words,
-- the type 'No a' is empty exactly when the
-- type 'a' is nonempty. (negation)
type No a = a -> Empty
-- For any type 'a', it cannot ever be that both
-- 'a' and 'No a' are inhabited (noncontradiction)
neverEmptyAndNonempty :: No (a, No a)
neverEmptyAndNonempty (a, noA) = noA a
-- A value of type Russ contains a proof of
-- its own non-existence (Russell's paradox)
data Russ = Russ (No Russ)
-- Witness to Russ being empty
noRuss :: No Russ
noRuss russ = case russ of Russ noRuss -> noRuss russ
-- Witness to Russ being nonempty
russ :: Russ
russ = Russ noRuss
-- Discharge the contradiction
anything :: a
anything = explode (neverEmptyAndNonempty (russ, noRuss))