typelits-witnesses 0.2.0.0 → 0.2.1.0

raw patch · 4 files changed

+186/−111 lines, 4 filesdep +base-compatdep +transformersdep ~basedep ~reflectionPVP: major bump suggested

API removals or changes: PVP suggests a major version bump

Dependencies added: base-compat, transformers

Dependency ranges changed: base, reflection

API changes (from Hackage documentation)

Files

• CHANGELOG.md +51/−0
• src/GHC/TypeLits/List.hs +127/−106
• src/GHC/TypeLits/Witnesses.hs +1/−1
• typelits-witnesses.cabal +7/−4

@@ -0,0 +1,51 @@+0.2.1.0+=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.1.0>++*   Added "eliminators", a staple of dependently typed programming, for+    `NatList` and `SymbolList`.++0.2.0.0+=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.2.0.0>++*   **Breaking**: Changed the name of `someNatsVal'` to `someNatsValPos`, to+    break away from the "just add `'`" anti-pattern and to make the function+    name a bit more meaningful.++*   Added `reifyNats'`, a "safe" version of `reifyNats`.  Ideally,+    `reifyNats` should be the safe one, but its connection to `reifyNat` from+    the *reflection* package is very strong and worth preserving, I think.++0.1.2.0+=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.2.0>++*   Added `mapNatList'` and `mapSymbolList'` companions to `mapNatList` and+    `mapSymbolList`; they use `NatList` and `SymbolList` instead of Rank-2+    types, so they can work better with function composition with `(.)` and+    other things that Rank-2 types would have trouble with.++*   Added `sameNats` and `sameSymbols`, modeled after `sameNat` and+    `sameSymbol`.  They provide witnesses to GHC that `KnownNat`s passed in+    are both the same.++=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.1.0>++*   Added strict fields to `NatList`, `SomeNats`, `SymbolList`, and+    `SomeSymbols`.  It really doesn't make any sense for them to be lazy.++0.1.0.1+=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.1>++*   Added README to the cabal package as an extra source file, for viewing on+    Hackage.++0.1.0.0+=======+<https://github.com/mstksg/typelits-witnesses/releases/tag/v0.1.0.0>++*   Initial version.+

@@ -1,21 +1,23 @@-{-# LANGUAGE TypeOperators #-}-{-# LANGUAGE KindSignatures #-}-{-# LANGUAGE StandaloneDeriving #-}-{-# LANGUAGE TypeFamilies #-}-{-# LANGUAGE RankNTypes #-}+{-# LANGUAGE ConstraintKinds #-} {-# LANGUAGE DataKinds #-}+{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-}+{-# LANGUAGE KindSignatures #-}+{-# LANGUAGE LambdaCase #-}+{-# LANGUAGE NoImplicitPrelude #-}+{-# LANGUAGE PolyKinds #-}+{-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-}-{-# LANGUAGE ConstraintKinds #-}+{-# LANGUAGE StandaloneDeriving #-}+{-# LANGUAGE TypeFamilies #-}+{-# LANGUAGE TypeOperators #-} {-# LANGUAGE UndecidableInstances #-}-{-# LANGUAGE PolyKinds #-}-{-# LANGUAGE FlexibleContexts #-}  -- | -- Module      : GHC.TypeLits.List -- Description : Typeclasses, singletons, and reifiers for type-level lists --               of 'Nat's and 'Symbol's.--- Copyright   : (c) Justin Le 2015+-- Copyright   : (c) Justin Le 2016 -- License     : MIT -- Maintainer  : justin@jle.im -- Stability   : unstable@@ -41,6 +43,7 @@   , reifyNats   , reifyNats'   , sameNats+  , elimNatList   -- ** Traversals   , traverseNatList   , traverseNatList'@@ -55,6 +58,7 @@   , someSymbolsVal   , reifySymbols   , sameSymbols+  , elimSymbolList   -- ** Traversals   , traverseSymbolList   , traverseSymbolList'@@ -64,11 +68,12 @@   , mapSymbolList'   ) where +import Data.Functor.Identity import Data.Proxy-import Data.Type.Equality+import Prelude.Compat import Data.Reflection+import Data.Type.Equality import GHC.TypeLits-import Data.Functor.Identity  -- | @'KnownNats' ns@ is intended to represent that every 'Nat' in the -- type-level list 'ns' is itself a 'KnownNat' (meaning, you can use@@ -121,7 +126,7 @@ -- Gives the the ability to "change" the represented natural number to -- a new one, in a 'SomeNat'. ----- Can be considered a form of a @Traversal' 'SomeNat' 'SomeNats'@.+-- Can be considered a form of a @Traversal' 'SomeNats' 'SomeNat'@. traverseNatList     :: forall f ns. Applicative f     => (forall n. KnownNat n => Proxy n -> f SomeNat)@@ -130,27 +135,25 @@ traverseNatList f = go   where     go :: forall ms. NatList ms -> f SomeNats-    go nl = case nl of-              ØNL       -> pure $ SomeNats ØNL-              p :<# nl' -> merge <$> f p <*> go nl'+    go = \case+      ØNL      -> pure $ SomeNats ØNL+      n :<# ns -> merge <$> f n <*> go ns     merge :: SomeNat -> SomeNats -> SomeNats-    merge sn sns = case sn of-                     SomeNat i ->-                       case sns of-                         SomeNats is ->-                           SomeNats (i :<# is)+    merge = \case+      SomeNat n -> \case+        SomeNats ns ->+          SomeNats (n :<# ns) --- | Like 'traverseNatList', but literally actually a @Traversal' 'SomeNat'--- 'SomeNats'@, avoiding the Rank-2 types, so is usable with lens-library--- machinery.+-- | Like 'traverseNatList', but literally actually a @Traversal'+-- 'SomeNats' 'SomeNat'@, avoiding the Rank-2 types, so is usable with+-- lens-library machinery. traverseNatList'     :: forall f. Applicative f     => (SomeNat -> f SomeNat)     -> SomeNats     -> f SomeNats-traverseNatList' f ns =-    case ns of-      SomeNats ns' -> traverseNatList (f . SomeNat) ns'+traverseNatList' f = \case+    SomeNats ns -> traverseNatList (f . SomeNat) ns  -- | Utility function for traversing over all of the @'Proxy' n@s in -- a 'NatList', each with the corresponding 'KnownNat' instance available.@@ -163,10 +166,23 @@ traverseNatList_ f = go   where     go :: forall ms. NatList ms -> f ()-    go nl = case nl of-              ØNL       -> pure ()-              p :<# nl' -> f p *> go nl'+    go = \case+      ØNL       -> pure ()+      n :<# ns -> f n *> go ns +-- | The "eliminator" for 'NatList'.  You can think of this as+-- a dependently typed analogy for a fold.+elimNatList+    :: forall p ns. ()+    => p '[]+    -> (forall m ms. (KnownNat m, KnownNats ms) => Proxy m -> p ms -> p (m ': ms))+    -> NatList ns+    -> p ns+elimNatList z s = \case+    ØNL      -> z+    n :<# ns -> s n (elimNatList z s ns)++ -- | Utility function for \"mapping\" over each of the 'Nat's in the -- 'NatList'. mapNatList@@ -247,49 +263,46 @@     => 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+sameNats = \case+    ØNL      -> \case+      ØNL      -> Just Refl+      _ :<# _  -> Nothing+    n :<# ns -> \case+      Ø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+-- | @'KnownSymbols' ss@ is intended to represent that every 'Symbol' in the+-- type-level list 'ss' is itself a 'KnownSymbol' (meaning, you can use -- 'symbolVal' to get its corresponding 'String'). -- -- You can use 'symbolsVal' to get the corresponding @['String']@ from--- @'KnownSymbols' ns@.+-- @'KnownSymbols' ss@. -- -- For reasons discussed further in the documentation for 'KnownNats', this--- also lets you generate a @'SymbolList' ns@, in order to iterate over the+-- also lets you generate a @'SymbolList' ss@, in order to iterate over the -- type-level list of 'Symbol's and take advantage of their 'KnownSymbol' -- instances.-class KnownSymbols (ns :: [Symbol]) where-    symbolsVal  :: p ns -> [String]-    symbolsList :: SymbolList ns+class KnownSymbols (ss :: [Symbol]) where+    symbolsVal  :: p ss -> [String]+    symbolsList :: SymbolList ss  instance KnownSymbols '[] where     symbolsVal  _ = []     symbolsList    = ØSL -instance (KnownSymbol n, KnownSymbols ns) => KnownSymbols (n ': ns) where-    symbolsVal  _ = symbolVal (Proxy :: Proxy n) : symbolsVal (Proxy :: Proxy ns)+instance (KnownSymbol s, KnownSymbols ss) => KnownSymbols (s ': ss) where+    symbolsVal  _ = symbolVal (Proxy :: Proxy s) : symbolsVal (Proxy :: Proxy ss)     symbolsList   = Proxy :<$ symbolsList  -- | Represents unknown type-level lists of 'Symbol's. It's a 'SymbolList', -- but you don't know what the list contains at compile-time. data SomeSymbols :: * where-    SomeSymbols :: KnownSymbols ns => !(SymbolList ns) -> SomeSymbols+    SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols  -- | Singleton-esque type for "traversing" over type-level lists of -- 'Symbol's. Essentially contains a (value-level) list of @'Proxy' n@s,@@ -299,68 +312,66 @@ -- Typically generated using 'symbolsList'. data SymbolList :: [Symbol] -> * where     ØSL   :: SymbolList '[]-    (:<$) :: (KnownSymbol n, KnownSymbols ns)-          => !(Proxy n) -> !(SymbolList ns) -> SymbolList (n ': ns)+    (:<$) :: (KnownSymbol s, KnownSymbols ss)+          => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss)  infixr 5 :<$ deriving instance Show (SymbolList ns) --- | Utility function for traversing over all of the @'Proxy' n@s in+-- | Utility function for traversing over all of the @'Proxy' s@s in -- a 'SymbolList', each with the corresponding 'KnownSymbol' instance -- available.  Gives the the ability to "change" the represented natural -- number to a new one, in a 'SomeSymbol'. ----- Can be considered a form of a @Traversal' 'SomeSymbol' 'SomeSymbols'@.+-- Can be considered a form of a @Traversal' 'SomeSymbols' 'SomeSymbol'@. traverseSymbolList-    :: forall f ns. Applicative f-    => (forall n. KnownSymbol n => Proxy n -> f SomeSymbol)-    -> SymbolList ns+    :: forall f ss. Applicative f+    => (forall s. KnownSymbol s => Proxy s -> f SomeSymbol)+    -> SymbolList ss     -> f SomeSymbols traverseSymbolList f = go   where     go :: forall ms. SymbolList ms -> f SomeSymbols-    go nl = case nl of-              ØSL       -> pure $ SomeSymbols ØSL-              p :<$ nl' -> merge <$> f p <*> go nl'+    go = \case+      ØSL      -> pure $ SomeSymbols ØSL+      s :<$ ss -> merge <$> f s <*> go ss     merge :: SomeSymbol -> SomeSymbols -> SomeSymbols-    merge s sl = case s of-                   SomeSymbol ps ->-                     case sl of-                       SomeSymbols sl' ->-                         SomeSymbols (ps :<$ sl')+    merge = \case+      SomeSymbol s -> \case+        SomeSymbols ss ->+          SomeSymbols (s :<$ ss)  -- | Like 'traverseSymbolList', but literally actually a--- @Traversal' 'SomeSymbol' 'SomeSymbols'@, avoiding the Rank-2 types, so+-- @Traversal' 'SomeSymbols' 'SomeSymbol'@, 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'+traverseSymbolList' f = \case+    SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns' --- | Utility function for traversing over all of the @'Proxy' n@s in+-- | Utility function for traversing over all of the @'Proxy' s@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+    :: forall f ss. Applicative f+    => (forall s a. KnownSymbol s => Proxy s -> f a)+    -> SymbolList ss     -> f () traverseSymbolList_ f = go   where-    go :: forall ms. SymbolList ms -> f ()-    go nl = case nl of-              ØSL       -> pure ()-              p :<$ nl' -> f p *> go nl'+    go :: forall ts. SymbolList ts -> f ()+    go = \case+      ØSL      -> pure ()+      s :<$ ss -> f s *> go ss  -- | Utility function for \"mapping\" over each of the 'Symbol's in the -- 'SymbolList'. mapSymbolList-    :: (forall n. KnownSymbol n => Proxy n -> SomeSymbol)-    -> SymbolList ns+    :: (forall s. KnownSymbol s => Proxy s -> SomeSymbol)+    -> SymbolList ss     -> SomeSymbols mapSymbolList f = runIdentity . traverseSymbolList (Identity . f) @@ -373,30 +384,43 @@     -> SomeSymbols mapSymbolList' f = runIdentity . traverseSymbolList' (Identity . f) +-- | The "eliminator" for 'SymbolList'.  You can think of this as+-- a dependently typed analogy for a fold.+elimSymbolList+    :: forall p ss. ()+    => p '[]+    -> (forall t ts. (KnownSymbol t, KnownSymbols ts) => Proxy t -> p ts -> p (t ': ts))+    -> SymbolList ss+    -> p ss+elimSymbolList z s = \case+    ØSL      -> z+    n :<$ ns -> s n (elimSymbolList z s ns)++ -- | 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. someSymbolsVal :: [String] -> SomeSymbols someSymbolsVal []     = SomeSymbols ØSL-someSymbolsVal (n:ns) =-    case someSymbolVal n of-      SomeSymbol m ->-        case someSymbolsVal ns of-          SomeSymbols ms ->-            SomeSymbols (m :<$ ms)+someSymbolsVal (s:ss) =+    case someSymbolVal s of+      SomeSymbol t ->+        case someSymbolsVal ss of+          SomeSymbols ts ->+            SomeSymbols (t :<$ ts)  -- | List equivalent of 'reifyNat'.  Given a list of integers, takes--- a function in an "environment" with a @'NatList' ns@ corresponding to--- the given list, where every @n@ in @ns@ has a 'KnownNat' instance.+-- a function in an "environment" with a @'SymbolList' ss@ corresponding to+-- the given list, where every @s@ in @ss@ has a 'KnownSymbol' instance. -- -- Essentially a continuation-style version of 'SomeSymbols'. reifySymbols :: [String]-             -> (forall ns. KnownSymbols ns => SymbolList ns -> r)+             -> (forall ss. KnownSymbols ss => SymbolList ss -> r)              -> r reifySymbols []     f = f ØSL-reifySymbols (n:ns) f = reifySymbol n $ \m ->-                          reifySymbols ns $ \ms ->-                            f (m :<$ ms)+reifySymbols (s:ss) f = reifySymbol s $ \t ->+                          reifySymbols ss $ \ts ->+                            f (t :<$ ts)   -- | Get evidence that the two 'KnownSymbols' lists are actually the "same"@@ -415,17 +439,14 @@     => 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+sameSymbols = \case+    ØSL      -> \case+      ØSL      -> Just Refl+      _ :<$ _  -> Nothing+    s :<$ ss -> \case+      ØSL      -> Nothing+      t :<$ ts -> do+        Refl <- sameSymbol s t+        Refl <- sameSymbols ss ts+        return Refl 

@@ -9,7 +9,7 @@ -- Module      : GHC.TypeLits.Witnesses -- Description : Instance witnesses for various arithmetic operations on --               GHC TypeLits.--- Copyright   : (c) Justin Le 2015+-- Copyright   : (c) Justin Le 2016 -- License     : MIT -- Maintainer  : justin@jle.im -- Stability   : unstable

@@ -1,5 +1,5 @@ name:                typelits-witnesses-version:             0.2.0.0+version:             0.2.1.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@@ -23,10 +23,11 @@ license-file:        LICENSE author:              Justin Le maintainer:          justin@jle.im-copyright:           (c) Justin Le 2015+copyright:           (c) Justin Le 2016 category:            Data build-type:          Simple extra-source-files:  README.md+                   , CHANGELOG.md cabal-version:       >=1.10  source-repository head@@ -38,9 +39,11 @@                        GHC.TypeLits.List   -- other-modules:          -- other-extensions:    -  build-depends:       base >=4.8 && <5-                     , reflection+  build-depends:       base >=4.7 && <5+                     , base-compat                      , constraints+                     , reflection >= 2+                     , transformers   hs-source-dirs:      src   ghc-options:         -Wall   default-language:    Haskell2010