typelits-witnesses 0.1.1.0 → 0.1.2.0

raw patch · 4 files changed

+163/−45 lines, 4 filesdep ~basePVP ok

version bump matches the API change (PVP)

Dependency ranges changed: base

API changes (from Hackage documentation)

Files

• README.md +20/−0
• src/GHC/TypeLits/List.hs +134/−37
• src/GHC/TypeLits/Witnesses.hs +7/−6
• typelits-witnesses.cabal +2/−2

@@ -1,6 +1,13 @@ typelits-witnesses ================== +[![typelits-witnesses on Stackage LTS 2](http://stackage.org/package/typelits-witnesses/badge/lts-2)](http://stackage.org/lts-2/package/typelits-witnesses)+[![typelits-witnesses on Stackage LTS 3](http://stackage.org/package/typelits-witnesses/badge/lts-3)](http://stackage.org/lts-3/package/typelits-witnesses)+[![typelits-witnesses on Stackage LTS 4](http://stackage.org/package/typelits-witnesses/badge/lts-4)](http://stackage.org/lts-4/package/typelits-witnesses)+[![typelits-witnesses on Stackage LTS](http://stackage.org/package/typelits-witnesses/badge/lts)](http://stackage.org/lts/package/typelits-witnesses)+[![typelits-witnesses on Stackage Nightly](http://stackage.org/package/typelits-witnesses/badge/nightly)](http://stackage.org/nightly/package/typelits-witnesses)++ Provides witnesses for `KnownNat` and `KnownSymbol` instances for various operations on GHC TypeLits --- in particular, the arithmetic operations defined in `GHC.TypeLits`, and also for type-level lists of `KnownNat` and@@ -131,6 +138,19 @@ 2 3 ~~~++Another thing you can do is provide witneses that two `[Nat]`s or `[Symbol]`s+are the same/were instantiated with the same numbers/symbols.++~~~haskell+> reifyNats [1,2,3] $ \ns -> do+  reifyNats [1,2,3] $ \ms -> do+    case sameNats ns ms of+      Just Refl -> -- in this branch, ns and ms are the same.+      Nothing   -> -- in this branch, they aren't+~~~++The above would match on the `Just Refl` branch.  See module documentation for more details and variations. 

@@ -29,33 +29,42 @@ -- existential types for dependent typing usage, and as an analogy with -- 'SomeNat' and 'SomeSymbol'. ----- See typeclass documentations for more information.+-- See typeclass documentations and README for more information.  module GHC.TypeLits.List (-  -- * @KnownNats@+  -- * 'KnownNats'     KnownNats(..)   , SomeNats(..)   , NatList(..)   , someNatsVal   , someNatsVal'   , reifyNats+  , sameNats+  -- ** Traversals   , traverseNatList   , traverseNatList'   , traverseNatList_+  -- *** Maps   , mapNatList-  -- * @KnownSymbols@+  , mapNatList'+  -- * 'KnownSymbols'   , KnownSymbols(..)   , SomeSymbols(..)   , SymbolList(..)   , someSymbolsVal   , reifySymbols+  , sameSymbols+  -- ** Traversals   , traverseSymbolList   , traverseSymbolList'   , traverseSymbolList_+  -- *** Maps   , mapSymbolList+  , mapSymbolList'   ) where  import Data.Proxy+import Data.Type.Equality import Data.Reflection import GHC.TypeLits import Data.Functor.Identity@@ -112,10 +121,11 @@ -- a new one, in a 'SomeNat'. -- -- Can be considered a form of a @Traversal' 'SomeNat' 'SomeNats'@.-traverseNatList :: forall f ns. Applicative f-                => (forall n. KnownNat n => Proxy n -> f SomeNat)-                -> NatList ns-                -> f SomeNats+traverseNatList+    :: forall f ns. Applicative f+    => (forall n. KnownNat n => Proxy n -> f SomeNat)+    -> NatList ns+    -> f SomeNats traverseNatList f = go   where     go :: forall ms. NatList ms -> f SomeNats@@ -129,13 +139,14 @@                          SomeNats is ->                            SomeNats (i :<# is) --- | Like 'traverseNatList', but literally actually a--- @Traversal' 'SomeNat' 'SomeNats'@, so is usable with lens-library+-- | Like 'traverseNatList', but literally actually a @Traversal' 'SomeNat'+-- 'SomeNats'@, avoiding the Rank-2 types, so is usable with lens-library -- machinery.-traverseNatList' :: forall f. Applicative f-                 => (SomeNat -> f SomeNat)-                 -> SomeNats-                 -> f SomeNats+traverseNatList'+    :: forall f. Applicative f+    => (SomeNat -> f SomeNat)+    -> SomeNats+    -> f SomeNats traverseNatList' f ns =     case ns of       SomeNats ns' -> traverseNatList (f . SomeNat) ns'@@ -143,10 +154,11 @@ -- | Utility function for traversing over all of the @'Proxy' n@s in -- a 'NatList', each with the corresponding 'KnownNat' instance available. -- Results are ignored.-traverseNatList_ :: forall f a ns. Applicative f-                 => (forall n. KnownNat n => Proxy n -> f a)-                 -> NatList ns-                 -> f ()+traverseNatList_+    :: forall f a ns. Applicative f+    => (forall n. KnownNat n => Proxy n -> f a)+    -> NatList ns+    -> f () traverseNatList_ f = go   where     go :: forall ms. NatList ms -> f ()@@ -156,11 +168,21 @@  -- | Utility function for \"mapping\" over each of the 'Nat's in the -- 'NatList'.-mapNatList :: (forall n. KnownNat n => Proxy n -> SomeNat)-           -> NatList ns-           -> SomeNats+mapNatList+    :: (forall n. KnownNat n => Proxy n -> SomeNat)+    -> NatList ns+    -> SomeNats mapNatList f = runIdentity . traverseNatList (Identity . f) +-- | Like 'mapNatList', but avoids the Rank-2 types, so can be used with+-- '.' (function composition) and in other situations where 'mapNatList'+-- would cause problems.+mapNatList'+    :: (SomeNat -> SomeNat)+    -> SomeNats+    -> SomeNats+mapNatList' f = runIdentity . traverseNatList' (Identity . f)+ -- | List equivalent of 'someNatVal'.  Convert a list of integers into an -- unknown type-level list of naturals.  Will return 'Nothing' if any of -- the given 'Integer's is negative.@@ -191,6 +213,38 @@ someNatsVal' :: [Integer] -> SomeNats someNatsVal' ns = reifyNats ns SomeNats +-- | Get evidence that the two 'KnownNats' lists are actually the "same"+-- list of 'Nat's (that they were instantiated with the same numbers).+--+-- Essentialy runs 'sameNat' over the lists:+--+-- @+-- case 'sameNats' ns ms of+--   Just 'Refl' -> -- in this branch, GHC recognizes that the two ['Nat']s+--                  -- are the same.+--   Nothing     -> -- in this branch, they aren't+-- @+sameNats+    :: (KnownNats ns, KnownNats ms)+    => NatList ns+    -> NatList ms+    -> Maybe (ns :~: ms)+sameNats ns ms =+    case ns of+      ØNL ->+        case ms of+          ØNL     -> Just Refl+          _ :<# _ -> Nothing+      n :<# ns' ->+        case ms of+          ØNL     -> Nothing+          m :<# ms' -> do+            Refl <- sameNat n m+            Refl <- sameNats ns' ms'+            return Refl+++ -- | @'KnownSymbols' ns@ is intended to represent that every 'Symbol' in the -- type-level list 'ns' is itself a 'KnownSymbol' (meaning, you can use -- 'symbolVal' to get its corresponding 'String').@@ -239,10 +293,11 @@ -- number to a new one, in a 'SomeSymbol'. -- -- Can be considered a form of a @Traversal' 'SomeSymbol' 'SomeSymbols'@.-traverseSymbolList :: forall f ns. Applicative f-                   => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)-                   -> SymbolList ns-                   -> f SomeSymbols+traverseSymbolList+    :: forall f ns. Applicative f+    => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)+    -> SymbolList ns+    -> f SomeSymbols traverseSymbolList f = go   where     go :: forall ms. SymbolList ms -> f SomeSymbols@@ -257,12 +312,13 @@                          SomeSymbols (ps :<$ sl')  -- | Like 'traverseSymbolList', but literally actually a--- @Traversal' 'SomeSymbol' 'SomeSymbols'@, so is usable with lens-library--- machinery.-traverseSymbolList' :: forall f. Applicative f-                 => (SomeSymbol -> f SomeSymbol)-                 -> SomeSymbols-                 -> f SomeSymbols+-- @Traversal' 'SomeSymbol' 'SomeSymbols'@, avoiding the Rank-2 types, so+-- is usable with lens-library machinery.+traverseSymbolList'+    :: forall f. Applicative f+    => (SomeSymbol -> f SomeSymbol)+    -> SomeSymbols+    -> f SomeSymbols traverseSymbolList' f ns =     case ns of       SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns'@@ -270,10 +326,11 @@ -- | Utility function for traversing over all of the @'Proxy' n@s in -- a 'SymbolList', each with the corresponding 'KnownSymbol' instance -- available. Results are ignored.-traverseSymbolList_ :: forall f ns. Applicative f-                    => (forall n a. KnownSymbol n => Proxy n -> f a)-                    -> SymbolList ns-                    -> f ()+traverseSymbolList_+    :: forall f ns. Applicative f+    => (forall n a. KnownSymbol n => Proxy n -> f a)+    -> SymbolList ns+    -> f () traverseSymbolList_ f = go   where     go :: forall ms. SymbolList ms -> f ()@@ -283,11 +340,21 @@  -- | Utility function for \"mapping\" over each of the 'Symbol's in the -- 'SymbolList'.-mapSymbolList :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)-              -> SymbolList ns-              -> SomeSymbols+mapSymbolList+    :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)+    -> SymbolList ns+    -> SomeSymbols mapSymbolList f = runIdentity . traverseSymbolList (Identity . f) +-- | Like 'mapSymbolList', but avoids the Rank-2 types, so can be used with+-- '.' (function composition) and in other situations where 'mapSymbolList'+-- would cause problems.+mapSymbolList'+    :: (SomeSymbol -> SomeSymbol)+    -> SomeSymbols+    -> SomeSymbols+mapSymbolList' f = runIdentity . traverseSymbolList' (Identity . f)+ -- | List equivalent of 'someNatVal'.  Convert a list of integers into an -- unknown type-level list of naturals.  Will return 'Nothing' if any of -- the given 'Integer's is negative.@@ -312,3 +379,33 @@ reifySymbols (n:ns) f = reifySymbol n $ \m ->                           reifySymbols ns $ \ms ->                             f (m :<$ ms)++-- | Get evidence that the two 'KnownSymbols' lists are actually the "same"+-- list of 'Symboles's (that they were instantiated with the same strings).+--+-- Essentialy runs 'sameSymbol' over the lists:+--+-- @+-- case 'sameSymbols' ns ms of+--   Just 'Refl' -> -- in this branch, GHC recognizes that the+--                  -- two ['Symbol']s are the same+--   Nothing     -> -- in this branch, they aren't+-- @+sameSymbols+    :: (KnownSymbols ns, KnownSymbols ms)+    => SymbolList ns+    -> SymbolList ms+    -> Maybe (ns :~: ms)+sameSymbols ns ms =+    case ns of+      ØSL ->+        case ms of+          ØSL     -> Just Refl+          _ :<$ _ -> Nothing+      n :<$ ns' ->+        case ms of+          ØSL     -> Nothing+          m :<$ ms' -> do+            Refl <- sameSymbol n m+            Refl <- sameSymbols ns' ms'+            return Refl

@@ -189,12 +189,13 @@ -- are set to match that of normal addition and multiplication, etc.) -- ---withNatOp :: (KnownNat n, KnownNat m)-          => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))-          -> Proxy n-          -> Proxy m-          -> (KnownNat q => r)-          -> r+withNatOp+    :: (KnownNat n, KnownNat m)+    => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q))+    -> Proxy n+    -> Proxy m+    -> (KnownNat q => r)+    -> r withNatOp op x y r = case natDict x `op` natDict y of                        Dict -> r 

@@ -1,5 +1,5 @@ name:                typelits-witnesses-version:             0.1.1.0+version:             0.1.2.0 synopsis:            Existential witnesses, singletons, and classes for operations on GHC TypeLits description:         Provides witnesses for 'KnownNat' and 'KnownSymbol'                      instances for various operations on GHC TypeLits - in@@ -38,7 +38,7 @@                        GHC.TypeLits.List   -- other-modules:          -- other-extensions:    -  build-depends:       base >=4.8 && <4.9+  build-depends:       base >=4.8 && <5                      , reflection                      , constraints   hs-source-dirs:      src