ParityNaturals.hs

{-# LANGUAGE GADTs #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeFamilyDependencies #-}

module Nat where

-- Our own little prelude with just Bool and not
import Prelude((++), Show(..), error)

data Bool
  = True
  | False
  deriving Show

not :: Bool -> Bool
not False = True
not True = False

-- Simple successor encoding of natural numbers
-- We'll define succ, pred, even, odd, +, and * on them
data Nat
  = Z
  | S Nat
  deriving Show

succ :: Nat -> Nat
succ = S

pred :: Nat -> Nat
pred Z = Z
pred (S n) = n

even :: Nat -> Bool
even Z = True
even (S Z) = False
even (S (S n)) = even n

odd :: Nat -> Bool
odd n = not (even n)

(+) :: Nat -> Nat -> Nat
n + Z = n
n + (S m) = S n + m

(*) :: Nat -> Nat -> Nat
_ * Z = Z
n * (S m) = n + (n * m)

-- One simple idea for encoding parity
-- However, this requires function writers to get things correct
data ParityNat
  = ZZ
  | SO ParityNat
  | SE ParityNat
  deriving Show

succPar :: ParityNat -> ParityNat
succPar ZZ = SO ZZ
succPar n@(SO _) = SE n
succPar n@(SE _) = SO n

predPar :: ParityNat -> ParityNat
predPar ZZ = ZZ
predPar (SO n) = n
predPar (SE n) = n

evenPar :: ParityNat -> Bool
evenPar ZZ = True
evenPar (SO _) = False
evenPar (SE _) = True

oddPar :: ParityNat -> Bool
oddPar n = not (evenPar n)

(+.) :: ParityNat -> ParityNat -> ParityNat
n +. ZZ = n
ZZ +. m = m
n@(SO _) +. (SO m) = SE n +. m
n@(SE _) +. (SO m) = SO n +. m
n@(SO _) +. (SE m) = SE n +. m
n@(SE _) +. (SE m) = SO n +. m

(*.) :: ParityNat -> ParityNat -> ParityNat
_ *. ZZ = ZZ
n *. (SO m) = n +. (n *. m)
n *. (SE m) = n +. (n *. m)

-- Now let's try enforcement in the types
data Parity = Even | Odd
  deriving Show

-- Essentially a type-level function from Parity -> Parity
-- Acts like our `not` function on bools
type family Opp (p :: Parity) = (r :: Parity) | r -> p where
  Opp 'Even = 'Odd
  Opp 'Odd = 'Even

-- The parity of a natural is now encoded in its type
data Natural :: Parity -> * where
  Zero :: Natural 'Even
  Succ :: (p ~ Opp r, r ~ Opp p) => Natural p -> Natural r

instance Show (Natural p) where
  show Zero = "Zero"
  show (Succ n) = "(Succ " ++ show n ++ ")"

succNat :: (p ~ Opp r, r ~ Opp p) => Natural p -> Natural r
succNat = Succ

predNat :: Natural p -> Natural (Opp p)
predNat Zero = error "Can't take the pred of Zero"
predNat (Succ n) = n

evenNat :: Natural 'Even -> Bool
evenNat _ = True

oddNat :: Natural 'Odd -> Bool
oddNat _ = True

type family Add (n :: Parity) (m :: Parity) = (nm :: Parity) where
  Add 'Odd 'Odd = 'Even
  Add p 'Even = p
  Add 'Even p = p

(+>) ::
  ( p1 ~ Opp r1
  , r1 ~ Opp p1
  , p2 ~ Opp r2
  , r2 ~ Opp p2
  , Add r1 r2 ~ Add p1 p2
  ) =>
  Natural p1 -> Natural p2 -> Natural (Add p1 p2)
n +> Zero = n
n +> (Succ m) = Succ n +> m

type family Mult (n :: Parity) (m :: Parity) = (nm :: Parity) where
  Mult 'Odd  'Odd  = 'Odd
  Mult _ _ = 'Even

(*>) ::
  ( p1 ~ Opp r1
  , r1 ~ Opp p1
  , p2 ~ Opp r2
  , r2 ~ Opp p2
  , Add p1 (Mult p1 p2) ~ Mult p1 r2
  , Add p1 (Mult p1 r2) ~ Mult p1 p2
  , Add p1 (Mult p2 r2) ~ Mult p1 p2
  , Add p1 (Mult r2 p2) ~ Mult p1 r2
  , Add r1 (Opp (Mult p1 p2)) ~ Mult p1 r2
  , Add r1 (Opp (Mult p1 r2)) ~ Mult p1 p2
  , Add r1 p2 ~ Add p1 r2
  , Add r1 r2 ~ Add p1 p2
  , Opp (Opp (Mult p1 p2)) ~ Mult p1 p2
  , Opp (Opp (Mult p1 r2)) ~ Mult p1 r2
  ) =>
  Natural p1 -> Natural p2 -> Natural (Mult p1 p2)
_ *> Zero = Zero
n *> (Succ m) = n +> (n *> m)