{-# LANGUAGE GADTs #-}
-- | Natural numbers inductivey defined at the type-level, and of kind @*@.
module Language.Symantic.Typing.Peano where

import Data.Type.Equality

-- * Types 'Zero' and 'Succ'
data Zero
data Succ p

-- ** Type synonyms for a few numbers
type P0 = Zero
type P1 = Succ P0
type P2 = Succ P1
type P3 = Succ P2
-- ...

-- * Type 'SPeano'
-- | Singleton for 'Zero' and 'Succ'.
data SPeano p where
 SZero :: SPeano Zero
 SSucc :: SPeano p -> SPeano (Succ p)
instance TestEquality SPeano where
	testEquality SZero SZero = Just Refl
	testEquality (SSucc x) (SSucc y)
	 | Just Refl <- testEquality x y
	 = Just Refl
	testEquality _ _ = Nothing

-- * Type 'IPeano'
-- | Implicit construction of 'SPeano'.
class IPeano p where
	ipeano :: SPeano p
instance IPeano Zero where
	ipeano = SZero
instance IPeano p => IPeano (Succ p) where
	ipeano = SSucc ipeano

-- * Type 'EPeano'
data EPeano where
	EPeano :: SPeano p -> EPeano
instance Eq EPeano where
	EPeano x == EPeano y =
		case testEquality x y of
		 Just _ -> True
		 _ -> False
instance Show EPeano where
	show (EPeano x) = show (integral_from_peano x::Integer)

-- * Interface with 'Integral'
integral_from_peano :: Integral i => SPeano p -> i
integral_from_peano SZero = 0
integral_from_peano (SSucc x) = 1 + integral_from_peano x

peano_from_integral :: Integral i => i -> (forall p. SPeano p -> ret) -> ret
peano_from_integral 0 k = k SZero
peano_from_integral i k | i > 0 =
	peano_from_integral (i - 1) $ \p -> k (SSucc p)
peano_from_integral _ _ = error "peano_from_integral"

{-
-- | /Type-level natural number/, inductively defined.
data Nat
 =   Z
 |   S Nat

data SNat n where
	SNatZ :: SNat 'Z
	SNatS :: SNat n -> SNat ('S n)
instance Show (SNat n) where
	showsPrec _p = showsPrec 10 . intNat

intNat :: SNat n -> Int
intNat = go 0
	where
	go :: Int -> SNat n -> Int
	go i SNatZ     = i
	go i (SNatS n) = go (1 + i) n

type family (+) (a::Nat) (b::Nat) :: Nat where
	'Z   + b = b
	'S a + b = 'S (a + b)
-}