From b3c104ebefb71eb16b137f610fcf79fd060eedc7 Mon Sep 17 00:00:00 2001 From: mniip Date: Wed, 11 Jul 2018 12:49:49 +0300 Subject: [PATCH] Enhance the documentation --- GHC/TypeLits/Induction.hs | 18 ++++++++++++++++++ GHC/TypeLits/Singletons.hs | 24 ++++++++++++++++++++++++ singleton-typelits.cabal | 24 +++++++++++++++++++++++- 3 files changed, 65 insertions(+), 1 deletion(-) diff --git a/GHC/TypeLits/Induction.hs b/GHC/TypeLits/Induction.hs index 05a646d..12cf06c 100644 --- a/GHC/TypeLits/Induction.hs +++ b/GHC/TypeLits/Induction.hs @@ -38,6 +38,9 @@ induceIsZero = go natSingleton go IsNonZero y z = y -- | \((\forall n. P(n) \to P(n + 1)) \to P(0) \to \forall m. P(m)\) +-- For example: +-- +-- > inducePeano f z :: p 3 = f (f (f z)) inducePeano :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 0 -> p m inducePeano = go natSingleton where @@ -46,6 +49,9 @@ inducePeano = go natSingleton 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)\) +-- For example: +-- +-- > induceTwosComp f1 f2 z :: p 12 = f2 (f1 (f2 z)) 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 @@ -55,6 +61,9 @@ induceTwosComp = go natSingleton 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)\) +-- For example: +-- +-- > induceBaseComp (_ :: r 10) d f z :: p 123 = (d :: q 2) `f` ((d :: q 1) `f` ((d :: q 0) `f` z) 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 @@ -63,6 +72,9 @@ induceBaseComp _ = go natSingleton 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)\) +-- For example: +-- +-- > induceUnary f o :: p 5 = f (f (f (f o))) induceUnary :: KnownNat m => (forall n. KnownNat n => p n -> p (1 + n)) -> p 1 -> p (1 + m) induceUnary = go posSingleton where @@ -71,6 +83,9 @@ induceUnary = go posSingleton 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)\) +-- For example: +-- +-- > inducePosBinary f0 f1 o :: p 10 = f0 (f1 (f0 o)) 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 @@ -80,6 +95,9 @@ inducePosBinary = go posSingleton 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)\) +-- For example: +-- +-- > inducePosBase (_ :: r 10) d f l :: p 123 = (d :: q 3) `f` ((d :: q 2) `f` l (d :: q 1)) 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 diff --git a/GHC/TypeLits/Singletons.hs b/GHC/TypeLits/Singletons.hs index 8d588e0..4d3f64e 100644 --- a/GHC/TypeLits/Singletons.hs +++ b/GHC/TypeLits/Singletons.hs @@ -62,6 +62,10 @@ instance NatSingleton NatIsZero where Nothing -> error $ "Malformed KnownNat instance: " ++ show n -- | A natural number is either 0 or a successor of another natural number. +-- +-- For example, @3 = 1 + (1 + (1 + 0))@: +-- +-- > PeanoSucc (PeanoSucc (PeanoSucc PeanoZero)) :: NatPeano 3 data NatPeano (n :: Nat) where PeanoZero :: NatPeano 0 PeanoSucc :: KnownNat n => NatPeano n -> NatPeano (1 + n) @@ -75,6 +79,10 @@ instance NatSingleton NatPeano where IsNonZero -> PeanoSucc natSingleton -- | A natural number is either 0, or twice another natural number plus 1 or 2. +-- +-- For example, @12 = 2 + 2 * (1 + 2 * (2 + 2 * 0))@: +-- +-- > TwosCompx2p2 (TwosCompx2p1 (TwosCompx2p2 TwosCompZero)) :: NatTwosComp 12 data NatTwosComp (n :: Nat) where TwosCompZero :: NatTwosComp 0 TwosCompx2p1 :: KnownNat n => NatTwosComp n -> NatTwosComp (1 + 2 * n) @@ -93,6 +101,10 @@ instance NatSingleton NatTwosComp where 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]@. +-- +-- For example, @123 = (2 + 1) + 10 * ((1 + 1) + 10 * ((0 + 1) + 10 * 0))@: +-- +-- > BaseCompxBp1p (natSingleton :: p 2) (BaseCompxBp1p (natSingleton :: p 1) (BaseCompxBp1p (natSingleton :: p 0) BaseCompZero)) :: NatBaseComp p 10 123 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) @@ -122,6 +134,10 @@ instance PositiveSingleton Proxy where posSingleton = Proxy -- | A positive number is either 1 or a successor of another positive number. +-- +-- For example, @5 = 1 + (1 + (1 + (1 + 1)))@: +-- +-- > UnarySucc (UnarySucc (UnarySucc (UnarySucc UnaryOne))) :: Unary 5 data Unary (n :: Nat) where UnaryOne :: Unary 1 UnarySucc :: KnownNat n => Unary n -> Unary (1 + n) @@ -135,6 +151,10 @@ instance PositiveSingleton Unary where IsNonZero -> UnarySucc posSingleton -- | A positive number is either 1, or twice another positive number plus 0 or 1. +-- +-- For example, @10 = 0 + 2 * (1 + 2 * (0 + 2 * 1))@: +-- +-- > Bin0 (Bin1 (Bin0 BinOne)) :: PosBinary 10 data PosBinary (n :: Nat) where BinOne :: PosBinary 1 Bin0 :: KnownNat n => PosBinary n -> PosBinary (2 * n) @@ -156,6 +176,10 @@ instance PositiveSingleton PosBinary where 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)@. +-- +-- For example, @123 = 3 + 10 * (2 + 10 * 1)@: +-- +-- > BaseDigit (natSingleton :: p 3) (BaseDigit (natSingleton :: p 2) (BaseLead (natSingleton :: p 1))) :: PosBase p 10 123 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) diff --git a/singleton-typelits.cabal b/singleton-typelits.cabal index b6f1af9..89894ab 100644 --- a/singleton-typelits.cabal +++ b/singleton-typelits.cabal @@ -1,7 +1,29 @@ name: singleton-typelits version: 0.0.0.1 synopsis: Singletons and induction over GHC TypeLits -description: Singletons and induction schemes over 'GHC.TypeLits.Nat' +description: + Singletons and induction schemes over 'GHC.TypeLits.Nat'. + . + While the TypeLits interface provided by GHC does allow case-analysing the + values of the naturals ('GHC.TypeLits.natVal'), it does not facilitate writing + type-safe programs involving that AP, if one were to write: + . + > case natVal (x :: Proxy n) of 0 -> foo x + . + In the RHS of this pattern match @n@ is equal to @0@ but this isn't something + GHC can reason about, as this is an ordinary pattern match on an 'Integer'. + If the type of @foo@ was @Proxy 0 -> ...@ this wouldn't typecheck and one + would have to resort to @unsafeCoerce@. In order to make GHC infer something + like this, @natVal@ needs to return a GADT that includes proofs about the + natural number it refers to, such that when pattern matching on that GADT the + proofs become available to the typechecker. + . + This package provides a handful of variants of such GADTs for overcoming this + type of issue, as well as functions to do typesafe induction on naturals + without resorting to manual GADT unpacking. The most basic form of induction - + Peano-style induction (P(0) and P(n) implies P(n + 1)) can be inefficient in + practice on large numbers, so this package also provides more efficient binary + and arbitrary-base induction schemes. homepage: https://github.com/mniip/singleton-typelits license: BSD3 license-file: LICENSE