summaryrefslogtreecommitdiff
diff options
context:
space:
mode:
authormniip <>2018-07-11 18:33:00 (GMT)
committerhdiff <hdiff@hdiff.luite.com>2018-07-11 18:33:00 (GMT)
commit7532d313083a96a1cf34f9d179dbfb5cd8820cfc (patch)
tree4770aa1892b8beded6c7bcef5d6b92716b80e621
parentafbe03fc025a507394d450ff8c88e81f177f10b4 (diff)
version 0.1.0.0HEAD0.1.0.0master
-rw-r--r--GHC/TypeLits/Induction.hs45
-rw-r--r--GHC/TypeLits/Singletons.hs37
-rw-r--r--LICENSE2
-rw-r--r--singleton-typelits.cabal28
4 files changed, 94 insertions, 18 deletions
diff --git a/GHC/TypeLits/Induction.hs b/GHC/TypeLits/Induction.hs
index 56ec5b5..a05c429 100644
--- a/GHC/TypeLits/Induction.hs
+++ b/GHC/TypeLits/Induction.hs
@@ -1,12 +1,13 @@
-- |
-- Module : GHC.TypeLits.Induction
-- Description : Induction for GHC TypeLits
--- Copyright : (C) 2017 mniip
+-- Copyright : (C) 2017-2018 mniip
-- License : MIT
-- Maintainer : mniip@mniip.com
--- Stability : experimental
+-- Stability : stable
-- Portability : portable
{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-}
+{-# LANGUAGE Safe #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module GHC.TypeLits.Induction
@@ -37,6 +38,10 @@ 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
@@ -45,6 +50,10 @@ 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
@@ -54,14 +63,24 @@ 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)\)
-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
+--
+-- For example:
+--
+-- > induceBaseComp (_ :: s q) (_ :: r 10) d f z :: p 123 = (d :: q 2) `f` ((d :: q 1) `f` ((d :: q 0) `f` z)
+--
+-- The @s q@ parameter is necessary because presently GHC is unable to unify @q@ under the equational constraint @1 + k <= b@.
+induceBaseComp :: forall r b q p m c s. (KnownNat b, b ~ (1 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, 1 + k <= b) => q k) -> (forall k n. (KnownNat k, 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 :: forall m. NatBaseComp Proxy b m -> (forall k. (KnownNat k, 1 + k <= b) => q k) -> (forall k n. (KnownNat k, 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)\)
+--
+-- 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
@@ -70,6 +89,10 @@ 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
@@ -79,9 +102,15 @@ 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)\)
-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
+--
+-- For example:
+--
+-- > inducePosBase (_ :: s q) (_ :: r 10) d f l :: p 123 = (d :: q 3) `f` ((d :: q 2) `f` l (d :: q 1))
+--
+-- The @s q@ parameter is necessary because presently GHC is unable to unify @q@ under the equational constraint @1 + k <= b@.
+inducePosBase :: forall r b q p m c s. (KnownNat b, b ~ (2 + c), KnownNat m) => s q -> r b -> (forall k. (KnownNat k, 1 + k <= b) => q k) -> (forall k n. (KnownNat k, 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 :: forall m. PosBase Proxy b m -> (forall k. (KnownNat k, 1 + k <= b) => q k) -> (forall k n. (KnownNat k, 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)
diff --git a/GHC/TypeLits/Singletons.hs b/GHC/TypeLits/Singletons.hs
index 1a146cf..e3ec64c 100644
--- a/GHC/TypeLits/Singletons.hs
+++ b/GHC/TypeLits/Singletons.hs
@@ -1,12 +1,13 @@
-- |
-- Module : GHC.TypeLits.Singletons
-- Description : Singletons for GHC TypeLits
--- Copyright : (C) 2017 mniip
+-- Copyright : (C) 2017-2018 mniip
-- License : MIT
-- Maintainer : mniip@mniip.com
--- Stability : experimental
+-- Stability : stable
-- Portability : portable
{-# LANGUAGE TypeOperators, KindSignatures, DataKinds, PolyKinds, GADTs, RankNTypes, StandaloneDeriving, InstanceSigs, ScopedTypeVariables #-}
+{-# LANGUAGE Trustworthy #-}
{-# OPTIONS_GHC -fno-warn-tabs #-}
module GHC.TypeLits.Singletons
@@ -61,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)
@@ -74,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)
@@ -92,15 +101,19 @@ 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)
+ BaseCompZero :: (KnownNat b, b ~ (1 + c)) => NatBaseComp p b 0
+ BaseCompxBp1p :: (KnownNat b, b ~ (1 + c), 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
+instance (KnownNat b, b ~ (1 + c), 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
@@ -121,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)
@@ -134,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)
@@ -155,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)
@@ -163,7 +188,7 @@ instance ShowN p => Show (PosBase p b n) where
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
+instance (KnownNat b, b ~ (2 + c), 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
diff --git a/LICENSE b/LICENSE
index 450ec63..55a790b 100644
--- a/LICENSE
+++ b/LICENSE
@@ -1,4 +1,4 @@
-Copyright (c) 2017, mniip
+Copyright (c) 2017-2018, mniip
All rights reserved.
diff --git a/singleton-typelits.cabal b/singleton-typelits.cabal
index 4994375..da6b48b 100644
--- a/singleton-typelits.cabal
+++ b/singleton-typelits.cabal
@@ -1,7 +1,29 @@
name: singleton-typelits
-version: 0.0.0.0
+version: 0.1.0.0
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
@@ -13,5 +35,5 @@ cabal-version: >=1.10
library
exposed-modules: GHC.TypeLits.Singletons, GHC.TypeLits.Induction
- build-depends: base >=4.9 && <4.11
+ build-depends: base >=4.9 && <4.12
default-language: Haskell2010