{-# LANGUAGE TypeOperators, GADTs, KindSignatures, RankNTypes #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE FlexibleInstances, MultiParamTypeClasses, ConstraintKinds, CPP #-}
{-# OPTIONS_GHC -Wall #-}
module TypeUnary.Nat
(
module TypeUnary.TyNat
, Nat(..), predN, zero, one, two, three, four
, withIsNat, natSucc, natIsNat
, natToZ, natEq, natAdd, natMul
, IsNat(..)
, induction
, PlusZero, plusZero
, (:<:)(..), succLim
, Index(..), unIndex, succI, index0, index1, index2, index3
, coerceToIndex
) where
import Prelude hiding (foldr,sum)
import Data.Maybe (isJust)
import Data.Constraint (Dict(..))
import Data.Proof.EQ
import TypeUnary.TyNat
data Nat :: * -> * where
Zero :: Nat Z
Succ :: IsNat n => Nat n -> Nat (S n)
instance Show (Nat n) where
show n = show (natToZ n :: Integer)
withIsNat :: (IsNat n => Nat n -> a) -> (Nat n -> a)
withIsNat p Zero = p Zero
withIsNat p (Succ n) = p (Succ n)
natSucc :: Nat n -> Nat (S n)
natSucc = withIsNat Succ
natIsNat :: Nat n -> (IsNat n => Nat n)
natIsNat Zero = Zero
natIsNat (Succ n) = Succ n
predN :: Nat (S n) -> Nat n
predN (Succ n) = n
natToZ :: Num a => Nat n -> a
natToZ Zero = 0
natToZ (Succ n) = ((1+) . natToZ) n
{-# INLINE natToZ #-}
natEq :: Nat m -> Nat n -> Maybe (m :=: n)
Zero `natEq` Zero = Just Refl
Succ m `natEq` Succ n = liftEq <$> (m `natEq` n)
_ `natEq` _ = Nothing
natAdd :: Nat m -> Nat n -> Nat (m :+: n)
Zero `natAdd` n = n
Succ m `natAdd` n = natSucc (m `natAdd` n)
natMul :: forall m n. Nat m -> Nat n -> Nat (m :*: n)
Zero `natMul` _ = Zero
Succ m `natMul` n = n `natAdd` (m `natMul` n)
zero :: Nat N0
zero = Zero
one :: Nat N1
one = Succ zero
two :: Nat N2
two = Succ one
three :: Nat N3
three = Succ two
four :: Nat N4
four = Succ three
induction :: forall p .
p Z => (forall n. IsNat n => Dict (p n) -> Dict (p (S n)))
-> (forall n. IsNat n => Dict (p n))
induction s = go nat
where
go :: forall n. Nat n -> Dict (p n)
go Zero = Dict
go (Succ m) = s (go m)
class (n :+: Z) ~ n => PlusZero n
instance (n :+: Z) ~ n => PlusZero n
plusZero :: IsNat n => Dict (PlusZero n)
plusZero = induction (\ Dict -> Dict)
#if 0
class ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r
instance ((p :+: q) :+: r) ~ (p :+: (q :+: r)) => PlusAssocR p q r
plusAssocR :: (IsNat p, IsNat q, IsNat r) => Dict (PlusAssocR p q r)
plusAssocR ...
#endif
infix 4 :<:
data m :<: n where
ZLess :: Z :<: S n
SLess :: m :<: n -> S m :<: S n
succLim :: m :<: n -> m :<: S n
succLim ZLess = ZLess
succLim (SLess p) = SLess (succLim p)
data Index lim = forall n. IsNat n => Index (n :<: lim) (Nat n)
unIndex :: Num a => Index m -> a
unIndex (Index _ j) = natToZ j
instance Eq (Index lim) where
Index _ n == Index _ n' = isJust (n `natEq` n')
succI :: Index m -> Index (S m)
succI (Index p n) = Index (SLess p) (Succ n)
index0 :: Index (N1 :+: m)
index0 = Index ZLess Zero
index1 :: Index (N2 :+: m)
index1 = succI index0
index2 :: Index (N3 :+: m)
index2 = succI index1
index3 :: Index (N4 :+: m)
index3 = succI index2
coerceToIndex :: (Eq i, Show i, Num i, IsNat m) => i -> Index m
coerceToIndex = coerceToIndex' nat
coerceToIndex' :: (Eq i, Show i, Num i) => Nat m -> i -> Index m
coerceToIndex' mOrig niOrig = loop mOrig niOrig
where
loop :: (Eq i, Show i, Num i) => Nat m -> i -> Index m
loop Zero _ = error $ "coerceToIndex: out of bounds: "
++ show niOrig ++ " should be less than "
++ show mOrig
loop (Succ _) 0 = Index ZLess Zero
loop (Succ m') ni' = succI (loop m' (ni'-1))
instance Show (Index n) where
show (Index _ n) = show n
instance IsNat n => Num (Index n) where
fromInteger = coerceToIndex
(+) = noIndex "(+)"
(*) = noIndex "(*)"
abs = noIndex "abs"
signum = noIndex "signum"
negate = noIndex "negate"
noIndex :: String -> a
noIndex meth = error (meth ++ ": no method for Index n. Sorry.")
class IsNat n where nat :: Nat n
instance IsNat Z where nat = Zero
instance IsNat n => IsNat (S n) where nat = Succ nat