{- Copyright (c) 2010, Gregory M. Crosswhite. All rights reserved. -}

{-# LANGUAGE TypeFamilies #-}

module TypeLevel.NaturalNumber.Operations where

import TypeLevel.NaturalNumber

-- | The 'Plus' type family provides a function that adds two
-- type-level natural numbers.  This function is implemented by
-- induction on the first argument --- a fact that one should be aware
-- of when using it in function signatures.
type family Plus m n
-- | base case
type instance Plus Zero n = n
-- | inductive case
type instance Plus (SuccessorTo m) n = SuccessorTo (Plus m n)

-- | The 'Plus' type family provides a function that subtracts two
-- type-level natural numbers.  This function is implemented by
-- induction on both arguments, with the base case being when the
-- second argument is Zero.
type family Minus m n
-- | base case
type instance Minus m Zero = m
-- | inductive case
type instance Minus (SuccessorTo m) (SuccessorTo n) = Minus m n