Singletons.hs

{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-}

module GHC.TypeLits.Singletons
	(
		NatSingleton(..),
		NatIsZero(..), induceIsZero,
		NatUnary(..), induceUnary,
		NatTwosComp(..), induceTwosComp,
		NatBaseComp(..), induceBaseComp,
		
		PositiveSingleton(..),
		Peano(..), inducePeano,
		PosBinary(..), inducePosBinary,
		PosBase(..), inducePosBase,
	)
	where

import GHC.TypeLits
import Data.Type.Equality
import Unsafe.Coerce
import Data.Proxy

class NatSingleton (p :: Nat -> *) where
	natSingleton :: KnownNat n => p n

instance NatSingleton Proxy where
	natSingleton = Proxy

data NatIsZero (n :: Nat) where
	Zero :: NatIsZero 0
	NonZero :: KnownNat n => NatIsZero (1 + n)
deriving instance Show (NatIsZero n)

instance NatSingleton NatIsZero where
	natSingleton :: forall n. KnownNat n => NatIsZero n
	natSingleton = case natVal (Proxy :: Proxy n) of
		0 -> (unsafeCoerce :: NatIsZero 0 -> NatIsZero n) Zero
		n -> case someNatVal (n - 1) of
			Just (SomeNat (p :: Proxy m)) -> (unsafeCoerce :: NatIsZero (1 + m) -> NatIsZero n) $ NonZero
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n

induceIsZero :: KnownNat m => (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m
induceIsZero = go natSingleton
	where
		go :: NatIsZero m -> (forall n. KnownNat n => p (1 + n)) -> p 0 -> p m
		go Zero y z = z
		go NonZero y z = y

data NatUnary (n :: Nat) where
	UnaryZero :: NatUnary 0
	UnarySucc :: KnownNat n => NatUnary n -> NatUnary (1 + n)
deriving instance Show (NatUnary n)

instance NatSingleton NatUnary where
	natSingleton :: forall n. KnownNat n => NatUnary n
	natSingleton = case natSingleton :: NatIsZero n of
		Zero -> UnaryZero
		NonZero -> UnarySucc natSingleton

induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m
induceUnary = go natSingleton
	where
		go :: NatUnary m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m
		go UnaryZero f z = z
		go (UnarySucc n) f z = f (go n f z)

data NatTwosComp (n :: Nat) where
	TwosCompZero :: NatTwosComp 0
	TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + 2 * n)
	TwosCompx2p2 :: KnownNat n => NatTwosComp n -> NatTwosComp (2 + 2 * n)
deriving instance Show (NatTwosComp n)

instance NatSingleton NatTwosComp where
	natSingleton :: forall n. KnownNat n => NatTwosComp n
	natSingleton = case natVal (Proxy :: Proxy n) of
		0 -> (unsafeCoerce :: NatTwosComp 0 -> NatTwosComp n) TwosCompZero
		n -> case someNatVal ((n - 1) `div` 2) of
			Just (SomeNat (p :: Proxy m)) -> if even n
				then (unsafeCoerce :: NatTwosComp (2 + 2 * m) -> NatTwosComp n) $ TwosCompx2p2 natSingleton
				else (unsafeCoerce :: NatTwosComp (1 + 2 * m) -> NatTwosComp n) $ TwosCompx2p1 natSingleton
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n

induceTwosComp :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> (forall n. KnownNat n => p n -> p (2 + 2 * n)) -> p 0 -> p m
induceTwosComp = go natSingleton
	where
		go :: NatTwosComp m -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> (forall n. KnownNat n => p n -> p (2 + 2 * n)) -> p 0 -> p m
		go TwosCompZero f g z = z
		go (TwosCompx2p1 n) f g z = f (go n f g z)
		go (TwosCompx2p2 n) f g z = g (go n f g z)

data NatBaseComp (p :: Nat -> *) (b :: Nat) (n :: Nat) where
	BaseCompZero :: NatBaseComp p b 0
	BaseCompxBp1p :: (KnownNat k, 1 + k <= b, KnownNat n) => p k -> NatBaseComp p b n -> NatBaseComp p b (1 + k + b * n)

instance (KnownNat b, NatSingleton p) => NatSingleton (NatBaseComp p b) where
	natSingleton :: forall n. KnownNat n => NatBaseComp p b n
	natSingleton = case natVal (Proxy :: Proxy n) of
		0 -> (unsafeCoerce :: NatBaseComp p b 0 -> NatBaseComp p b n) BaseCompZero
		n -> case someNatVal ((n - 1) `div` base) of
			Just (SomeNat (p :: Proxy m)) -> case someNatVal ((n - 1) `mod` base) of
				Just (SomeNat (p :: Proxy k)) -> (unsafeCoerce :: NatBaseComp p b (1 + k + b * m) -> NatBaseComp p b n) $ case unsafeCoerce Refl :: (1 + k <=? b) :~: True of
					Refl -> BaseCompxBp1p (natSingleton :: p k) (natSingleton :: NatBaseComp p b m)
				Nothing -> error $ "Malformed KnownNat instance: " ++ show base
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n
		where
			base = natVal (Proxy :: Proxy b)

induceBaseComp :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (1 + k + b * n)) -> p 0 -> p m
induceBaseComp _ = go natSingleton
	where
		go :: forall m. NatBaseComp Proxy b m -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (1 + k + b * n)) -> p 0 -> p m
		go BaseCompZero q f z = z
		go (BaseCompxBp1p k n) q f z = f q (go n q f z)

class PositiveSingleton (p :: Nat -> *) where
	posSingleton :: KnownNat n => p (1 + n)


data Peano (n :: Nat) where
	PeanoOne :: Peano 1
	PeanoSucc :: KnownNat n => Peano n -> Peano (1 + n)
deriving instance Show (Peano n)

instance PositiveSingleton Peano where
	posSingleton :: forall n. KnownNat n => Peano (1 + n)
	posSingleton = case natSingleton :: NatIsZero n of
		Zero -> PeanoOne
		NonZero -> PeanoSucc posSingleton

inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + m)
inducePeano = go posSingleton
	where
		go :: Peano m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p m
		go PeanoOne f o = o
		go (PeanoSucc n) f o = f (go n f o)

data PosBinary (n :: Nat) where
	BinOne :: PosBinary 1
	Bin0 :: KnownNat n => PosBinary n -> PosBinary (2 * n)
	Bin1 :: KnownNat n => PosBinary n -> PosBinary (1 + 2 * n)
deriving instance Show (PosBinary n)

instance PositiveSingleton PosBinary where
	posSingleton :: forall n. KnownNat n => PosBinary (1 + n)
	posSingleton = case natVal (Proxy :: Proxy n) of
		0 -> (unsafeCoerce :: PosBinary 1 -> PosBinary (1 + n)) BinOne
		n -> case someNatVal ((n - 1) `div` 2) of
			Just (SomeNat (p :: Proxy m)) -> case someNatVal (natVal (Proxy :: Proxy m) + 1) of
				Just (SomeNat (q :: Proxy l)) -> case unsafeCoerce Refl :: l :~: 1 + m of
					Refl -> if even n
						then (unsafeCoerce :: PosBinary (1 + 2 * l) -> PosBinary (1 + n)) $ Bin1 posSingleton
						else (unsafeCoerce :: PosBinary (2 * l) -> PosBinary (1 + n)) $ Bin0 posSingleton
				Nothing -> error $ "Malformed KnownNat instance: " ++ show n
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n

inducePosBinary :: KnownNat m => (forall n. KnownNat n => p n -> p (2 * n)) -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> p 1 -> p (1 + m)
inducePosBinary = go posSingleton
	where
		go :: PosBinary m -> (forall n. KnownNat n => p n -> p (2 * n)) -> (forall n. KnownNat n => p n -> p (1 + 2 * n)) -> p 1 -> p m
		go BinOne f g z = z
		go (Bin0 n) f g z = f (go n f g z)
		go (Bin1 n) f g z = g (go n f g z)

data PosBase (p :: Nat -> *) (b :: Nat) (n :: Nat) where
	BaseLead :: (KnownNat k, 1 + k <= b, k ~ (1 + n)) => p k -> PosBase p b k
	BaseDigit :: (KnownNat k, 1 + k <= b, KnownNat n) => p k -> PosBase p b n -> PosBase p b (k + b * n)

instance (KnownNat b, NatSingleton p) => PositiveSingleton (PosBase p b) where
	posSingleton :: forall n. KnownNat n => PosBase p b (1 + n)
	posSingleton = case natVal (Proxy :: Proxy n) of
		n | n < base - 1 -> case someNatVal (n + 1) of
			Just (SomeNat (p :: Proxy k)) -> case unsafeCoerce Refl :: k :~: (1 + n) of
				Refl -> case unsafeCoerce Refl :: (1 + (1 + n) <=? b) :~: True of
					Refl -> BaseLead natSingleton
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n
		n -> case someNatVal ((n - base + 1) `div` base) of
			Just (SomeNat (p :: Proxy m)) -> case someNatVal (natVal (Proxy :: Proxy m) + 1) of
				Just (SomeNat (q :: Proxy l)) -> case unsafeCoerce Refl :: l :~: 1 + m of
					Refl -> case someNatVal ((n - base + 1) `mod` base) of
						Just (SomeNat (p :: Proxy k)) -> (unsafeCoerce :: PosBase p b (k + b * l) -> PosBase p b (1 + n)) $ case unsafeCoerce Refl :: (1 + k <=? b) :~: True of
							Refl -> BaseDigit (natSingleton :: p k) (posSingleton :: PosBase p b l)
						Nothing -> error $ "Malformed KnownNat instance: " ++ show base
				Nothing -> error $ "Malformed KnownNat instance: " ++ show base
			Nothing -> error $ "Malformed KnownNat instance: " ++ show n
		where
			base = natVal (Proxy :: Proxy b)

inducePosBase :: forall r b q p m. (KnownNat b, KnownNat m) => r b -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (k + b * n)) -> (forall k n. (KnownNat k, 1 + k <= b, k ~ (1 + n)) => q k -> p k) -> p (1 + m)
inducePosBase _ = go posSingleton
	where
		go :: forall m. PosBase Proxy b m  -> (forall m. KnownNat m => q m) -> (forall k n. (KnownNat b, 1 + k <= b, KnownNat n) => q k -> p n -> p (k + b * n)) -> (forall k n. (KnownNat k, 1 + k <= b, k ~ (1 + n)) => q k -> p k) -> p m
		go (BaseLead n) q f g = g q
		go (BaseDigit k n) q f g = f q (go n q f g)