nat.hs

{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE ViewPatterns #-}
{-# LANGUAGE TypeOperators #-}

import Prelude (Show(..), Enum(..), Num(..), flip, (++), Functor(..), Applicative(..), Monad(..), Foldable(..), Traversable(..), (<$>))
import qualified Prelude as P
import Data.Function
import Control.Applicative ((<**>))
import Control.Monad (join)

newtype Nat = N { r :: forall a. (a -> a) -> a -> a }
newtype Bool = B { if' :: forall a. a -> a -> a }

pattern True <- (\b -> if' b P.True P.False -> P.True) where
  True = B $ \t _ -> t

pattern False <- (\b -> if' b P.True P.False -> P.True) where
  False = B $ \_ f -> f

instance Show Nat where
  show n = show (r n succ 0)
  
instance Show Bool where
  show b = if' b "True" "False"

instance Enum Nat where
  succ n = N (\f x -> f (r n f x))
  pred n = N (\f x -> r n (\g h -> h (g f)) (const x) id)
  toEnum 0 = N (\f x -> x)
  toEnum n = succ (toEnum (n-1))
  fromEnum n = r n succ 0

instance Num Nat where
  n + m = N (\f x -> r n f (r m f x))
  abs = id
  n * m = r n ((+) m) 0
  signum n = r n (const 1) 0
  fromInteger 0 = N (\f x -> x)
  fromInteger n = succ (fromInteger (n-1))
  n - m = r m pred n

inf :: Nat
inf = N (const.fix)

isZero :: Nat -> Bool
isZero n = r n (const False) True

not :: Bool -> Bool
not b = if' b False True

nonZero :: Nat -> Bool
nonZero = not . isZero

(&&) :: Bool -> Bool -> Bool
(&&) x y = B $ \t f -> if' x (if' y t f) f

(||) :: Bool -> Bool -> Bool
(||) x y = B $ \t f -> if' x t (if' y t f)

class Eq a where
  (==) :: a -> a -> Bool
  (/=) :: a -> a -> Bool
  x /= y = not (x == y)

newtype Ordering = O { c :: forall a. a -> a -> a -> a }

instance Show Ordering where
  show o = c o "LT" "EQ" "GT"

pattern LT <- (\o -> c o P.True P.False P.False -> P.True) where
  LT = O $ \x _ _ -> x
pattern EQ <- (\o -> c o P.False P.True P.False -> P.True) where
  EQ = O $ \_ x _ -> x
pattern GT <- (\o -> c o P.False P.False P.True -> P.True) where
  GT = O $ \_ _ x -> x

instance Eq Ordering where
  (==) x = c x isLt isEq isGt where
    isLt y = c y True False False
    isEq y = c y False True False
    isGt y = c y False False True

instance Eq Nat where
  (==) n = r n (\f m -> nonZero m && f (pred m)) isZero

class Eq a => Ord a where
  compare :: a -> a -> Ordering
  compare x y = if' lte (if' gte EQ LT) GT where
    lte = x <= y
    gte = x >= y
  
  (<=) :: a -> a -> Bool
  (>=) :: a -> a -> Bool
  x <= y = compare y x /= GT
  x >= y = compare x y /= LT
  
  (<)  :: a -> a -> Bool
  (>)  :: a -> a -> Bool
  (<) x y = not (x >= y)
  (>) x y = not (x <= y)

instance Ord Nat where
  (<=) = flip (>=)
  (>=) n = r n (\f m -> isZero m || f (pred m)) isZero

newtype a :*: b = P { p :: forall c. (a -> b -> c) -> c }

data SPair a b = SPair a b

pattern x :*: y <- (flip p SPair -> (SPair x y)) where
  x :*: y = P $ \f -> f x y

instance (Show a, Show b) => Show (a :*: b) where
  show x = p x (\y z -> "(" ++ show y ++ "," ++ show z ++ ")")
  
newtype List a = L { l :: forall b. (a -> b -> b) -> b -> b }

pattern Nil <- (\xs -> l xs (\_ _ -> P.False) P.True -> P.True) where
  Nil = L $ \_ b -> b

infixr 4 :>
pattern y :> ys <- (\xs -> l xs (\e _ -> P.Just (SPair e (tail xs))) P.Nothing -> P.Just (SPair y ys)) where
  y :> ys = L $ \f b -> f y (l ys f b)

instance Show a => Show (List a) where
  show xs = "[" ++ l xs f "]" where
    f e a = show e ++ "," ++ a
  
instance Functor List where
  fmap f xs = l xs (\e a -> f e :> a) Nil

instance Functor ((:*:) a) where
  fmap f x = p x (\y z -> y :*: f z)
  
fst :: a :*: b -> a
fst x = p x (\y _ -> y)

snd :: a :*: b -> b
snd x = p x (\_ y -> y)

(...) :: Nat -> Nat -> List Nat
(...) x y = if' (x >= y) (x :> Nil) (x :> (succ x ... y) )

newtype Maybe a = M { m :: forall b. b -> (a -> b) -> b }

pattern Nothing <- (\x -> m x P.True (const P.False) -> P.True) where
  Nothing = M $ \b _ -> b

pattern Just x <- (\y -> m y P.Nothing P.Just -> P.Just x) where
  Just x = M $ \_ f -> f x

instance Show a => Show (Maybe a) where
  show x = m x "Nothing" (\y -> "Just " ++ show y)

instance Functor Maybe where
  fmap f x = M $ \d c -> m x d (c.f)

instance Applicative Maybe where
  pure = Just
  f <*> x = m f Nothing (\g -> fmap g x)
  
instance Monad Maybe where
  x >>= f = m x Nothing f

head :: List a -> Maybe a
head xs = l xs (\e _ -> Just e) Nothing

newtype a :+: b = E { e :: forall c. (a -> c) -> (b -> c) -> c }

pattern Left x <- (\y -> e y P.Just (const P.Nothing) -> P.Just x) where
  Left x = E $ \l _ -> l x

pattern Right x <- (\y -> e y (const P.Nothing) P.Just -> P.Just x) where
  Right x = E $ \_ r -> r x

instance Functor ((:+:) a) where
  fmap f x = E $ \l r -> e x l (r . f)

instance (Show a, Show b) => Show (a :+: b) where
  show x = e x (\y -> "Left " ++ show y) (\y -> "Right " ++ show y)

concat :: List a -> List a -> List a
concat xs ys = L $ \f b -> l xs f (l ys f b)

flatten :: List (List a) -> List a
flatten xs = l xs concat Nil

instance Applicative List where
  pure x = x :> Nil
  xs <*> ys = flatten $ fmap (\f -> fmap f ys) xs

instance Monad List where
  xs >>= f = flatten $ fmap f xs

tail :: List a -> List a
tail xs = L $ \c n -> l xs (\h t g -> g h (t c)) (const n) (const id)

instance Applicative ((:+:) a) where
  pure = Right
  f <*> x = e f Left (\g -> e x Left (Right . g))
  
instance Monad ((:+:) a) where
  x >>= f = e x Left f

newtype Identity a = I { y :: forall b. (a -> b) -> b }

instance Functor Identity where
  fmap f x = I $ \c -> y x (c.f)
  
instance Applicative Identity where
  pure x = I ($x)
  f <*> x = I $ \c -> c (y x (y f id))

instance Monad Identity where
  x >>= f = I (y (y x f))

newtype StateT s m a = S { rs :: forall b. s -> m ((s -> a -> b) -> b) }

(<$$>) :: Functor f => f (a -> b) -> a -> f b
(<$$>) f x = fmap ($x) f

instance Functor m => Functor (StateT s m) where
  fmap f x = S (\s -> rs x s <$$> (\s x c -> c s (f x)))

instance Monad m => Applicative (StateT s m) where
  pure x = S $ \s -> pure $ \c -> c s x
  f <*> x = S (\s -> join (rs f s <$$> (\s f -> rs x s <$$> (\s x c -> c s (f x)))))

instance Monad m => Monad (StateT s m) where
  x >>= f = S (\s -> join (rs x s <$$> (\s x -> rs (f x) s)))
  
type State s a = StateT s Identity a

runState :: s -> State s a -> s :*: a
runState s st = y (rs st s) (\c -> c (:*:))

evalState :: s -> State s a -> a
evalState s st = y (rs st s) (\c -> c (\_ x -> x))

execState :: s -> State s a -> s
execState s st = y (rs st s) (\c -> c (\x _ -> x))

get :: Applicative m => StateT s m s
get = S $ \s -> pure (\c -> c s s)

put :: Applicative m => s -> StateT s m ()
put s = S $ \_ -> pure (\c -> c s ())

modify :: Applicative m => (s -> s) -> StateT s m ()
modify f = S $ \s -> pure (\c -> c (f s) ())

instance Foldable List where
  foldr f b xs = l xs f b

instance Traversable List where
  traverse f xs = l xs g (pure Nil) where
    g e a = (:>) <$> f e <*> a