Enhance the documentation

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

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)

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