Nat

Nat.hs

{-# LANGUAGE InstanceSigs #-}

module Nat where

data Nat
  = Zero
  | Succ Nat
  deriving (Eq, Ord, Show)

class AdditiveSemigroup a where
  infixl 6 .+.
  (.+.) :: a -> a -> a

instance AdditiveSemigroup Nat where
  (.+.) :: Nat -> Nat -> Nat
  Zero .+. n = n
  (Succ m) .+. n = m .+. (Succ n)

class AdditiveMonoid a where
  zero :: a

instance AdditiveMonoid Nat where
  zero :: Nat
  zero = Zero

class MultiplicativeSemigroup a where
  infixl 7 .*.
  (.*.) :: a -> a -> a

instance MultiplicativeSemigroup Nat where
  (.*.) :: Nat -> Nat -> Nat
  Zero .*. _ = Zero
  _ .*. Zero = Zero
  (Succ Zero) .*. n = n
  (Succ m) .*. n = m .*. n .+. n

class MultiplicativeMonoid a where
  one :: a

instance MultiplicativeMonoid Nat where
  one :: Nat
  one = Succ Zero

class (MultiplicativeMonoid a, AdditiveMonoid a) => Semiring a

instance Semiring Nat

----

n0, n1, n2, n3, n4, n5, n6, n7, n8, n9 :: Nat
n0 = Zero
n1 = Succ n0
n2 = Succ n1
n3 = Succ n2
n4 = Succ n3
n5 = Succ n4
n6 = Succ n5
n7 = Succ n6
n8 = Succ n7
n9 = Succ n8

tests :: [Bool]
tests = [
  -- Eq
    n0 == n0
  , n1 == n1
  , n0 /= n1
  -- Ord
  , n0 < n1
  , n1 > n0
  , n3 <= n3
  , n3 <= n4
  , n4 >= n3
  , n4 >= n4
  -- Num + (left/right) identity, commutativity, associativity
  , n0 .+. n7 == n7
  , n7 .+. n0 == n7
  , n2 .+. n3 == n3 .+. n2
  , (n2 .+. n3) .+. n4 == n2 .+. (n3 .+. n4)
  -- Num * (left/right) identity, commutativity, associativity
  , n1 .*. n5 == n5
  , n5 .*. n1 == n5
  , n2 .*. n3 == n3 .*. n2
  , (n2 .*. n3) .*. n4 == n2 .*. (n3 .*. n4)
  -- distributivity
  , n4 .*. (n3 .+. n6) == n4 .*. n3 .+. n4 .*. n6
  ]

runTests :: [Bool] -> Bool
runTests = all (True &&)