Seemingly impossible functional programs (Cantor spaces).

Impossible.hs

{-# LANGUAGE FlexibleInstances #-}

module Impossible where

-- http://math.andrej.com/2007/09/28/seemingly-impossible-functional-programs
-- http://math.andrej.com/2008/11/21/a-haskell-monad-for-infinite-search-in-finite-time
-- https://www.tcs.ifi.lmu.de/mitarbeiter/martin-hofmann/publikationen-pdfs/c69-onmonadicparametricityof2orderfunction.pdf
-- https://arxiv.org/abs/1203.1539v1
-- http://math.andrej.com/2011/12/06/how-to-make-the-impossible-functionals-run-even-faster
-- https://www.reddit.com/r/types/comments/fxk4d4/finitism_in_type_theory

data Natural = Zero | Succ Natural deriving Eq

instance Enum Natural where
  toEnum n
    | n <= 0    = Zero
    | otherwise = Succ (toEnum (pred n))

  fromEnum Zero     = 0
  fromEnum (Succ n) = succ (fromEnum n)

instance Num Natural where
  n + m = toEnum $ fromEnum n + fromEnum m
  n - m = toEnum $ fromEnum n + fromEnum m
  n * m = toEnum $ fromEnum n + fromEnum m
  abs n = n
  signum n = if n == 0 then 0 else 1
  fromInteger = toEnum . fromInteger

instance Show Natural where
  showsPrec d n =
    showParen (d > 0) $ \s ->
      showsPrec 0 (fromEnum n) " :: Natural" ++ s

type Cantor = Natural -> Bool

(#) :: Bool -> Cantor -> Cantor
b # c = \n -> if n == 0 then b else c (pred n)

forsome, forevery :: (Cantor -> Bool) -> Bool
forsome  p = p (find p)
forevery p = not (forsome (not . p))

find :: (Cantor -> Bool) -> Cantor
find p =
  if forsome (\a -> p (True # a))
    then True  # find (\a -> p (True  # a))
    else False # find (\a -> p (False # a))

search :: (Cantor -> Bool) -> Maybe Cantor
search p = if forsome p then Just (find p) else Nothing

instance Eq a => Eq (Cantor -> a) where
  f == g = forevery (\a -> f a == g a)

coerce :: Bool -> Natural
coerce True  = 1
coerce False = 0

f, g, h :: Cantor -> Natural
f p = coerce (p (7 * coerce (p 4) + 4 * coerce (p 4) + 4))
g p = coerce (p (coerce (p 4) + 11 * coerce (p 7)))
h p =
  if p 7
    then if p 4 then coerce (p 4) else coerce (p 11)
    else if p 4 then coerce (p 8) else coerce (p 15)