diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,3 +1,16 @@ +Version 0.3.0.0 +=============== + + + +* Added extra witnesses inside the constructors of `(:<=?)`. +* Allowed functions to polymorphically expect `p n` instead of `Proxy n` + whenever possible. +* Soft deprecation of *GHC.TypeLits.Witnesses*, in case people want to use + the functionality of *singletons* without the full library. +* Formal deprecation of *GHC.TypeLits.List*, with migration information, + because it's just so much more unweidly than using *singletons*. + Version 0.2.3.0 =============== diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -1,11 +1,10 @@ typelits-witnesses ================== -[![typelits-witnesses on Hackage](https://img.shields.io/hackage/v/lens.svg?maxAge=2592000)](https://hackage.haskell.org/package/typelits-witnesses) +[![typelits-witnesses on Hackage](https://img.shields.io/hackage/v/typelits-witnesses.svg?maxAge=2592000)](https://hackage.haskell.org/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) -[![Build -Status](https://travis-ci.org/mstksg/typelits-witnesses.svg?branch=master)](https://travis-ci.org/mstksg/typelits-witnesses) +[![Build Status](https://travis-ci.org/mstksg/typelits-witnesses.svg?branch=master)](https://travis-ci.org/mstksg/typelits-witnesses) Provides witnesses for `KnownNat` and `KnownSymbol` instances for various @@ -30,10 +29,73 @@ [singletons]: https://hackage.haskell.org/package/singletons +GHC.TypeLits.Compare +-------------------- -`GHC.TypeLits.Witnesses` ------------------------- +Provides tools for refining upper and lower bounds on `KnownNat`s and proving +inequalities involving *GHC.TypeLits*'s comparison API. (Both with `<=?` and +`CmpNat`). +If a library function requires `1 <= n` constraint, but only `KnownNat n` is +available: + +~~~haskell +foo :: (KnownNat n, 1 <= n) => Proxy n -> Int + +bar :: KnownNat n => Proxy n -> Int +bar n = case Proxy @1 %<=? n of + LE Refl -> foo n + NLE _ -> 0 +~~~ + +`foo` requires that `1 <= n`, but `bar` has to handle all cases of `n`. `%<=?` +lets you compare the `KnownNat`s in two `Proxy`s and returns a `:<=?`, which +has two constructors, `LE` and `NLE`. + +If you pattern match on the result, in the `LE` branch, the constraint +`1 <= n` will be satisfied according to GHC, so `bar` can safely call +`foo`, and GHC will recognize that `1 <= n`. + +In the `NLE` branch, the constraint that `1 > n` is satisfied, so any +functions that require that constraint would be callable. + +For convenience, `isLE` and `isNLE` are also offered: + +~~~haskell +bar :: KnownNat n => Proxy n -> Int +bar n = case Proxy @1 `isLE` n of + Just Refl -> foo n + Nothing -> 0 +~~~ + +Similarly, if a library function requires something involving `CmpNat`, +you can use `cmpNat` and the `SCmpNat` type: + +~~~haskell +foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int +foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int + +bar :: KnownNat n => Proxy n -> Int +bar n = case Proxy @5 `cmpNat` n of + CLT Refl -> foo1 n + CEQ _ -> 0 + CGT Refl -> foo2 n +~~~ + +You can use the `Refl` that `cmpNat` gives you with `flipCmpNat` and +`cmpNatLE` to "flip" the inequality or turn it into something compatible +with `<=?` (useful for when you have to work with libraries that mix the +two methods) or `cmpNatEq` and `eqCmpNat` to get to/from witnesses for +equality of the two `Nat`s. + + +GHC.TypeLits.Witnesses +---------------------- + +**SOFT DEPRECATED**: Use *[singletons][]* library instead! However, this +module is still here in case people want the functionality of *singletons* +without requiring the entire library. + Provides witnesses for instances arising from the arithmetic operations defined in `GHC.TypeLits`. @@ -59,7 +121,7 @@ ~~~haskell getDoubled :: KnownNat n => Proxy n -> Integer -getDoubled p = natVal (Proxy :: Proxy (n * 2)) +getDoubled p = natVal (Proxy @(n * 2)) ~~~ Which is supposed to call `natVal` with `n * 2`. However, this fails, because @@ -70,23 +132,23 @@ ~~~haskell getDoubled :: forall n. KnownNat n => Proxy n -> Integer -getDoubled p = withNatOp (%*) p (Proxy :: Proxy 2) $ - natVal (Proxy :: Proxy (n * 2)) +getDoubled p = withNatOp (%*) p (Proxy @2) $ + natVal (Proxy @(n * 2)) ~~~ Within the scope of the argument of -`withNatOp (%*) (Proxy :: Proxy n) (Proxy :: Proxy m)`, `n * m` is an instance +`withNatOp (%*) (Proxy @n) (Proxy @m)`, `n * m` is an instance of `KnownNat`, so you can use `natVal` on it, and get the expected result: ~~~haskell -> getDoubled (Proxy :: Proxy 12) +> getDoubled (Proxy @12) 24 ~~~ There are four "nat operations" defined here, corresponding to the four type-level operations on `Nat` provided in `GHC.TypeLits`: `(%+)`, `(%-)`, -`(%*)`, and `(%^)`, corresponding to addition, subtraction, multiplication, -and exponentiation, respectively. +`(%*)`, and `(%^)`, corresponding to addition, subtraction, multiplication, and +exponentiation, respectively. Note that `(%-)` is implemented in a way that allows for the result to be a *negative* `Nat`. @@ -94,68 +156,35 @@ There are more advanced operations dealing with low-level machinery, as well, in the module. See module documentation for more detail. -`GHC.TypeLits.Compare` ----------------------- - -Provides tools for refining upper and lower bounds on `KnownNat`s and proving -inequalities involving *GHC.TypeLits*'s comparison API. (Both with `<=?` and -`CmpNat`). +### Singletons replacement -If a library function requires `1 <= n` constraint, but only `KnownNat n` is -available: +This module is deprecated, and it is recommended you use the functionality from +the *[singletons][]* package instead. A direct translation using `Proxy` would +be: ~~~haskell -foo :: (KnownNat n, 1 <= n) => Proxy n -> Int - -bar :: KnownNat n => Proxy n -> Int -bar n = case (Proxy :: Proxy 1) %<=? n of - LE Refl -> foo n - NLE _ -> 0 +getDoubled :: forall n. KnownNat n => Proxy n -> Integer +getDoubled p = withKnownNat (SNat @n %:* SNat @2) $ + natVal (Proxy @(n * 2)) ~~~ -`foo` requires that `1 <= n`, but `bar` has to handle all cases of `n`. `%<=?` -lets you compare the `KnownNat`s in two `Proxy`s and returns a `:<=?`, which -has two constructors, `LE` and `NLE`. - -If you pattern match on the result, in the `LE` branch, the constraint -`1 <= n` will be satisfied according to GHC, so `bar` can safely call -`foo`, and GHC will recognize that `1 <= n`. - -In the `NLE` branch, the constraint that `1 > n` is satisfied, so any -functions that require that constraint would be callable. - -For convenience, `isLE` and `isNLE` are also offered: +But one using singletons throughout the whole process would be: ~~~haskell -bar :: KnownNat n => Proxy n -> Int -bar n = case isLE (Proxy :: Proxy 1) n of - Just Refl -> foo n - Nothing -> 0 +getDoubled :: forall n. KnownNat n => Sing n -> Integer +getDoubled s = withKnownNat (s %:* SNat @2) $ + natVal (Proxy @(n * 2)) ~~~ -Similarly, if a library function requires something involving `CmpNat`, -you can use `cmpNat` and the `SCmpNat` type: -~~~haskell -foo1 :: (KnownNat n, CmpNat 5 n ~ LT) => Proxy n -> Int -foo2 :: (KnownNat n, CmpNat 5 n ~ GT) => Proxy n -> Int - -bar :: KnownNat n => Proxy n -> Int -bar n = case cmpNat (Proxy :: Proxy 5) n of - CLT Refl -> foo1 n - CEQ Refl -> 0 - CGT Refl -> foo2 n -~~~ - -You can use the `Refl` that `cmpNat` gives you with `flipCmpNat` and -`cmpNatLE` to "flip" the inequality or turn it into something compatible -with `<=?` (useful for when you have to work with libraries that mix the -two methods) or `cmpNatEq` and `eqCmpNat` to get to/from witnesses for -equality of the two `Nat`s. - -`GHC.TypeLits.List` +GHC.TypeLits.List ------------------- +**HARD DEPRECATED: Use *[singletons][]* library instead! This module is +extremely unweildy, and using *singletons* is much, much smoother on many +levels, and integrates everything together in a nice way. This module will +likely be removed in a future version. + Provides analogies of `KnownNat`, `SomeNat`, `natVal`, etc., to type-level lists of `KnownNat` instances, and also singletons for iterating over type-level lists of `Nat`s and `Symbol`s. @@ -164,7 +193,7 @@ `natsVal`, which is like `natVal` but for type-level lists of `KnownNats`: ~~~haskell -> natsVal (Proxy :: Proxy [1,2,3]) +> natsVal (Proxy @[1,2,3]) [1,2,3] ~~~ @@ -184,7 +213,7 @@ ~~~ ~~~haskell -> printNats (natsList :: NatList [1,2,3]) +> printNats (natsList :: @[1,2,3]) 1 2 3 @@ -222,4 +251,21 @@ The above would match on the `Just Refl` branch. See module documentation for more details and variations. + +### Singletons replacement + +This module is deprecated, and it is recommended you use the functionality from +the *[singletons][]* package instead. `natsVal` is `fromSing`, `reifyNats` is +`toSing`/`withSomeSing`, `sameNats` is simply `%~`, and you can traverse/reify +singletons of lists too: + +~~~haskell +printNats :: forall (ns :: [Nat]). Sing ns -> IO () +printNats ss = case ss of + SNil -> + return () + s `SCons` ss' -> do + print $ fromSing s + printNats ss' +~~~ diff --git a/src/GHC/TypeLits/Compare.hs b/src/GHC/TypeLits/Compare.hs --- a/src/GHC/TypeLits/Compare.hs +++ b/src/GHC/TypeLits/Compare.hs @@ -87,65 +87,65 @@ , flipCmpNat , cmpNatEq , eqCmpNat + , reflCmpNat -- ** Interfacing with '<=?' , cmpNatLE ) where import Data.Type.Equality -import Data.Proxy import GHC.TypeLits import Unsafe.Coerce isLE :: (KnownNat m, KnownNat n) - => Proxy m - -> Proxy n + => p m + -> p n -> Maybe ((m <=? n) :~: 'True) isLE m n = case m %<=? n of LE Refl -> Just Refl - NLE _ -> Nothing + NLE _ _ -> Nothing isNLE :: (KnownNat m, KnownNat n) - => Proxy m - -> Proxy n + => p m + -> p n -> Maybe ((m <=? n) :~: 'False) isNLE m n = case m %<=? n of - NLE Refl -> Just Refl - LE _ -> Nothing + NLE Refl Refl -> Just Refl + LE _ -> Nothing data (:<=?) :: Nat -> Nat -> * where LE :: ((m <=? n) :~: 'True) -> (m :<=? n) - NLE :: ((m <=? n) :~: 'False) -> (m :<=? n) + NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> (m :<=? n) (%<=?) :: (KnownNat m, KnownNat n) - => Proxy m - -> Proxy n + => p m + -> p n -> (m :<=? n) m %<=? n | natVal m <= natVal n = LE (unsafeCoerce Refl) - | otherwise = NLE (unsafeCoerce Refl) + | otherwise = NLE (unsafeCoerce Refl) (unsafeCoerce Refl) data SCmpNat :: Nat -> Nat -> * where CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n - CEQ :: (CmpNat m n :~: 'EQ) -> SCmpNat m n + CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n cmpNat :: (KnownNat m, KnownNat n) - => Proxy m - -> Proxy n + => p m + -> p n -> SCmpNat m n cmpNat m n = case compare (natVal m) (natVal n) of LT -> CLT (unsafeCoerce Refl) - EQ -> CEQ (unsafeCoerce Refl) + EQ -> CEQ (unsafeCoerce Refl) (unsafeCoerce Refl) GT -> CGT (unsafeCoerce Refl) flipCmpNat :: SCmpNat m n -> SCmpNat n m -flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl) - CEQ Refl -> CEQ (unsafeCoerce Refl) - CGT Refl -> CLT (unsafeCoerce Refl) +flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl) + CEQ Refl Refl -> CEQ (unsafeCoerce Refl) Refl + CGT Refl -> CLT (unsafeCoerce Refl) cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n) cmpNatEq = \case Refl -> unsafeCoerce Refl @@ -153,7 +153,10 @@ eqCmpNat :: (m :~: n) -> (CmpNat m n :~: 'EQ) eqCmpNat = \case Refl -> unsafeCoerce Refl +reflCmpNat :: (m :~: n) -> SCmpNat m n +reflCmpNat r = CEQ (eqCmpNat r) r + cmpNatLE :: SCmpNat m n -> (m :<=? n) -cmpNatLE = \case CLT Refl -> LE (unsafeCoerce Refl) - CEQ Refl -> LE (unsafeCoerce Refl) - CGT Refl -> NLE (unsafeCoerce Refl) +cmpNatLE = \case CLT Refl -> LE (unsafeCoerce Refl) + CEQ Refl Refl -> LE (unsafeCoerce Refl) + CGT Refl -> NLE (unsafeCoerce Refl) (unsafeCoerce Refl) diff --git a/src/GHC/TypeLits/List.hs b/src/GHC/TypeLits/List.hs --- a/src/GHC/TypeLits/List.hs +++ b/src/GHC/TypeLits/List.hs @@ -33,7 +33,8 @@ -- -- See typeclass documentations and README for more information. -module GHC.TypeLits.List ( +module GHC.TypeLits.List + {-# DEPRECATED "Use singletons package instead" #-} ( -- * 'KnownNats' KnownNats(..) , SomeNats(..) @@ -75,6 +76,7 @@ import Data.Type.Equality import GHC.TypeLits + -- | @'KnownNats' ns@ is intended to represent that every 'Nat' in the -- type-level list 'ns' is itself a 'KnownNat' (meaning, you can use -- 'natVal' to get its corresponding 'Integer'). @@ -92,6 +94,9 @@ class KnownNats (ns :: [Nat]) where natsVal :: p ns -> [Integer] natsList :: NatList ns +{-# DEPRECATED KnownNats "Use SingI from the singletons package instead" #-} +{-# DEPRECATED natsVal "Use fromSing from the singletons package instead" #-} +{-# DEPRECATED natsList "Use sing from the singletons package instead" #-} instance KnownNats '[] where natsVal _ = [] @@ -106,6 +111,7 @@ -- compile-time. data SomeNats :: * where SomeNats :: KnownNats ns => !(NatList ns) -> SomeNats +{-# DEPRECATED SomeNats "Use SomeSing from the singletons package instead" #-} -- | Singleton-esque type for "traversing" over type-level lists of 'Nat's. -- Essentially contains a (value-level) list of @'Proxy' n@s, but each 'n' @@ -117,6 +123,7 @@ ØNL :: NatList '[] (:<#) :: (KnownNat n, KnownNats ns) => !(Proxy n) -> !(NatList ns) -> NatList (n ': ns) +{-# DEPRECATED NatList "Use Sing from the singletons package instead" #-} infixr 5 :<# deriving instance Show (NatList ns) @@ -211,6 +218,7 @@ SomeNat m <- someNatVal n SomeNats ms <- someNatsVal ns return $ SomeNats (m :<# ms) +{-# DEPRECATED someNatsVal "Use toSing from the singletons package instead" #-} -- | List equivalent of 'reifyNat'. Given a list of integers, takes -- a function in an "environment" with a @'NatList' ns@ corresponding to @@ -228,6 +236,7 @@ reifyNats (n:ns) f = reifyNat n $ \m -> reifyNats ns $ \ms -> f (m :<# ms) +{-# DEPRECATED reifyNats "Use withSomeSing from the singletons package instead" #-} -- | "Safe" version of 'reifyNats', which will only run the continuation if -- every 'Integer' in the list is non-negative. If not, then returns @@ -241,13 +250,14 @@ case someNatsVal ns of Just (SomeNats ms) -> f ms Nothing -> d - +{-# DEPRECATED reifyNats' "Use withSomeSing from the singletons package instead" #-} -- | Like 'someNatsVal', but will also go ahead and produce 'KnownNat's -- whose integer values are negative. It won't ever error on producing -- them, but extra care must be taken when using the produced 'SomeNat's. someNatsValPos :: [Integer] -> SomeNats someNatsValPos ns = reifyNats ns SomeNats +{-# DEPRECATED someNatsValPos "Use toSing from the singletons package instead" #-} -- | Get evidence that the two 'KnownNats' lists are actually the "same" -- list of 'Nat's (that they were instantiated with the same numbers). @@ -274,7 +284,7 @@ Refl <- sameNat n m Refl <- sameNats ns ms return Refl - +{-# DEPRECATED sameNats "Use (%~) from the singletons package instead" #-} -- | @'KnownSymbols' ss@ is intended to represent that every 'Symbol' in the @@ -291,6 +301,9 @@ class KnownSymbols (ss :: [Symbol]) where symbolsVal :: p ss -> [String] symbolsList :: SymbolList ss +{-# DEPRECATED KnownSymbols "Use SingI from the singletons package instead" #-} +{-# DEPRECATED symbolsVal "Use fromSing from the singletons package instead" #-} +{-# DEPRECATED symbolsList "Use sing from the singletons package instead" #-} instance KnownSymbols '[] where symbolsVal _ = [] @@ -304,6 +317,7 @@ -- but you don't know what the list contains at compile-time. data SomeSymbols :: * where SomeSymbols :: KnownSymbols ss => !(SymbolList ss) -> SomeSymbols +{-# DEPRECATED SomeSymbols "Use SomeSing from the singletons package instead" #-} -- | Singleton-esque type for "traversing" over type-level lists of -- 'Symbol's. Essentially contains a (value-level) list of @'Proxy' n@s, @@ -315,6 +329,7 @@ ØSL :: SymbolList '[] (:<$) :: (KnownSymbol s, KnownSymbols ss) => !(Proxy s) -> !(SymbolList ss) -> SymbolList (s ': ss) +{-# DEPRECATED SymbolList "Use Sing from the singletons package instead" #-} infixr 5 :<$ deriving instance Show (SymbolList ns) @@ -411,6 +426,7 @@ case someSymbolsVal ss of SomeSymbols ts -> SomeSymbols (t :<$ ts) +{-# DEPRECATED someSymbolsVal "Use toSing from the singletons package instead" #-} -- | List equivalent of 'reifyNat'. Given a list of integers, takes -- a function in an "environment" with a @'SymbolList' ss@ corresponding to @@ -424,6 +440,7 @@ reifySymbols (s:ss) f = reifySymbol s $ \t -> reifySymbols ss $ \ts -> f (t :<$ ts) +{-# DEPRECATED reifySymbols "Use withSomeSing from the singletons package instead" #-} -- | Get evidence that the two 'KnownSymbols' lists are actually the "same" @@ -451,4 +468,5 @@ Refl <- sameSymbol s t Refl <- sameSymbols ss ts return Refl +{-# DEPRECATED sameSymbols "Use (%~) from the singletons package instead" #-} diff --git a/src/GHC/TypeLits/Witnesses.hs b/src/GHC/TypeLits/Witnesses.hs --- a/src/GHC/TypeLits/Witnesses.hs +++ b/src/GHC/TypeLits/Witnesses.hs @@ -15,6 +15,7 @@ -- Stability : unstable -- Portability : non-portable -- +-- __Deprecated: Use the /singletons/ package instead__ -- -- This module provides witnesses for instances that result from the -- various arithmetic operations on GHC TypeLits 'Nat' types. In general, @@ -67,9 +68,13 @@ -- production of witnesses and entailments will hold, but be aware that any -- functions that rely on 'KnownNat' instances to be non-negative can -- potentially break. +-- +-- module GHC.TypeLits.Witnesses ( + -- * Singletons + -- $singletons -- * High level wrapper withNatOp -- * Direct witnesses @@ -93,12 +98,61 @@ import Data.Reflection import Unsafe.Coerce +-- $singletons +-- +-- All of the functionality in this module can be subsumed by the +-- /singletons/ package, by utilizing: +-- +-- * "Data.Singletons" +-- * "Data.Singletons.TypeLits" +-- * "Data.Singletons.Prelude.Num" +-- +-- This module is left in this package as an alternative for those who +-- might, for some reason, not want to add a /singletons/ dependency to +-- their project. However, if you do much at the type level, using the +-- /singletons/ library is much preferred, as it provides a unifed +-- interface for all of the functionality here, generalized to other kinds +-- besides 'Nat'. +-- +-- For all functions in this module, a /singletons/ equivalent is included +-- for help migrating. +-- +-- In general: +-- +-- +-- * The /singletons/ type @'Sing' n@ (or its equivalent, @'SNat' n@) +-- subsumes both @'Proxy' n@ and @'Dict' ('KnownNat' n)@. You can +-- replace both @'Proxy' n@ and @'Dict' ('KnownNat' n)@ with @'SNat' n@ +-- to move to singletons style. +-- +-- * 'dictNatVal' and 'natVal' are both just 'fromSing'. +-- +-- * Replace '%+', '%-', and '%*' with their /singletons/ +-- equivalents, '%:+', '%:-', and '%:*' from +-- "Data.Singletons.Prelude.Num". Note that the current version of +-- /singletons/ does not have an equivalent for '%^'. +-- +-- * Use 'withKnownNat' from /singletons/ (or just pattern match on +-- 'SNat') to get a 'KnownNat' instance from a @'SNat' n@, the same way +-- you'd get one from a 'Dict'. +-- +-- * The high-level combinator 'withNatOp' can simply be replaced with +-- applying your singleton functions ('%+' etc.) to 'SNat' values, and +-- pattern matching on the result, or using 'withKnownNat' on the result. +-- + -- | Create a 'Dict' witness for @'KnownNat' n@. -natDict :: KnownNat n => Proxy n -> Dict (KnownNat n) +-- +-- Not necessary with /singletons/, as @'SNat' n@ stands in for both +-- @'Proxy' n@ and @'Dict' ('KnownNat' n)@. +natDict :: KnownNat n => p n -> Dict (KnownNat n) natDict _ = Dict -- | Get the 'Integer' from the 'KnownNat' instance witnessed by the -- 'Dict'. +-- +-- With /singletons/, this is 'fromSing', which takes an @'SNat' n@ and +-- returns an 'Integer'. dictNatVal :: forall n. Dict (KnownNat n) -> Integer dictNatVal Dict = natVal (Proxy :: Proxy n) @@ -112,6 +166,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators. +-- +-- With /singletons/, this is '%:+' from "Data.Singletons.Prelude.Num". (%+) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n + m)) Dict %+ Dict = mapDict entailAdd (Dict :: Dict (KnownNat n, KnownNat m)) @@ -123,6 +179,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators. +-- +-- With /singletons/, this is '%:-' from "Data.Singletons.Prelude.Num". (%-) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n - m)) Dict %- Dict = mapDict entailSub (Dict :: Dict (KnownNat n, KnownNat m)) @@ -131,6 +189,8 @@ -- -- Follows proper association and fixity for usage with other similar -- operators. +-- +-- With /singletons/, this is '%:*' from "Data.Singletons.Prelude.Num". (%*) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n * m)) Dict %* Dict = mapDict entailMul (Dict :: Dict (KnownNat n, KnownNat m)) @@ -188,12 +248,29 @@ -- (Note that associativity and fixity for the witness-generating operators -- are set to match that of normal addition and multiplication, etc.) -- +-- With /singletons/, @'withNatOp' f x y@ is @'withKnownNat' (f x y)@. -- +-- So, instead of +-- +-- @ +-- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $ +-- 'natVal' ('Proxy' :: 'Proxy' (n + 1)) +-- @ +-- +-- You can just use +-- +-- @ +-- 'withKnownNat' ('SNat' @n) ('SNat @1) $ +-- 'natVal' ('Proxy' :: 'Proxy' (n + 1)) +-- @ +-- +-- 'natVal' can of course be replaced with 'fromSing'. +-- withNatOp :: (KnownNat n, KnownNat m) => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) - -> Proxy n - -> Proxy m + -> p n + -> p m -> (KnownNat q => r) -> r withNatOp op x y r = case natDict x `op` natDict y of diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal --- a/typelits-witnesses.cabal +++ b/typelits-witnesses.cabal @@ -1,5 +1,5 @@ name: typelits-witnesses -version: 0.2.3.0 +version: 0.3.0.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 @@ -34,12 +34,16 @@ license-file: LICENSE author: Justin Le maintainer: justin@jle.im -copyright: (c) Justin Le 2016 +copyright: (c) Justin Le 2018 category: Data build-type: Simple extra-source-files: README.md , CHANGELOG.md cabal-version: >=1.10 +tested-with: GHC == 7.8.4 + , GHC == 7.10.3 + , GHC == 8.0.2 + , GHC == 8.2.1 source-repository head type: git @@ -51,11 +55,18 @@ GHC.TypeLits.Compare -- other-modules: -- other-extensions: - build-depends: base >=4.7 && <5 - , base-compat - , constraints - , reflection >= 2 - , transformers + if impl(ghc >= 8.0) + build-depends: base >=4.7 && <5 + , base-compat + , constraints + , reflection >= 2 + , transformers + else + build-depends: base >=4.7 && <5 + , base-compat + , constraints < 0.9.1 + , reflection >= 2 + , transformers hs-source-dirs: src ghc-options: -Wall default-language: Haskell2010