{- |
Module      :  Data.Numeric.Witness.Peano
Description :  Peano-style natural numbers paired with type-level naturals.
Copyright   :  Copyright (c) 2014 Kenneth Foner

Maintainer  :  kenneth.foner@gmail.com
Stability   :  experimental
Portability :  non-portable

This module defines GADT type witnesses for Peano-style natural numbers.
-}

{-# LANGUAGE ConstraintKinds     #-}
{-# LANGUAGE DataKinds           #-}
{-# LANGUAGE FlexibleContexts    #-}
{-# LANGUAGE FlexibleInstances   #-}
{-# LANGUAGE GADTs               #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE StandaloneDeriving  #-}
{-# LANGUAGE TypeFamilies        #-}
{-# LANGUAGE TypeOperators       #-}

module Data.Numeric.Witness.Peano where

data Zero
data Succ n

-- | Natural numbers paired with type-level natural numbers. These terms act as witnesses of a particular natural.
data Natural n where
   Zero :: Natural Zero
   Succ :: Natural n -> Natural (Succ n)
deriving instance Show (Natural n)

-- | Given a context expecting a particular natural, we can manufacture it from the aether.
class ReifyNatural n                               where reifyNatural :: Natural n
instance ReifyNatural Zero                         where reifyNatural = Zero
instance (ReifyNatural n) => ReifyNatural (Succ n) where reifyNatural = Succ (reifyNatural :: Natural n)

-- | Type level less-than-or-equal test.
type family LessThanOrEqual a b where
   LessThanOrEqual Zero     Zero     = True
   LessThanOrEqual Zero     (Succ m) = True
   LessThanOrEqual (Succ n) (Succ m) = LessThanOrEqual n m
   LessThanOrEqual x y               = False

-- | This constraint is a more succinct way of requiring that @a@ be less than or equal to @b@.
type a <= b = (LessThanOrEqual a b ~ True)

-- | Type level less-than test.
type family LessThan a b where
   LessThan Zero     (Succ m) = True
   LessThan (Succ n) (Succ m) = LessThan n m
   LessThan x        y        = False

-- | This constraint is a more succinct way of requiring that @a@ be less than @b@.
type a < b = (LessThan a b ~ True)

-- | Type level addition.
type family x + y where
   x + Zero     = x
   x + (Succ y) = Succ (x + y)

-- | Type level subtraction.
type family x - y where
   x        - Zero     = x
   (Succ x) - (Succ y) = x - y

-- | Addition of naturals at the term and type levels simultaneously.
plus :: Natural a -> Natural b -> Natural (a + b)
plus x Zero     = x
plus x (Succ y) = Succ (plus x y)

-- | Subtraction of naturals at the term and type level simultaneously. Note that it is statically prohibited to subtract
--   a number larger than the number from which it is being subtracted.
minus :: (b <= a) => Natural a -> Natural b -> Natural (a - b)
minus x        Zero     = x
minus (Succ x) (Succ y) = minus x y
minus _ _ = error "minus: the impossible occurred" -- GHC can't prove this is unreachable