Initial commit
This commit is contained in:
mniip
commit
2b62656721
5 changed files with 320 additions and 0 deletions
87
GHC/TypeLits/Induction.hs
Normal file
87
GHC/TypeLits/Induction.hs
Normal file
|
|
@ -0,0 +1,87 @@
|
|||
-- |
|
||||
-- Module : GHC.TypeLits.Induction
|
||||
-- Description : Induction for GHC TypeLits
|
||||
-- Copyright : (C) 2017 mniip
|
||||
-- License : MIT
|
||||
-- Maintainer : mniip@mniip.com
|
||||
-- Stability : experimental
|
||||
-- Portability : portable
|
||||
{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-}
|
||||
{-# OPTIONS_GHC -fno-warn-tabs #-}
|
||||
|
||||
module GHC.TypeLits.Induction
|
||||
(
|
||||
-- * Natural number induction
|
||||
induceIsZero,
|
||||
inducePeano,
|
||||
induceTwosComp,
|
||||
induceBaseComp,
|
||||
|
||||
-- * Positive number induction
|
||||
induceUnary,
|
||||
inducePosBinary,
|
||||
inducePosBase
|
||||
)
|
||||
where
|
||||
|
||||
import Data.Proxy
|
||||
import GHC.TypeLits
|
||||
import GHC.TypeLits.Singletons
|
||||
|
||||
-- | \((\forall n. n > 0 \to P(n)) \to P(0) \to \forall m. P(m)\)
|
||||
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 IsZero y z = z
|
||||
go IsNonZero y z = y
|
||||
|
||||
-- | \((\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m)\)
|
||||
inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m
|
||||
inducePeano = go natSingleton
|
||||
where
|
||||
go :: NatPeano m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m
|
||||
go PeanoZero f z = z
|
||||
go (PeanoSucc n) f z = f (go n f z)
|
||||
|
||||
-- | \((\forall n. P(n) \to P(2n + 1)) \to \\ (\forall n. P(n) \to P(2n + 2)) \to \\ P(0) \to \\ \forall m. P(m)\)
|
||||
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)
|
||||
|
||||
-- | \(\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d + 1)) \to \\ \forall m. P(m)\)
|
||||
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, 1 + m <= b) => 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)
|
||||
|
||||
-- | \((\forall n. P(n) \to P(n + 1)) \to P(1) \to \forall m > 0. P(m)\)
|
||||
induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + m)
|
||||
induceUnary = go posSingleton
|
||||
where
|
||||
go :: Unary m -> (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p m
|
||||
go UnaryOne f o = o
|
||||
go (UnarySucc n) f o = f (go n f o)
|
||||
|
||||
-- | \((\forall n. P(n) \to P(2n)) \to \\ (\forall n. P(n) \to P(2n + 1)) \to \\ P(1) \to \\ \forall m > 0. P(m)\)
|
||||
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)
|
||||
|
||||
-- | \(\forall b. (\prod_d Q(d)) \to \\ (\forall n. \forall d. d < b \to Q(d) \to P(n) \to P(bn + d)) \to \\ (\forall d. d > 0 \to d < b \to Q(d) \to P(d)) \to \\ \forall m > 0. P (m)\)
|
||||
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)
|
||||
184
GHC/TypeLits/Singletons.hs
Normal file
184
GHC/TypeLits/Singletons.hs
Normal file
|
|
@ -0,0 +1,184 @@
|
|||
-- |
|
||||
-- Module : GHC.TypeLits.Singletons
|
||||
-- Description : Singletons for GHC TypeLits
|
||||
-- Copyright : (C) 2017 mniip
|
||||
-- License : MIT
|
||||
-- Maintainer : mniip@mniip.com
|
||||
-- Stability : experimental
|
||||
-- Portability : portable
|
||||
{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-}
|
||||
{-# OPTIONS_GHC -fno-warn-tabs #-}
|
||||
|
||||
module GHC.TypeLits.Singletons
|
||||
(
|
||||
-- * Natural number singletons
|
||||
NatSingleton(..),
|
||||
NatIsZero(..),
|
||||
NatPeano(..),
|
||||
NatTwosComp(..),
|
||||
NatBaseComp(..),
|
||||
|
||||
-- * Positive number singleton
|
||||
PositiveSingleton(..),
|
||||
Unary(..),
|
||||
PosBinary(..),
|
||||
PosBase(..),
|
||||
|
||||
ShowN(..)
|
||||
)
|
||||
where
|
||||
|
||||
import GHC.TypeLits
|
||||
import Data.Type.Equality
|
||||
import Unsafe.Coerce
|
||||
import Data.Proxy
|
||||
|
||||
-- | A class of singletons capable of representing any 'KnownNat' natural number.
|
||||
class NatSingleton (p :: Nat -> *) where
|
||||
natSingleton :: KnownNat n => p n
|
||||
|
||||
-- | Auxiliary class for implementing 'Show' on higher-kinded singletons.
|
||||
class ShowN (p :: Nat -> *) where showsPrecN :: Int -> p n -> ShowS
|
||||
|
||||
instance ShowN Proxy where showsPrecN = showsPrec
|
||||
|
||||
instance NatSingleton Proxy where
|
||||
natSingleton = Proxy
|
||||
|
||||
-- | A natural number is either 0 or 1 plus something.
|
||||
data NatIsZero (n :: Nat) where
|
||||
IsZero :: NatIsZero 0
|
||||
IsNonZero :: KnownNat n => NatIsZero (1 + n)
|
||||
deriving instance Show (NatIsZero n)
|
||||
instance ShowN NatIsZero where showsPrecN = showsPrec
|
||||
|
||||
instance NatSingleton NatIsZero where
|
||||
natSingleton :: forall n. KnownNat n => NatIsZero n
|
||||
natSingleton = case natVal (Proxy :: Proxy n) of
|
||||
0 -> (unsafeCoerce :: NatIsZero 0 -> NatIsZero n) IsZero
|
||||
n -> case someNatVal (n - 1) of
|
||||
Just (SomeNat (p :: Proxy m)) -> (unsafeCoerce :: NatIsZero (1 + m) -> NatIsZero n) $ IsNonZero
|
||||
Nothing -> error $ "Malformed KnownNat instance: " ++ show n
|
||||
|
||||
-- | A natural number is either 0 or a successor of another natural number.
|
||||
data NatPeano (n :: Nat) where
|
||||
PeanoZero :: NatPeano 0
|
||||
PeanoSucc :: KnownNat n => NatPeano n -> NatPeano (1 + n)
|
||||
deriving instance Show (NatPeano n)
|
||||
instance ShowN NatPeano where showsPrecN = showsPrec
|
||||
|
||||
instance NatSingleton NatPeano where
|
||||
natSingleton :: forall n. KnownNat n => NatPeano n
|
||||
natSingleton = case natSingleton :: NatIsZero n of
|
||||
IsZero -> PeanoZero
|
||||
IsNonZero -> PeanoSucc natSingleton
|
||||
|
||||
-- | A natural number is either 0, or twice another natural number plus 1 or 2.
|
||||
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 ShowN NatTwosComp where showsPrecN = showsPrec
|
||||
|
||||
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
|
||||
|
||||
-- | A natural number is either 0, or @b@ times another natural number plus a digit in @[1, b]@.
|
||||
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 ShowN p => Show (NatBaseComp p b n) where
|
||||
showsPrec d BaseCompZero = showString "BaseCompZero"
|
||||
showsPrec d (BaseCompxBp1p a b) = showParen (d > 10) $ showString "BaseCompxBp1p " . showsPrecN 11 a . showString " " . showsPrec 11 b
|
||||
instance ShowN p => ShowN (NatBaseComp p b) where showsPrecN = showsPrec
|
||||
|
||||
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)
|
||||
|
||||
-- | A class of singletons capable of representing postive 'KnownNat' natural numbers.
|
||||
class PositiveSingleton (p :: Nat -> *) where
|
||||
posSingleton :: KnownNat n => p (1 + n)
|
||||
|
||||
instance PositiveSingleton Proxy where
|
||||
posSingleton = Proxy
|
||||
|
||||
-- | A positive number is either 1 or a successor of another positive number.
|
||||
data Unary (n :: Nat) where
|
||||
UnaryOne :: Unary 1
|
||||
UnarySucc :: KnownNat n => Unary n -> Unary (1 + n)
|
||||
deriving instance Show (Unary n)
|
||||
instance ShowN Unary where showsPrecN = showsPrec
|
||||
|
||||
instance PositiveSingleton Unary where
|
||||
posSingleton :: forall n. KnownNat n => Unary (1 + n)
|
||||
posSingleton = case natSingleton :: NatIsZero n of
|
||||
IsZero -> UnaryOne
|
||||
IsNonZero -> UnarySucc posSingleton
|
||||
|
||||
-- | A positive number is either 1, or twice another positive number plus 0 or 1.
|
||||
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 ShowN PosBinary where showsPrecN = showsPrec
|
||||
|
||||
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
|
||||
|
||||
-- | A positive number is either a digit in @[1, b)@, or another positive number times @b@ plus a digit in @[0, b)@.
|
||||
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 ShowN p => Show (PosBase p b n) where
|
||||
showsPrec d (BaseLead a) = showParen (d > 10) $ showString "BaseLead " . showsPrecN 11 a
|
||||
showsPrec d (BaseDigit a b) = showParen (d > 10) $ showString "BaseDigit " . showsPrecN 11 a . showString " " . showsPrec 11 b
|
||||
instance ShowN p => ShowN (PosBase p b) where showsPrecN = showsPrec
|
||||
|
||||
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)
|
||||
Loading…
Add table
Add a link
Reference in a new issue