Hilbert's Epsilon

Epsilon.hs

{-# LANGUAGE NPlusKPatterns, RankNTypes #-}

-- ransacking infinite structures quickly without side-effects

import Data.Maybe (fromMaybe)
import Control.Applicative
import Data.Map (Map)
import qualified Data.Map as Map
import Control.Monad
import Control.Monad.Trans.Class
import Data.Functor.Identity

type Cantor = Int -> Bool

infixr 0 #
(#) :: Bool -> Cantor -> Cantor
(x # a) 0 = x
(x # a) (i + 1) = a i

berger :: (Cantor -> Bool) -> Cantor
berger p = if ex $ \a -> p $ False # a
           then False # berger $ \a -> p $ False # a
           else True  # berger $ \a -> p $ True # a
  where ex q = q (berger q)

escardo :: (Cantor -> Bool) -> Cantor
escardo p = branch x l r where
  branch x l r n = case divMod n 2 of
    (0, 0) -> x
    (q, 1) -> l q
    (q, 0) -> r (q - 1)
  x = ex $ \l -> ex $ \r -> p $ branch True l r
  l = escardo $ \l -> ex $ \r -> p $ branch x l r
  r = escardo $ \r -> p $ branch x l r
  ex q = q $ escardo q

newtype S s m a = S { runS :: s -> m (a, s) }

instance Monad m => Functor (S s m) where
  fmap = liftM

instance Monad m => Applicative (S s m) where
  pure = return
  (<*>) = ap

instance Monad m => Monad (S s m) where
  return a = S $ \s -> return (a, s)
  S m >>= k = S $ \s -> do
    (a, s') <- m s
    runS (k a) s'

instance MonadTrans (S s) where
  lift m = S $ \s -> liftM (\a -> (a, s)) m

modulusM :: (Monad m, Real a) => (forall f. (Applicative f, Monad f) => (a -> f b) -> f c) -> (a -> m b) -> m a
modulusM phi alpha = liftM snd $ runS (phi beta) 0 where
  beta n = S $ \ i -> do
    a <- alpha n
    return (a, max i n)

modulus :: Real a => (forall f. (Applicative f, Monad f) => (a -> f b) -> f c) -> (a -> b) -> a
modulus phi alpha = runIdentity $ modulusM phi (Identity . alpha)

foo :: Int
foo = modulus (\a -> a 10 >>= a) (\n -> n * n)

newtype K r s m a = K { runK :: (a -> s -> m r) -> s -> m r }

instance Monad m => Functor (K r s m) where
  fmap = liftM

instance Monad m => Applicative (K r s m) where
  pure = return
  (<*>) = ap

instance Monad m => Monad (K r s m) where
  return a = K $ \k -> k a
  K m >>= f = K $ \k -> m $ \a -> runK (f a) k

instance MonadTrans (K r s) where
  lift m = K $ \k s -> m >>= \a -> k a s

type MonadHom f g = forall x. f x -> g x

-- we can also build hashable versions, pure Int-based versions, and ones that can operate purely off Eq with different asymptotics.

neighborhoodM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m (Map a Bool)
neighborhoodM phi = liftM snd $ runK (phi lift beta) (\a s -> return (a, s)) Map.empty where
  beta n = K $ \k s -> case Map.lookup n s of
    Just b -> k b s
    Nothing -> k True (Map.insert n True s) >>= \(r,t) -> case r of
      True -> return (True, t)
      False -> k False (Map.insert n False s)

neighborhood :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Map a Bool
neighborhood phi = runIdentity $ neighborhoodM (const phi)

bauerM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m (a -> Bool)
bauerM p = do
  m <- neighborhoodM p
  return $ \n -> fromMaybe True $ Map.lookup n m

bauer :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> a -> Bool
bauer phi = runIdentity $ bauerM (const phi)

newtype W m a = W { runW :: m a }

instance Monad m => Functor (W m) where
  fmap = liftM

instance Monad m => Applicative (W m) where
  pure = return
  (<*>) = ap

instance Monad m => Monad (W m) where
  return a = W (return a)
  W m >>= f = W (m >>= runW . f)

instance MonadTrans W where
  lift = W

existsM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m Bool
existsM phi = runW $ do
   q <- W $ bauerM phi
   phi W (return . q)

exists :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Bool
exists phi = runIdentity $ do
   q <- bauerM (const phi)
   phi (return . q)

forAllM :: (Monad m, Ord a) => (forall f. (Applicative f, Monad f) => MonadHom m f -> (a -> f Bool) -> f Bool) -> m Bool
forAllM phi = liftM not $ existsM (\hom -> liftM not . phi hom)

forAll :: Ord a => (forall f. (Applicative f, Monad f) => (a -> f Bool) -> f Bool) -> Bool
forAll phi = runIdentity $ forAllM (const phi)

(===) :: (Applicative f, Eq a) => f a -> f a -> f Bool
(===) = liftA2 (==)

(/==) :: (Applicative f, Eq a) => f a -> f a -> f Bool
(/==) = liftA2 (/=)