{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE DataKinds #-}
{-# LANGUAGE ExplicitForAll #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}

module Arithmetic.Plus
  ( zeroL
  , zeroR
  , commutative
  , associative
  ) where

import Arithmetic.Unsafe (type (:=:) (Eq))
import GHC.TypeNats (type (+))

-- | Any number plus zero is equal to the original number.
zeroR :: m :=: (m + 0)
zeroR :: forall (m :: Nat). m :=: (m + 0)
zeroR = m :=: m
m :=: (m + 0)
forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Zero plus any number is equal to the original number.
zeroL :: m :=: (0 + m)
zeroL :: forall (m :: Nat). m :=: (0 + m)
zeroL = m :=: m
m :=: (0 + m)
forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Addition is commutative.
commutative :: forall a b. a + b :=: b + a
commutative :: forall (a :: Nat) (b :: Nat). (a + b) :=: (b + a)
commutative = (a + b) :=: (b + a)
forall (a :: Nat) (b :: Nat). a :=: b
Eq

-- | Addition is associative.
associative :: forall a b c. (a + b) + c :=: a + (b + c)
associative :: forall (a :: Nat) (b :: Nat) (c :: Nat).
((a + b) + c) :=: (a + (b + c))
associative = ((a + b) + c) :=: (a + (b + c))
forall (a :: Nat) (b :: Nat). a :=: b
Eq