Skip to content

Embed URL

HTTPS clone URL

Subversion checkout URL

You can clone with
or
.
Download ZIP
Hilbert's Epsilon
{-# 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 (/=)
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Something went wrong with that request. Please try again.