{-# LANGUAGE RankNTypes #-} -- | module Cantor ( _Natural ) where import Control.Monad.Hyper import Data.Profunctor import Numeric.Natural type Cantor = Natural -> Bool type Functional = Cantor -> Bool -- | find :: Functional -> Cantor find p = branch x0 l0 (find (\r -> p (branch x0 l0 r))) where x0 = forsome (\l -> forsome (\r -> p (branch True l r))) l0 = find (\l -> forsome (\r -> p (branch x0 l r))) branch x _ _ 0 = x branch _ l r n | odd n = l ((n - 1) `div` 2) | otherwise = r ((n - 2) `div` 2) forevery, forsome :: Functional -> Bool forsome f = f (find f) forevery f = not (forsome (not . f)) type Iso' s a = forall p f. (Profunctor p, Functor f) => p a (f a) -> p s (f s) -- | Inductive Hyper functions from Bool to Bool are isomorphic to the natural numbers. _Natural :: Iso' Natural (Hyper Bool Bool) _Natural = dimap (ana enum) (fmap (cata denum)) where unpair :: Natural -> (Natural, Natural) unpair 0 = (0, 0) unpair n = (xr + 2*x, yr + 2*y) where (p, xr) = divMod n 2 (q, yr) = divMod p 2 (x, y) = unpair q enum :: Natural -> Functional enum 0 = const False enum 1 = const True enum n0 = fn' (n0-2) where fn' f a = compute 0 f where compute k 0 = not (a k) compute k 1 = a k compute k n | n' <- n - 2, q <- div n' 5 = case mod n' 5 of 0 -> not (a k) && compute (k+1) q 1 -> a k && compute (k+1) q 2 -> not (a k) || compute (k+1) q 3 -> a k || compute (k+1) q 4 | (x, y) <- unpair q -> if a k then compute (k+1) y else compute (k+1) x pair :: Natural -> Natural -> Natural pair 0 0 = 0 pair m n = mr + 2 * nr + 4 * pair mq nq where (mq, mr) = divMod m 2 (nq, nr) = divMod n 2 shift :: Bool -> Functional -> Functional shift b f = f . prepend b prepend b _ 0 = b prepend _ a n = a (n-1) getConst :: Functional -> Maybe Bool getConst f | forevery (\a -> f a == b) = Just b | otherwise = Nothing where b = f (const False) denum :: Functional -> Natural denum f0 = case getConst f0 of Just False -> 0 Just True -> 1 Nothing -> 2 + go f0 where go f | a <- shift False f , b <- shift True f = case getConst a of Nothing -> case getConst b of Nothing -> 6 + 5 * pair (go a) (go b) Just False -> 2 + 5 * go a Just True -> 5 + 5 * go a Just False -> case getConst b of Nothing -> 3 + 5 * go b Just False -> error "impossible" Just True -> 1 Just True -> case getConst b of Nothing -> 4 + 5 * go b Just False -> 0 Just True -> error "impossible"