universe.hs

{-#LANGUAGE DeriveFunctor #-}
{-#LANGUAGE ExistentialQuantification #-}
{-#LANGUAGE FlexibleInstances #-}
{-#LANGUAGE ScopedTypeVariables #-}
module Main where

import Data.List
import Data.Maybe
import Data.Void
import Numeric.Natural
import Prelude hiding (quot, rem)

-- Cardinality
-------------------------------------------------------------------------------

data Cardinality a = Finite Natural | Infinite
  deriving (Eq, Ord, Read, Show)

lessThan :: Natural -> Cardinality a -> Bool
lessThan n (Finite m) = n < m
lessThan _         _  = True

unsafeFromFinite :: Cardinality a -> Natural
unsafeFromFinite (Finite n) = n
unsafeFromFinite _ = error "Infinite"

-- SomeCardinality
-------------------------------------------------------------------------------

data SomeCardinality = forall a. SomeCardinality (Cardinality a)

instance Eq SomeCardinality where
  SomeCardinality (Finite n) == SomeCardinality (Finite m) = n == m
  SomeCardinality Infinite   == SomeCardinality  Infinite  = True
  SomeCardinality _          == SomeCardinality  _         = False

instance Ord SomeCardinality where
  SomeCardinality (Finite n) <= SomeCardinality (Finite m) = n <= m
  SomeCardinality (Finite _) <= SomeCardinality         _  = True
  SomeCardinality         _  <= SomeCardinality         _  = False

-- Universe
-------------------------------------------------------------------------------

class Universe a where
  cardinality :: Cardinality a
  fromNatural :: Natural -> Maybe a
  toNatural :: a -> Natural

  universe :: [a]
  universe = map fromJust . takeWhile isJust $ map fromNatural [0..]

-- Universe Instances
-------------------------------------------------------------------------------

instance Universe Void where
  cardinality = Finite 0
  fromNatural _ = Nothing
  toNatural = absurd

instance Universe () where
  cardinality = unsafeCardinality
  fromNatural = unsafeFromNatural
  toNatural = unsafeToNatural

instance Universe Bool where
  cardinality = unsafeCardinality
  fromNatural = unsafeFromNatural
  toNatural = unsafeToNatural

instance Universe Natural where
  cardinality = Infinite
  fromNatural = Just
  toNatural = id

instance (Universe a, Universe b) => Universe (a, b) where
  cardinality = case (cardinality :: Cardinality a,
                      cardinality :: Cardinality b) of
    (Finite a, Finite b) -> Finite $ a * b
    _                    -> Infinite

  fromNatural n = case (cardinality :: Cardinality a,
                        cardinality :: Cardinality b) of
    (Finite 0,        _) -> Nothing
    (       _, Finite 0) -> Nothing
    (Finite a, Finite b) -> let (quot, rem) = n `quotRem` a
                            in  if n < a * b
                                  then (,) <$> fromNatural rem <*> fromNatural quot
                                  else Nothing
    (Finite a,        _) -> let (quot, rem) = n `quotRem` a
                            in  (,) <$> fromNatural rem  <*> fromNatural quot
    (       _, Finite b) -> let (quot, rem) = n `quotRem` b
                            in  (,) <$> fromNatural quot <*> fromNatural rem
    _                    ->
      let (a, b) = bitunpair n
      in  (,) <$> fromNatural a <*> fromNatural b

  toNatural (l, r) = case (cardinality :: Cardinality a,
                           cardinality :: Cardinality b) of
    (Finite a,        _) -> toNatural l + (a * toNatural r)
    (       _, Finite b) -> toNatural r + (b * toNatural l)
    _                    -> bitpair (toNatural l, toNatural r)

instance (Universe a, Universe b) => Universe (Either a b) where
  cardinality = case (cardinality :: Cardinality a,
                      cardinality :: Cardinality b) of
    (Finite a, Finite b) -> Finite $ a + b
    _                    -> Infinite

  fromNatural n = case (cardinality :: Cardinality a,
                        cardinality :: Cardinality b) of
    (Finite 0,        _) -> Nothing
    (       _, Finite 0) -> Nothing
    (       a,        b) ->
      let an = n `div` 2
          bn = (n - 1) `div` 2
      in  if SomeCardinality a <= SomeCardinality b
            then if even n
                   then if an `lessThan` a
                          then Left  <$> fromNatural an
                          else Right <$> fromNatural (n - unsafeFromFinite a)
                   else if an `lessThan` a 
                          then Right <$> fromNatural bn
                          else Right <$> fromNatural (n - unsafeFromFinite a)
            else if odd n
                   then if bn `lessThan` b
                          then Right <$> fromNatural bn
                          else Left  <$> fromNatural (n - unsafeFromFinite b)
                   else if n == 0 || bn `lessThan` b
                          then Left  <$> fromNatural an
                          else Left  <$> fromNatural (n - unsafeFromFinite b)

  toNatural (Left l) =
    let a  = toNatural l
        an = a * 2
        b  = cardinality :: Cardinality b
    in  if b == Infinite || an `lessThan` b
          then an
          else a + unsafeFromFinite b

  toNatural (Right r) =
    let b  = toNatural r
        bn = (b * 2) + 1
        a  = cardinality :: Cardinality a
    in  if a == Infinite || bn `lessThan` a
          then bn
          else b + unsafeFromFinite a

instance Universe a => Universe (Maybe a) where
  cardinality = sameCardinality (cardinality :: Cardinality (Either () a))
  fromNatural = fmap fromEither . (fromNatural :: (Natural -> Maybe (Either () a)))
  toNatural = toNatural . toEither

sameCardinality :: Cardinality a -> Cardinality b
sameCardinality (Finite n) = Finite n
sameCardinality _          = Infinite

toEither :: Maybe a -> Either () a
toEither Nothing = Left ()
toEither (Just a) = Right a

fromEither :: Either a b -> Maybe b
fromEither = either (const Nothing) (Just)

newtype ListF a b = ListF { fromListF :: Either () (a, b) }
  deriving (Functor)

instance (Universe a, Universe b) => Universe (ListF a b) where
  cardinality = sameCardinality (cardinality :: Cardinality (Either () (a, b)))
  fromNatural n = ListF <$> fromNatural n
  toNatural = toNatural . fromListF

newtype Fix f = Fix { unFix :: f (Fix f) }

cata :: Functor f => (f a -> a) -> (Fix f -> a)
cata f = f . fmap (cata f) . unFix

ana :: Functor f => (a -> f a) -> (a -> Fix f)
ana f = Fix . fmap (ana f) . f

fromList :: [a] -> Fix (ListF a)
fromList = ana $ \aas -> case aas of
  []     -> ListF $ Left ()
  (a:as) -> ListF $ Right (a, as)

toList :: Fix (ListF a) -> [a]
toList = cata $ \(ListF either) -> case either of
  Left       _  -> []
  Right (a, as) -> a:as

instance Universe a => Universe (Fix (ListF a)) where
  cardinality = Infinite
  fromNatural = fmap Fix . fromNatural
  toNatural = toNatural . unFix

instance Universe a => Universe [a] where
  cardinality = sameCardinality (cardinality :: Cardinality (Fix (ListF a)))
  fromNatural = fmap toList . fromNatural
  toNatural = toNatural . fromList

-- Bitwise Pairing and Unpairing Functions
-------------------------------------------------------------------------------

-- http://www.cse.unt.edu/~tarau/research/2009/jfpPRIMES.pdf

type Bit = Integer

nat2set :: Natural -> [Bit]
nat2set n = nat2exps n 0 where
  nat2exps 0 _ = []
  nat2exps n' x = if even n' then xs else x : xs where
    xs = nat2exps (n' `div` 2) (x + 1)

set2nat :: [Bit] -> Natural
set2nat = sum . map (2 ^)

bitpair :: (Natural, Natural) -> Natural
bitpair (i, j) = set2nat (evens i ++ odds j) where
  evens = map (2 *) . nat2set
  odds = map ((+) 1) . evens

bitunpair :: Natural -> (Natural, Natural)
bitunpair n = (f xs, f ys) where
  (xs, ys) = partition even $ nat2set n
  f = set2nat . map (`div` 2)

-- Helper Functions for Writing Instances
-------------------------------------------------------------------------------

-- | Unsafe due to potential 'Int' overflow
unsafeFromNatural :: forall a. (Bounded a, Enum a) => Natural -> Maybe a
unsafeFromNatural n | i <= fromEnum (maxBound :: a) = Just $ toEnum i
                    | otherwise                     = Nothing
  where i = fromIntegral n

-- | Unsafe due to potential 'Int' overflow
unsafeToNatural :: Enum a => a -> Natural
unsafeToNatural = fromIntegral . fromEnum

-- | Unsafe due to potential 'Int' overflow
unsafeCardinality :: forall a. (Bounded a, Enum a) => Cardinality a
unsafeCardinality = Finite . fromIntegral $ 1 + fromEnum (maxBound :: a) - fromEnum (minBound :: a)

-- Example Data Types & Instances
-------------------------------------------------------------------------------

data OneTwoOrThree = One | Two | Three
  deriving (Bounded, Enum, Eq, Ord, Read, Show)

instance Universe OneTwoOrThree where
  cardinality = unsafeCardinality
  fromNatural = unsafeFromNatural
  toNatural = unsafeToNatural

data Alpha = A | B | C | D | E | F | G | H | I | J | K | L | M
           | N | O | P | Q | R | S | T | U | V | W | X | Y | Z
  deriving (Bounded, Enum, Eq, Ord, Read, Show)

instance Universe Alpha where
  cardinality = unsafeCardinality
  fromNatural = unsafeFromNatural
  toNatural = unsafeToNatural

main :: IO ()
main = pure ()