diff --git a/CHANGELOG.md b/CHANGELOG.md --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -1,5 +1,25 @@ +Changelog +========= + +Version 0.4.0.0 +--------------- + + + +*June 20, 2019* + +* Complete overhaul of *GHC.TypeLits.Witnesses* to more or less match the + interface of singletons. This changes the role of the module to be a + "lightweight" version of the singletons library as it pertains to `Nat` and + `Symbol`. +* Removal of the *GHC.TypeLits.List* module. We could perform the same + overhaul as *GHC.TypeLits.Witnesses*, but it is complex enough that it + would be better to just use *singletons* instead at that point. +* Remove all external dependencies, except for *base* and *dependent-sum*. +* Break compatibility with GHC < 8.2 + Version 0.3.0.3 -=============== +--------------- @@ -9,7 +29,7 @@ * Break compatibility with GHC < 8.0 Version 0.3.0.2 -=============== +--------------- @@ -19,7 +39,7 @@ take different "proxy" types (`p` and `q`). Version 0.3.0.1 -=============== +--------------- @@ -27,7 +47,7 @@ haddocks for *GHC.TypeLits.List*. Version 0.3.0.0 -=============== +--------------- @@ -40,7 +60,7 @@ because it's just so much more unweidly than using *singletons*. Version 0.2.3.0 -=============== +--------------- @@ -48,7 +68,7 @@ inequalities on `KnownNat`s and associated utility functions. Version 0.2.2.0 -=============== +--------------- @@ -56,7 +76,7 @@ and `sameSymbols`. Version 0.2.1.0 -=============== +--------------- @@ -64,7 +84,7 @@ `NatList` and `SymbolList`. Version 0.2.0.0 -=============== +--------------- @@ -77,7 +97,7 @@ the *reflection* package is very strong and worth preserving, I think. Version 0.1.2.0 -=============== +--------------- @@ -91,7 +111,7 @@ are both the same. Version 0.1.1.0 -=============== +--------------- @@ -99,7 +119,7 @@ `SomeSymbols`. It really doesn't make any sense for them to be lazy. Version 0.1.0.1 -=============== +--------------- @@ -107,7 +127,7 @@ Hackage. Version 0.1.0.0 -=============== +--------------- diff --git a/README.md b/README.md --- a/README.md +++ b/README.md @@ -6,266 +6,17 @@ [![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) - -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 -`KnownSymbol` instances. - -This is useful for situations where you have `KnownNat n`, and you want to -prove to GHC `KnownNat (n + 3)`, or `KnownNat (2*n + 4)`. - -It's also useful for when you want to work with type level lists of -`KnownNat`/`KnownSymbol` instances and singletons for traversing them, and be -able to apply analogies of `natVal`/`symbolVal` to lists with analogies for -`SomeNat` and `SomeSymbol`. +This library contains: -Note that most of the functionality in this library can be reproduced in a more -generic way using the great [singletons][] library. The versions here are -provided as a "plumbing included" alternative that makes some commonly found -design patterns involving GHC's TypeLits functionality a little smoother, -especially when working with external libraries or GHC TypeLit's `Nat` -comparison API. +* A small specialized subset of the *[singletons][]* library as it pertains to + `Nat` and `Symbol`, for when you need some simple functionality without + wanting to invoke the entire *singletons* library. +* Operations for manipulating these singletons and `KnownNat` and + `KnownSymbol` instances, such as addition and multiplication of + singletons/`KnownNat` instances. +* Operations for the comparison of `Nat`s in a way that works well with + *GHC.TypeLits*'s different comparison systems. This is helpful for + bridging together libraries that use different systems; this functionality + is not yet provided by *singletons*. [singletons]: https://hackage.haskell.org/package/singletons - -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`). - -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`. - -In general, if you have `KnownNat n`, GHC can't infer `KnownNat (n + 1)`; -and if you have `KnownNat m`, as well, GHC can't infer `KnownNat (n + m)`. - -This can be extremely annoying when dealing with libraries and applications -where one regularly adds and subtracts type-level nats and expects `KnownNat` -instances to follow. For example, vector concatenation of length-encoded -vector types can be: - -~~~haskell -concat :: (KnownNat n, KnownNat m) - => Vector n a - -> Vector m a - -> Vector (n + m) a -~~~ - -But, `n + m` now does not have a `KnownNat` instance, which severely hinders -what you can do with this! - -Consider this concrete (but silly) example: - -~~~haskell -getDoubled :: KnownNat n => Proxy n -> Integer -getDoubled p = natVal (Proxy @(n * 2)) -~~~ - -Which is supposed to call `natVal` with `n * 2`. However, this fails, because -while `n` is a `KnownNat`, `n * 2` is not necessarily so. This module lets -you re-assure GHC that this is okay. - -The most straightforward/high-level usage is with `withNatOp`: - -~~~haskell -getDoubled :: forall n. KnownNat n => Proxy n -> Integer -getDoubled p = withNatOp (%*) p (Proxy @2) $ - natVal (Proxy @(n * 2)) -~~~ - -Within the scope of the argument of -`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 @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. - -Note that `(%-)` is implemented in a way that allows for the result to be a -*negative* `Nat`. - -There are more advanced operations dealing with low-level machinery, as well, -in the module. See module documentation for more detail. - -### Singletons replacement - -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 -getDoubled :: forall n. KnownNat n => Proxy n -> Integer -getDoubled p = withKnownNat (SNat @n %:* SNat @2) $ - natVal (Proxy @(n * 2)) -~~~ - -But one using singletons throughout the whole process would be: - -~~~haskell -getDoubled :: forall n. KnownNat n => Sing n -> Integer -getDoubled s = withKnownNat (s %:* SNat @2) $ - natVal (Proxy @(n * 2)) -~~~ - - -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. - -If you had `KnownNats ns`, then you have two things you can do with it; first, -`natsVal`, which is like `natVal` but for type-level lists of `KnownNats`: - -~~~haskell -> natsVal (Proxy @[1,2,3]) -[1,2,3] -~~~ - -And more importantly, `natsList`, which provides singletons that you can -pattern match on to "reify" the structure of the list, getting a `Proxy n` for -every item in the list with a `KnownNat`/`KnownSymbol` instance in scope for -you to use: - -~~~haskell -printNats :: NatList ns -> IO () -printNats nl = case nl of - ØNL -> - return () - p :># nl' -> do - print $ natVal p - printNats nl' -~~~ - -~~~haskell -> printNats (natsList :: @[1,2,3]) -1 -2 -3 -~~~ - -Without this, there is no way to "iterate over" and "access" every `Nat` in a -list of `KnownNat`s. You can't "iterate" over `[1,2,3]` in `Proxy [1,2,3]`, -but you can iterate over them in `NatList [1,2,3]`. - -This module also lets you "reify" lists of `Integer`s or `String`s into -`NatList`s and `SymbolList`s, so you can access them at the type level for -some dependent types fun. - -~~~haskell -> reifyNats [1,2,3] $ \nl -> do - print nl - printNats nl -Proxy :<# Proxy :<# Proxy :<# ØNL -1 -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. - -### 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 @@ -9,8 +9,6 @@ -- | -- Module : GHC.TypeLits.Compare --- Description : Tools and singletons for proving and refining inequalities --- and bounds on GHC TypeLits types using '<=' and '<=?' -- Copyright : (c) Justin Le 2016 -- License : MIT -- Maintainer : justin@jle.im @@ -26,7 +24,7 @@ -- @'KnownNat' n@ is available: -- -- @ --- foo :: (KnownNat n, 1 '<=' n) => 'Proxy' n -> Int +-- foo :: (KnownNat n, 1 '<=' n) => 'Data.Proxy.Proxy' n -> Int -- -- bar :: KnownNat n => Proxy n -> Int -- bar n = case (Proxy :: Proxy 1) '%<=?' n of @@ -35,7 +33,7 @@ -- @ -- -- @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 +-- @%<=?@ lets you compare the 'KnownNat's in two 'Data.Proxy.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 @@ -73,7 +71,9 @@ -- 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. - +-- +-- This module is useful for helping bridge between libraries that use +-- different 'Nat'-based comparison systems in their type constraints. module GHC.TypeLits.Compare ( -- * '<=' and '<=?' (:<=?)(..) @@ -89,8 +89,8 @@ , cmpNatEq , eqCmpNat , reflCmpNat - -- ** Interfacing with '<=?' , cmpNatLE + , cmpNatGOrdering ) where @@ -98,7 +98,11 @@ import Data.Type.Equality import GHC.TypeLits import Unsafe.Coerce +import Data.GADT.Compare +-- | Simplified version of '%<=?': check if @m@ is less than or equal to to +-- @n@. If it is, match on @'Just' 'Refl'@ to get GHC to believe it, +-- within the body of the pattern match. isLE :: (KnownNat m, KnownNat n) => p m @@ -108,6 +112,9 @@ LE Refl -> Just Refl NLE _ _ -> Nothing +-- | Simplified version of '%<=?': check if @m@ is not less than or equal +-- to to @n@. If it is, match on @'Just' 'Refl'@ to get GHC to believe it, +-- within the body of the pattern match. isNLE :: (KnownNat m, KnownNat n) => p m @@ -117,10 +124,13 @@ NLE Refl Refl -> Just Refl LE _ -> Nothing +-- | Two possible ordered relationships between two natural numbers. data (:<=?) :: Nat -> Nat -> Type where LE :: ((m <=? n) :~: 'True) -> (m :<=? n) NLE :: ((m <=? n) :~: 'False) -> ((n <=? m) :~: 'True) -> (m :<=? n) +-- | Compare @m@ and @n@, classifying their relationship into some +-- constructor of ':<=?'. (%<=?) :: (KnownNat m, KnownNat n) => p m @@ -129,11 +139,14 @@ m %<=? n | natVal m <= natVal n = LE (unsafeCoerce Refl) | otherwise = NLE (unsafeCoerce Refl) (unsafeCoerce Refl) +-- | Three possible ordered relationships between two natural numbers. data SCmpNat :: Nat -> Nat -> Type where CLT :: (CmpNat m n :~: 'LT) -> SCmpNat m n CEQ :: (CmpNat m n :~: 'EQ) -> (m :~: n) -> SCmpNat m n CGT :: (CmpNat m n :~: 'GT) -> SCmpNat m n +-- | Compare @m@ and @n@, classifying their relationship into some +-- constructor of 'SCmpNat'. cmpNat :: (KnownNat m, KnownNat n) => p m @@ -144,21 +157,36 @@ EQ -> CEQ (unsafeCoerce Refl) (unsafeCoerce Refl) GT -> CGT (unsafeCoerce Refl) +-- | Flip an inequality. flipCmpNat :: SCmpNat m n -> SCmpNat n m flipCmpNat = \case CLT Refl -> CGT (unsafeCoerce Refl) CEQ Refl Refl -> CEQ (unsafeCoerce Refl) Refl CGT Refl -> CLT (unsafeCoerce Refl) +-- | @'CmpNat' m n@ being 'EQ' implies that @m@ is equal to @n@. cmpNatEq :: (CmpNat m n :~: 'EQ) -> (m :~: n) cmpNatEq = \case Refl -> unsafeCoerce Refl +-- | A witness of equality implies that @'CmpNat' m n@ is 'Eq'. eqCmpNat :: (m :~: n) -> (CmpNat m n :~: 'EQ) eqCmpNat = \case Refl -> unsafeCoerce Refl +-- | Inject a witness of equality into an 'SCmpNat' at 'CEQ'. reflCmpNat :: (m :~: n) -> SCmpNat m n reflCmpNat r = CEQ (eqCmpNat r) r +-- | Convert to ':<=?' cmpNatLE :: SCmpNat m n -> (m :<=? n) cmpNatLE = \case CLT Refl -> LE (unsafeCoerce Refl) CEQ Refl Refl -> LE (unsafeCoerce Refl) CGT Refl -> NLE (unsafeCoerce Refl) (unsafeCoerce Refl) + +-- | Convert to 'GOrdering' +-- +-- @since 0.4.0.0 +cmpNatGOrdering :: SCmpNat n m -> GOrdering n m +cmpNatGOrdering = \case + CLT Refl -> GLT + CEQ Refl Refl -> GEQ + CGT Refl -> GGT + diff --git a/src/GHC/TypeLits/List.hs b/src/GHC/TypeLits/List.hs deleted file mode 100644 --- a/src/GHC/TypeLits/List.hs +++ /dev/null @@ -1,503 +0,0 @@ -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE KindSignatures #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE TypeInType #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE UndecidableInstances #-} - --- | --- Module : GHC.TypeLits.List --- Description : Typeclasses, singletons, and reifiers for type-level lists --- of 'Nat's and 'Symbol's. --- Copyright : (c) Justin Le 2016 --- License : MIT --- Maintainer : justin@jle.im --- Stability : unstable --- Portability : non-portable --- --- --- Provides the 'KnownNats' and 'KnownSymbols' typeclasses in analogy to --- 'KnownNat' and 'KnownSymbol' from "GHC.TypeLits". Also provides --- singleton-esque structures for traversing over type-level lists of --- 'Nat's and 'Symbol's. Comes with continuation-style reifiers and --- existential types for dependent typing usage, and as an analogy with --- 'SomeNat' and 'SomeSymbol'. --- --- See typeclass documentations and README for more information. - -module GHC.TypeLits.List - {-# DEPRECATED "Use singletons package instead" #-} ( - -- * 'KnownNats' - KnownNats(..) - , SomeNats(..) - , NatList(..) - , someNatsVal - , someNatsValPos - , reifyNats - , reifyNats' - , sameNats - , elimNatList - -- ** Traversals - , traverseNatList - , traverseNatList' - , traverseNatList_ - -- *** Maps - , mapNatList - , mapNatList' - -- * 'KnownSymbols' - , KnownSymbols(..) - , SomeSymbols(..) - , SymbolList(..) - , someSymbolsVal - , reifySymbols - , sameSymbols - , elimSymbolList - -- ** Traversals - , traverseSymbolList - , traverseSymbolList' - , traverseSymbolList_ - -- *** Maps - , mapSymbolList - , mapSymbolList' - ) where - -import Data.Functor.Identity -import Data.Kind -import Data.Proxy -import Data.Reflection -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'). --- --- In practice, just knowing that every item has a 'KnownNat' instance is --- not enough; it's nice, but unless you're able to "iterate" over every --- 'Nat' in the list, it's of limited use. That's why this class also --- provides a constructor for @'NatList' ns@, so that you can produce --- a 'NatList' for every @'KnownNat' ns@, which you can iterate over to get --- @'Proxy' n@s for every 'n' in 'ns' along with the @'KnownNat' n@ --- instances. --- --- It also has an analogy to 'natVal', 'natsVal', which lets you get a list --- of the represented 'Integer's for, say, @'Proxy' [1,2,3]@. --- --- __Deprecated:__ Use 'SingI' from /singletons/ instead. -class KnownNats (ns :: [Nat]) where - -- | __Deprecated:__ Use 'fromSing' from /singletons/ instead. - natsVal :: p ns -> [Integer] - -- | __Deprecated:__ Use 'sing' from /singletons/ instead. - 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 _ = [] - natsList = ØNL - -instance (KnownNat n, KnownNats ns) => KnownNats (n ': ns) where - natsVal _ = natVal (Proxy :: Proxy n) : natsVal (Proxy :: Proxy ns) - natsList = Proxy :<# natsList - --- | Represents unknown type-level lists of type-level natural numbers. --- It's a 'NatList', but you don't know what the list contains at --- compile-time. --- --- __Deprecated:__ Use 'SomeSing' from /singletons/ instead. -data SomeNats :: Type 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' --- has a 'KnownNat' instance for you to use. At runtime (after type --- erasure), is more or less equivalent to a @['Integer']@. --- --- Typically generated using 'natsList'. --- --- __Deprecated:__ Use 'Sing' from /singletons/ instead. -data NatList :: [Nat] -> Type where - Ø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) - --- | Utility function for traversing over all of the @'Proxy' n@s in --- a 'NatList', each with the corresponding 'KnownNat' instance available. --- 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' 'SomeNats' 'SomeNat'@. -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 - go = \case - ØNL -> pure $ SomeNats ØNL - n :<# ns -> merge <$> f n <*> go ns - merge :: SomeNat -> SomeNats -> SomeNats - merge = \case - SomeNat n -> \case - SomeNats ns -> - SomeNats (n :<# ns) - --- | 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 = \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. --- Results are ignored. -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 () - 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. --- --- /Since 0.2.1.0/ -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 - :: (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. --- --- __Deprecated:__ Use 'toSing' from /singletons/ instead. -someNatsVal :: [Integer] -> Maybe SomeNats -someNatsVal [] = Just (SomeNats ØNL) -someNatsVal (n:ns) = do - 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 --- the given list, where every @n@ in @ns@ has a 'KnownNat' instance. --- --- Essentially a continuation-style version of 'SomeNats'. --- --- Be aware that this also produces @'KnownNat' n@s where @n@ is negative, --- without complaining. To be consistent, within the library, this --- /should/ be called @reifyNatsPos@; however, the naming choice is for --- consistency with 'reifyNat' from the /reflections/ package. Use --- 'reifyNats'' for a "safe" version. --- --- __Deprecated:__ Use 'withSomeSing' from /singletons/ instead. -reifyNats :: [Integer] -> (forall ns. KnownNats ns => NatList ns -> r) -> r -reifyNats [] f = f ØNL -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 --- the given "default" value instead. --- --- __Deprecated:__ Use 'withSomeSing' from /singletons/ instead. -reifyNats' - :: [Integer] - -> r - -> (forall ns. KnownNats ns => NatList ns -> r) - -> r -reifyNats' ns d f = - 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. --- --- __Deprecated:__ Use 'toSing' from /singletons/ instead. -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). --- --- 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 --- @ --- --- __Deprecated:__ Use '%~' from /singletons/ instead. -sameNats - :: NatList ns - -> NatList ms - -> Maybe (ns :~: ms) -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 -{-# DEPRECATED sameNats "Use (%~) from the singletons package instead" #-} - - --- | @'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' ss@. --- --- For reasons discussed further in the documentation for 'KnownNats', this --- 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. --- --- __Deprecated:__ Use 'SingI from /singletons/ instead. -class KnownSymbols (ss :: [Symbol]) where - -- | __Deprecated:__ Use 'fromSing' from /singletons/ instead. - symbolsVal :: p ss -> [String] - -- | __Deprecated:__ Use 'sing from /singletons/ instead. - 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 _ = [] - symbolsList = ØSL - -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. --- --- __Deprecated:__ Use 'SomeSing' from /singletons/ instead. -data SomeSymbols :: Type 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, --- but each 'n' has a 'KnownSymbol' instance for you to use. At runtime --- (after type erasure), is more or less equivalent to a @['String']@. --- --- Typically generated using 'symbolsList'. --- --- __Deprecated:__ Use 'Sing' from /singletons/ instead. -data SymbolList :: [Symbol] -> Type where - Ø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) - --- | 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' 'SomeSymbols' 'SomeSymbol'@. -traverseSymbolList - :: 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 = \case - ØSL -> pure $ SomeSymbols ØSL - s :<$ ss -> merge <$> f s <*> go ss - merge :: SomeSymbol -> SomeSymbols -> SomeSymbols - merge = \case - SomeSymbol s -> \case - SomeSymbols ss -> - SomeSymbols (s :<$ ss) - --- | Like 'traverseSymbolList', but literally actually a --- @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 = \case - SomeSymbols ns' -> traverseSymbolList (f . SomeSymbol) ns' - --- | 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 ss. Applicative f - => (forall s a. KnownSymbol s => Proxy s -> f a) - -> SymbolList ss - -> f () -traverseSymbolList_ f = go - where - 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 s. KnownSymbol s => Proxy s -> SomeSymbol) - -> SymbolList ss - -> 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) - --- | The "eliminator" for 'SymbolList'. You can think of this as --- a dependently typed analogy for a fold. --- --- /Since 0.2.1.0/ -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. --- --- __Deprecated:__ Use 'toSing' from /singletons/ instead. -someSymbolsVal :: [String] -> SomeSymbols -someSymbolsVal [] = SomeSymbols ØSL -someSymbolsVal (s:ss) = - case someSymbolVal s of - SomeSymbol t -> - 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 --- the given list, where every @s@ in @ss@ has a 'KnownSymbol' instance. --- --- Essentially a continuation-style version of 'SomeSymbols'. --- --- __Deprecated:__ Use 'withSomeSing' from /singletons/ instead. -reifySymbols :: [String] - -> (forall ss. KnownSymbols ss => SymbolList ss -> r) - -> r -reifySymbols [] f = f ØSL -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" --- 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 --- @ --- --- __Deprecated:__ Use '%~' from /singletons/ instead. -sameSymbols - :: SymbolList ns - -> SymbolList ms - -> Maybe (ns :~: ms) -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 -{-# 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 @@ -1,307 +1,434 @@ -{-# LANGUAGE CPP #-} -{-# LANGUAGE ConstraintKinds #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE TypeOperators #-} -#if __GLASGOW_HASKELL__ >= 806 -{-# LANGUAGE NoStarIsType #-} -#endif +{-# LANGUAGE ConstraintKinds #-} +{-# LANGUAGE ExistentialQuantification #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE TypeInType #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE ViewPatterns #-} -- | -- Module : GHC.TypeLits.Witnesses --- Description : Instance witnesses for various arithmetic operations on --- GHC TypeLits. -- Copyright : (c) Justin Le 2016 -- License : MIT -- Maintainer : justin@jle.im -- Stability : unstable -- Portability : non-portable -- --- This module provides witnesses for instances that result from the --- various arithmetic operations on GHC TypeLits 'Nat' types. In general, --- if you have @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@; and if --- you have @'KnownNat' m@, as well, GHC can't infer @'KnownNat' (n + m)@. +-- This module essentially provides a lightweight subset of the +-- /singletons/ library specifically for 'Nat' and 'Symbol', from +-- "GHC.TypeLits". -- --- This can be extremely annoying when dealing with libraries and --- applications where one regularly adds and subtracts type-level nats and --- expects 'KnownNat' instances to follow. For example, vector --- concatenation of length-encoded vector types can be: +-- Its main functionality is for first-class manipulation of 'KnownNat' and +-- 'KnownSymbol' constraints. For example, in general, if you have +-- @'KnownNat' n@, GHC can't infer @'KnownNat' (n + 1)@. And, if you have +-- both @'KnownNat' n@ and @'KnownNat' m@, GHC can't infer @'KnownNat (n +-- + m)@. -- +-- This can be annoying when dealing with libraries and applications where +-- one regularly adds and subtracts type-level nats and expects 'KnownNat' +-- instances to follow. For example, vector concatenation of +-- length-encoded vector types can be: +-- -- @ -- concat :: ('KnownNat' n, 'KnownNat' m) => Vector n a -> Vector m a -> Vector (n + m) a -- @ -- -- But, now @n + m@ does not have a 'KnownNat' instance...which makes --- operations like this extremely less useful! +-- operations like this much less useful. -- --- At the highest level, this module can be used with 'withNatOp': +-- Usually, the easiest way to get around this is to use a typechecker +-- plugin, like +-- . However, +-- we can do this without the help of a typechecker plugin using +-- first-class values, at the cost of some increased verbosity. -- +-- We introduce @'SNat' n@, which is a term-level witness of knownnat-ness +-- that can be manipulated as a first-class value. +-- +-- If we have @'KnownNat' n@, we can construct an @'SNat' n@: +-- -- @ --- getDoubled :: forall n. 'KnownNat' n => 'Proxy' n -> 'Integer' --- getDoubled p = 'withNatOp' ('%*') p ('Proxy' :: 'Proxy' 2) $ --- natVal ('Proxy' :: 'Proxy' (n * 2)) +-- 'SNat' :: KnownNat n -> SNat n -- @ -- --- With the final argument of 'withNatOp', you can provide a result --- computed in an environment where @n * 2@ is indeed an instance of --- 'KnownNat'. --- --- For more complex usage, you can directly manipulate witnesses and then --- use them via pattern matching: +-- Furthermore, if we have an @'SNat' n@, we can /pattern match/ on the +-- 'SNat' constructor to get a @'KnownNat' n@ constraint: -- -- @ --- let pn = 'natDict' ('Proxy' :: 'Proxy' n) --- p1 = 'natDict' ('Proxy' :: 'Proxy' 1) --- p2 = 'natDict' ('Proxy' :: 'Proxy' 2) --- in case pn '%*' p2 '%+' p1 of --- 'Dict' -> 'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1)) +-- myFunc :: SNat n -> Bool +-- myFunc SNat = ... -- in this body, we have `KnownNat n` -- @ -- --- In the branch of the case statement, @n * 2 + 1@ indeed has a 'KnownNat' --- instance. +-- So if we have @'KnownNat' n@ and @'KnownNat' m@, we can get @'KnownNat' +-- (n + m)@ by using '%+', which adds together 'SNat's: -- --- Note that the operators have appropriate fixities to mimic value-level --- arithmetic operations. +-- @ +-- case (SNat :: SNat n) %+ (SNat :: SNat m) of +-- SNat -> -- in this branch, we have `KnownNat (n + m)` +-- @ -- --- __WARNING__: '%-' and 'entailSub' are is implemented in a way such --- that /negative/ 'KnownNat's are produced without any errors. The --- 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. +-- Note that this module converts between 'SNat' and 'Natural', and not +-- 'SNat' and 'Integer', in "GHC.TypeNats"-style. -- - - -module GHC.TypeLits.Witnesses - {-# DEPRECATED "Use singletons package instead" #-} ( - -- * Singletons - -- $singletons - -- * High level wrapper - withNatOp - -- * Direct witnesses - , natDict - , dictNatVal - -- * Witness generators +-- Of course, all of this functionality is provided by the /singletons/ +-- library, in "Data.Singletons.TypeLits". This module can be useful if +-- you want a lightweight alternative without the full might of +-- /singletons/. The main benefit of the /singletons/ library is providing +-- a unified interface for singletons of /all/ different kinds/types, and +-- not just 'Natural' and 'String'. +module GHC.TypeLits.Witnesses ( + -- * Nats + SNat(..) + , SomeNat(SomeNat_) + , Natural(FromSNat) + , fromSNat + , withKnownNat + , withSomeNat + , toSomeNat + -- ** Operations , (%+) , (%-) + , minusSNat + , minusSNat_ , (%*) , (%^) - -- * Entailments - , entailAdd - , entailSub - , entailMul - , entailExp + -- ** Compare + , (%<=?) + , sCmpNat + -- ** Unsafe + , unsafeLiftNatOp1 + , unsafeLiftNatOp2 + -- * Symbols + , SSymbol(..) + , SomeSymbol(SomeSymbol_) + , pattern FromSSymbol + , fromSSymbol + , withKnownSymbol + , withSomeSymbol + , toSomeSymbol ) where -import Data.Constraint +import Data.GADT.Compare +import Data.GADT.Show import Data.Proxy -import Data.Reflection -import GHC.TypeLits +import Data.Type.Equality +import GHC.Natural +import GHC.TypeLits hiding (natVal, someNatVal) +import GHC.TypeLits.Compare hiding ((%<=?)) +import GHC.TypeNats import Unsafe.Coerce +import qualified GHC.TypeLits.Compare as Comp --- $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 '%^'. +-- | An @'SNat' n@ is a witness for @'KnownNat' n@. -- --- * 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'. +-- This means that if you pattern match on the 'SNat' constructor, in that +-- branch you will have a @'KnownNat' n@ constraint. -- --- * 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. +-- @ +-- myFunc :: SNat n -> Bool +-- myFunc SNat = ... -- in this body, we have `KnownNat n` +-- @ -- +-- This is essentially a singleton for 'Nat', and stands in for the +-- /singletons/ 'SNat' and 'Data.Singleton.Sing' types. +data SNat n = KnownNat n => SNat --- | Create a 'Dict' witness for @'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 +deriving instance Eq (SNat n) +deriving instance Ord (SNat n) --- | 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) +instance Show (SNat n) where + showsPrec d x@SNat = showParen (d > 10) $ + showString "SNat @" . showsPrec 11 (fromSNat x) -infixl 6 %+ -infixl 6 %- -infixl 7 %* -infixr 8 %^ +instance GShow SNat where + gshowsPrec = showsPrec --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates --- a witness for @'KnownNat' (n + m)@. +instance TestEquality SNat where + testEquality (SNat :: SNat n) (SNat :: SNat m) = + flip fmap (sameNat (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case + Refl -> Refl + +instance GEq SNat where + geq = testEquality + +instance GCompare SNat where + gcompare x = cmpNatGOrdering . sCmpNat x + +data SomeNat__ = forall n. SomeNat__ (SNat n) + +-- | A useful pattern synonym for matching on a 'SomeNat' as if it +-- contained an @'SNat' n@, and not a @'Proxy' n@ as it exists in +-- "GHC.TypeLits". -- --- Follows proper association and fixity for usage with other similar --- operators. +-- A layer of compatibility letting us use the original 'SomeNat' type in +-- a way that works well with 'SNat'. -- --- 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)) +-- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor. +pattern SomeNat_ :: SNat n -> SomeNat +pattern SomeNat_ x <- ((\case SomeNat (Proxy :: Proxy n) -> SomeNat__ (SNat :: SNat n)) -> SomeNat__ x) + where + SomeNat_ (SNat :: SNat n) = SomeNat (Proxy :: Proxy n) +{-# COMPLETE SomeNat_ #-} --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates --- a witness for @'KnownNat' (n - m)@. +-- | A useful pattern synonym for matching on a 'Natural' as if it "were" +-- a 'SNat': -- --- Note that this is implemented in a way such that /negative/ 'KnownNat's --- are produced without any errors. +-- @ +-- myFunc :: Natural -> Bool +-- myFunc (FromSNat x) = ... -- x is `SNat n`, with `n` coming from the input +-- @ -- --- Follows proper association and fixity for usage with other similar --- operators. +-- It can be used as a function, as well, to convert an @'SNat' n@ back +-- into the 'Natural' that it represents. -- --- 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)) +-- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym. +pattern FromSNat :: SNat n -> Natural +pattern FromSNat x <- ((\i -> withSomeNat i SomeNat_) -> SomeNat_ x) + where + FromSNat = fromSNat +{-# COMPLETE FromSNat #-} --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates --- a witness for @'KnownNat' (n * m)@. +-- | Given an @'SNat' n@ and a value that would require a @'KnownNat' n@ +-- instance, create that value. -- --- Follows proper association and fixity for usage with other similar --- operators. +-- This stands in for the function of the same name from +-- "Data.Singletons.TypeLits". +withKnownNat :: SNat n -> (KnownNat n => r) -> r +withKnownNat SNat x = x + +-- | Promote ("reify") a 'Natural' to an @'SNat' n@, by providing +-- a continuation that would handle it in a way that is polymorphic over +-- all possible @n@. -- --- 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)) +-- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function. +withSomeNat :: Natural -> (forall n. SNat n -> r) -> r +withSomeNat (someNatVal->SomeNat (Proxy :: Proxy n)) x = x (SNat :: SNat n) --- | Given witnesses for @'KnownNat' n@ and @'KnownNat' m@, generates --- a witness for @'KnownNat' (n ^ m)@. +-- | Promote ("reify") a 'Natural' to an @'SNat' n@ existentially hidden +-- inside a 'SomeNat'. To use it, pattern match using 'SomeNat_'. -- --- Follows proper association and fixity for usage with other similar --- operators. -(%^) :: forall n m. Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat (n ^ m)) -Dict %^ Dict = mapDict entailExp (Dict :: Dict (KnownNat n, KnownNat m)) +-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function. +toSomeNat :: Natural -> SomeNat +toSomeNat = someNatVal --- | A high-level the interface of this module. Give it one of --- the witness-generating operators on 'KnownNat's in this module ('%+', --- '%-', '%*', or '%^'), two 'Proxy's containing the 'KnownNat's to --- be modified, and receive an environment where the result of the --- operation (applied to the 'KnownNat's) has a 'KnownNat' instance. +-- | Convert ("reflect") an 'SNat' back into the 'Natural' it represents. -- --- For example, with +-- This stands in the /singletons/ 'Data.Singleton.fromSing' function. +fromSNat :: SNat n -> Natural +fromSNat x@SNat = natVal x + +-- | Lift a unary operation to act on an @'SNat' n@ that returns an @'SNat' +-- m@. The function given must properly describe the relationship between +-- @n@ and @m@. -- +-- For example: +-- -- @ --- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) r +-- double :: SNat n -> SNat (n * 2) +-- double = unsafeLiftNatOp1 (*2) -- @ -- --- in @r@, @n + 1@ has a 'KnownNat' instance: +-- The correctness of the relationship is not checked, so be aware that +-- this can cause programs to break. +unsafeLiftNatOp1 + :: (Natural -> Natural) + -> SNat n + -> SNat m +unsafeLiftNatOp1 f x = withSomeNat (f (fromSNat x)) unsafeCoerce + +-- | Lift a binary operation to act on an @'SNat' n@ and @'SNat' m@ that +-- returns an @'SNat' o@. The function given must properly describe the +-- relationship between @n@, @m@, and @o@. -- +-- For example: +-- -- @ --- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $ --- 'natVal' ('Proxy' :: 'Proxy' (n + 1)) --- -- => will return the 'Integer' correpsonding to n + 1 +-- multiply :: SNat n -> SNat m -> SNat (n * m) +-- multiply = unsafeLiftNatOp2 (*) -- @ -- --- Normally, if @n@ is a 'KnownNat' instance, it is not in general --- inferrable that @n + 1@ also has a 'KnownNat' instance. This combinator --- makes it so. +-- The correctness of the relationship is not checked, so be aware that +-- this can cause programs to break. +unsafeLiftNatOp2 + :: (Natural -> Natural -> Natural) + -> SNat n + -> SNat m + -> SNat o +unsafeLiftNatOp2 f x y = withSomeNat (f (fromSNat x) (fromSNat y)) unsafeCoerce + +-- | Addition of 'SNat's. -- --- For multiple operations on values, this can be chained: +-- This also will provide the correct 'KnownNat' instance for @'SNat' (n +-- + m)@, so can be used as a way to "add" 'KnownNat' instances. -- --- @ --- 'withNatOp' ('%*') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 2) $ --- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' (n*2)) ('Proxy' :: 'Proxy' 1) $ --- 'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1)) --- @ +-- This stands in for the function with the same name from +-- "Data.Singletons.Prelude.Num". +(%+) :: SNat n -> SNat m -> SNat (n + m) +(%+) = unsafeLiftNatOp2 (+) + +-- | Subtraction of 'SNat's. Note that this is unsafe, as will trigger +-- a run-time underflow if @m@ is bigger than @n@ even though it will always +-- succeed at compiletime. -- --- But, at this point, it's easier and simpler to just directly use the --- operators and pattern match: +-- This also will provide the correct 'KnownNat' instance for @'SNat' (n +-- - m)@, so can be used as a way to "subtract" 'KnownNat' instances. -- --- @ --- let pn = 'natDict' ('Proxy' :: 'Proxy' n) --- p1 = 'natDict' ('Proxy' :: 'Proxy' 1) --- p2 = 'natDict' ('Proxy' :: 'Proxy' 2) --- in case pn '%*' p2 '%+' p1 of --- 'Dict' -> 'natVal' ('Proxy' :: 'Proxy' (n * 2 + 1)) --- @ +-- This stands in for the function with the same name from +-- "Data.Singletons.Prelude.Num". +(%-) :: SNat n -> SNat m -> SNat (n - m) +(%-) = unsafeLiftNatOp2 (-) + +-- | A safe version of '%-': it will return 'Left' if @n@ is less than @m@ +-- (with a witness that it is), or else return the subtracted 'SNat' in +-- 'Right' in a way that is guarunteed to not have runtime underflow. +minusSNat + :: SNat n + -> SNat m + -> Either (CmpNat n m :~: 'LT) (SNat (n - m)) +minusSNat (fromSNat->x) (fromSNat->y) = case minusNaturalMaybe x y of + Nothing -> Left (unsafeCoerce Refl) + Just z -> withSomeNat z unsafeCoerce + +-- | A version of 'minusSNat' that just returns a 'Maybe'. +minusSNat_ :: SNat n -> SNat m -> Maybe (SNat (n - m)) +minusSNat_ x = either (const Nothing) Just . minusSNat x + +-- | Addition of 'SNat's. -- --- (Note that associativity and fixity for the witness-generating operators --- are set to match that of normal addition and multiplication, etc.) +-- This also will provide the correct 'KnownNat' instance for @'SNat' (n +-- * m)@, so can be used as a way to "multiply" 'KnownNat' instances. -- --- With /singletons/, @'withNatOp' f x y@ is @'withKnownNat' (f x y)@. +-- This stands in for the function with the same name from +-- "Data.Singletons.Prelude.Num". +(%*) :: SNat n -> SNat m -> SNat (n - m) +(%*) = unsafeLiftNatOp2 (*) + +-- | Exponentiation of 'SNat's. -- --- So, instead of +-- This also will provide the correct 'KnownNat' instance for @'SNat' (n +-- ^ m)@, so can be used as a way to "exponentiate" 'KnownNat' instances. -- +-- This stands in for the function with the same name from +-- "Data.Singletons.TypeLits". +(%^) :: SNat n -> SNat m -> SNat (n ^ m) +(%^) = unsafeLiftNatOp2 (^) + +-- | Compare @n@ and @m@, categorizing them into one of the constructors of +-- ':<=?'. +(%<=?) :: SNat n -> SNat m -> n :<=? m +x@SNat %<=? y@SNat = x Comp.%<=? y + +-- | Compare @n@ and @m@, categorizing them into one of the constructors of +-- 'SCmpNat'. +sCmpNat :: SNat n -> SNat m -> SCmpNat n m +sCmpNat x@SNat y@SNat = cmpNat x y + +-- | An @'SSymbol' n@ is a witness for @'KnownSymbol' n@. +-- +-- This means that if you pattern match on the 'SSymbol' constructor, in that +-- branch you will have a @'KnownSymbol' n@ constraint. +-- -- @ --- 'withNatOp' ('%+') ('Proxy' :: 'Proxy' n) ('Proxy' :: 'Proxy' 1) $ --- 'natVal' ('Proxy' :: 'Proxy' (n + 1)) +-- myFunc :: SSymbol n -> Bool +-- myFunc SSymbol = ... -- in this body, we have `KnownSymbol n` -- @ -- --- You can just use +-- This is essentially a singleton for 'Symbol', and stands in for the +-- /singletons/ 'SSymbol' and 'Data.Singleton.Sing' types. +data SSymbol n = KnownSymbol n => SSymbol + +deriving instance Eq (SSymbol n) +deriving instance Ord (SSymbol n) + +instance Show (SSymbol n) where + showsPrec d x@SSymbol = showParen (d > 10) $ + showString "SSymbol @" . showsPrec 11 (fromSSymbol x) + +instance GShow SSymbol where + gshowsPrec = showsPrec + +instance TestEquality SSymbol where + testEquality (SSymbol :: SSymbol n) (SSymbol :: SSymbol m) = + flip fmap (sameSymbol (Proxy :: Proxy n) (Proxy :: Proxy m)) $ \case + Refl -> Refl + +instance GEq SSymbol where + geq = testEquality + +instance GCompare SSymbol where + gcompare x y = case compare (fromSSymbol x) (fromSSymbol y) of + LT -> GLT + EQ -> unsafeCoerce GEQ + GT -> GGT + +data SomeSymbol__ = forall n. SomeSymbol__ (SSymbol n) + +-- | A useful pattern synonym for matching on a 'SomeSymbol' as if it +-- contained an @'SSymbol' n@, and not a @'Proxy' n@ as it exists in +-- "GHC.TypeLits". -- +-- A layer of compatibility letting us use the original 'SomeSymbol' type in +-- a way that works well with 'SSymbol'. +-- +-- This stands in for the /singletons/ 'Data.Singleton.SomeSing' constructor. +pattern SomeSymbol_ :: SSymbol n -> SomeSymbol +pattern SomeSymbol_ x <- ((\case SomeSymbol (Proxy :: Proxy n) -> SomeSymbol__ (SSymbol :: SSymbol n)) -> SomeSymbol__ x) + where + SomeSymbol_ (SSymbol :: SSymbol n) = SomeSymbol (Proxy :: Proxy n) +{-# COMPLETE SomeSymbol_ #-} + +-- | A useful pattern synonym for matching on a 'String' as if it "were" +-- a 'SSymbol': +-- -- @ --- 'withKnownNat' ('SNat' @n) ('SNat @1) $ --- 'natVal' ('Proxy' :: 'Proxy' (n + 1)) +-- myFunc :: String -> Bool +-- myFunc (FromSSymbol x) = ... -- x is `SSymbol n`, with `n` coming from the input -- @ -- --- 'natVal' can of course be replaced with 'fromSing'. +-- It can be used as a function, as well, to convert an @'SSymbol' n@ back +-- into the 'String' that it represents. -- -withNatOp - :: (KnownNat n, KnownNat m) - => (Dict (KnownNat n) -> Dict (KnownNat m) -> Dict (KnownNat q)) - -> p n - -> p m - -> (KnownNat q => r) - -> r -withNatOp op x y r = case natDict x `op` natDict y of - Dict -> r - --- | An entailment for addition of 'KnownNat' instances. -entailAdd :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n + m) -entailAdd = Sub $ - reifyNat (natVal (Proxy :: Proxy n) + natVal (Proxy :: Proxy m)) $ \p -> - unsafeCoerce (natDict p) +-- This stands in for the /singletons/ 'Data.Singleton.FromSing' pattern synonym, except +-- it matches on a 'String' instead of a 'Data.Text.Text'. +pattern FromSSymbol :: SSymbol n -> String +pattern FromSSymbol x <- ((\i -> withSomeSymbol i SomeSymbol_) -> SomeSymbol_ x) + where + FromSSymbol = fromSSymbol +{-# COMPLETE FromSSymbol #-} --- | An entailment for subtraction of 'KnownNat' instances. +-- | Given an @'SSymbol' n@ and a value that would require a @'KnownSymbol' n@ +-- instance, create that value. -- --- Note that this is implemented in a way such that /negative/ 'KnownNat's --- are produced without any errors. -entailSub :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n - m) -entailSub = Sub $ - reifyNat (natVal (Proxy :: Proxy n) - natVal (Proxy :: Proxy m)) $ \p -> - unsafeCoerce (natDict p) +-- This stands in for the function of the same name from +-- "Data.Singletons.TypeLits". +withKnownSymbol :: SSymbol n -> (KnownSymbol n => r) -> r +withKnownSymbol SSymbol x = x --- | An entailment for multiplication of 'KnownNat' instances. -entailMul :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n * m) -entailMul = Sub $ - reifyNat (natVal (Proxy :: Proxy n) * natVal (Proxy :: Proxy m)) $ \p -> - unsafeCoerce (natDict p) +-- | Promote ("reify") a 'String' to an @'SSymbol' n@, by providing +-- a continuation that would handle it in a way that is polymorphic over +-- all possible @n@. +-- +-- This stands in the /singletons/ 'Data.Singleton.withSomeSing' function, except it takes +-- a 'String' instead of 'Data.Text.Text'. +withSomeSymbol :: String -> (forall n. SSymbol n -> r) -> r +withSomeSymbol (someSymbolVal->SomeSymbol (Proxy :: Proxy n)) x = x (SSymbol :: SSymbol n) --- | An entailment for exponentiation of 'KnownNat' instances. -entailExp :: forall n m. (KnownNat n, KnownNat m) :- KnownNat (n ^ m) -entailExp = Sub $ - reifyNat (natVal (Proxy :: Proxy n) ^ natVal (Proxy :: Proxy m)) $ \p -> - unsafeCoerce (natDict p) +-- | Promote ("reify") a 'String' to an @'SSymbol' n@ existentially hidden +-- inside a 'SomeNat'. To use it, pattern match using 'SomeSymbol_'. +-- +-- This stands in the /singletons/ 'Data.Singleton.toSomeSing' function, except it takes +-- a 'String' instead of 'Data.Text.Text'. +toSomeSymbol :: String -> SomeSymbol +toSomeSymbol = someSymbolVal +-- | Convert ("reflect") an 'SSymbol' back into the 'String' it represents. +-- +-- This stands in the /singletons/ 'Data.Singleton.fromSing' function, except it returns +-- a 'String' instead of 'Data.Text.Text'. +fromSSymbol :: SSymbol n -> String +fromSSymbol x@SSymbol = symbolVal x diff --git a/typelits-witnesses.cabal b/typelits-witnesses.cabal --- a/typelits-witnesses.cabal +++ b/typelits-witnesses.cabal @@ -1,40 +1,26 @@ --- This file has been generated from package.yaml by hpack version 0.28.2. +cabal-version: 1.12 + +-- This file has been generated from package.yaml by hpack version 0.31.1. -- -- see: https://github.com/sol/hpack -- --- hash: 49b45270e83bf287fa91eedadcbf979e2b8e5438d6ec9adaa6e6fea22183f1a0 +-- hash: 8a6351c34d982cd0199ea26cf5f6378e136998abb7019115d627268f8977bdda name: typelits-witnesses -version: 0.3.0.3 +version: 0.4.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 - particular, the arithmetic operations defined in - "GHC.TypeLits", and also for type-level lists of - 'KnownNat' and 'KnownSymbol' instances. - . - This is useful for situations where you have - @'KnownNat' n@, and you want to prove to GHC - @'KnownNat' (n + 3)@, or @'KnownNat' (2*n + 4)@, or when - constraints on the lower or upper limits of @n@ are - needed. - . - It's also useful for when you want to work with type - level lists of 'KnownNat' or 'KnownSymbol' instances and - singletons for traversing them, and be able to apply - analogies of 'natVal' and 'symbolVal' to lists with - analogies for 'SomeNat' and 'SomeSymbol'. - . - Note that most of the functionality in this library can - be reproduced in a more generic way using the great - - library. The versions here are provided as a "plumbing - included" alternative that makes some commonly found - design patterns involving GHC's TypeLits functionality a - little smoother, especially when working with external - libraries or GHC TypeLit's Nat comparison API. +description: This library contains: . - See README for more information. + * A small specialized subset of the *singletons* library as it pertains to + `Nat` and `Symbol`, for when you need some simple functionality without + wanting to invoke the entire *singletons* library. + * Operations for manipulating these singletons and `KnownNat` and + `KnownSymbol` instances, such as addition and multiplication of + singletons/`KnownNat` instances. + * Operations for the comparison of `Nat`s in a way that works well with + *GHC.TypeLits*'s different comparison systems. This is helpful for + bridging together libraries that use different systems; this functionality + is not yet provided by *singletons*. category: Data homepage: https://github.com/mstksg/typelits-witnesses author: Justin Le @@ -42,12 +28,11 @@ copyright: (c) Justin Le 2018 license: MIT license-file: LICENSE -tested-with: GHC>=8.0 && <8.8 +tested-with: GHC>=8.2 && <8.8 build-type: Simple -cabal-version: >= 1.10 extra-source-files: - CHANGELOG.md README.md + CHANGELOG.md source-repository head type: git @@ -55,16 +40,14 @@ library exposed-modules: - GHC.TypeLits.Witnesses - GHC.TypeLits.List GHC.TypeLits.Compare + GHC.TypeLits.Witnesses other-modules: Paths_typelits_witnesses hs-source-dirs: src - ghc-options: -Wall + ghc-options: -Wall -Wredundant-constraints -Werror=incomplete-patterns -Wcompat build-depends: - base >=4.7 && <5 - , constraints - , reflection >=2 + base >=4.10 && <5 + , dependent-sum default-language: Haskell2010