singletons 3.0 → 3.0.1
raw patch · 4 files changed
+206/−9 lines, 4 filesdep ~base
Dependency ranges changed: base
Files
- CHANGES.md +11/−0
- singletons.cabal +6/−5
- src/Data/Singletons.hs +169/−4
- tests/ByHand.hs +20/−0
CHANGES.md view
@@ -1,6 +1,17 @@ Changelog for the `singletons` project ====================================== +3.0.1 [2021.10.30]+------------------+* Add `SingI1` and `SingI2`, higher-order versions of `SingI`, to+ `Data.Singletons`, along with various derived functions:++ * `sing{1,2}`+ * `singByProxy{1,2}` and `singByProxy{1,2}#`+ * `usingSing{1,2}`+ * `withSing{1,2}`+ * `singThat{1,2}`+ 3.0 [2021.03.12] ---------------- * The `singletons` library has been split into three libraries:
singletons.cabal view
@@ -1,5 +1,5 @@ name: singletons-version: 3.0+version: 3.0.1 cabal-version: 1.24 synopsis: Basic singleton types and definitions homepage: http://www.github.com/goldfirere/singletons@@ -13,8 +13,9 @@ , GHC == 8.4.4 , GHC == 8.6.5 , GHC == 8.8.4- , GHC == 8.10.4+ , GHC == 8.10.7 , GHC == 9.0.1+ , GHC == 9.2.1 , GHCJS==8.4 extra-source-files: README.md, CHANGES.md license: BSD3@@ -46,7 +47,7 @@ type: git location: https://github.com/goldfirere/singletons.git subdir: singletons- tag: v3.0+ tag: v3.0.1 source-repository head type: git@@ -56,7 +57,7 @@ library hs-source-dirs: src- build-depends: base >= 4.9 && < 4.16+ build-depends: base >= 4.9 && < 4.17 default-language: Haskell2010 exposed-modules: Data.Singletons Data.Singletons.Decide@@ -73,5 +74,5 @@ other-modules: ByHand ByHand2 - build-depends: base >= 4.9 && < 4.16,+ build-depends: base >= 4.9 && < 4.17, singletons
src/Data/Singletons.hs view
@@ -53,17 +53,23 @@ Sing, SLambda(..), (@@), - SingI(..), SingKind(..),+ SingI(..),+ SingI1(..), sing1,+ SingI2(..), sing2,+ SingKind(..), -- * Working with singletons KindOf, SameKind, SingInstance(..), SomeSing(..), singInstance, pattern Sing, withSingI, withSomeSing, pattern FromSing,- singByProxy, demote,+ usingSingI1, usingSingI2,+ singByProxy, singByProxy1, singByProxy2,+ demote, demote1, demote2, - singByProxy#,- withSing, singThat,+ singByProxy#, singByProxy1#, singByProxy2#,+ withSing, withSing1, withSing2,+ singThat, singThat1, singThat2, -- ** @WrappedSing@ WrappedSing(..), SWrappedSing(..), UnwrapSing,@@ -210,6 +216,46 @@ -- extension to use this method the way you want. sing :: Sing a +-- | A version of the 'SingI' class lifted to unary type constructors.+#if __GLASGOW_HASKELL__ >= 900+type SingI1 :: forall {k1} {k2}. (k1 -> k2) -> Constraint+#endif+class+#if __GLASGOW_HASKELL__ >= 806+ (forall x. SingI x => SingI (f x)) =>+#endif+ SingI1 f where+ -- | Lift an explicit singleton through a unary type constructor.+ -- You will likely need the @ScopedTypeVariables@ extension to use this+ -- method the way you want.+ liftSing :: Sing x -> Sing (f x)++-- | Produce a singleton explicitly using implicit 'SingI1' and 'SingI'+-- constraints. You will likely need the @ScopedTypeVariables@ extension to use+-- this method the way you want.+sing1 :: (SingI1 f, SingI x) => Sing (f x)+sing1 = liftSing sing++-- | A version of the 'SingI' class lifted to binary type constructors.+#if __GLASGOW_HASKELL__ >= 900+type SingI2 :: forall {k1} {k2} {k3}. (k1 -> k2 -> k3) -> Constraint+#endif+class+#if __GLASGOW_HASKELL__ >= 806+ (forall x y. (SingI x, SingI y) => SingI (f x y)) =>+#endif+ SingI2 f where+ -- | Lift explicit singletons through a binary type constructor.+ -- You will likely need the @ScopedTypeVariables@ extension to use this+ -- method the way you want.+ liftSing2 :: Sing x -> Sing y -> Sing (f x y)++-- | Produce a singleton explicitly using implicit 'SingI2' and 'SingI'+-- constraints. You will likely need the @ScopedTypeVariables@ extension to use+-- this method the way you want.+sing2 :: (SingI2 f, SingI x, SingI y) => Sing (f x y)+sing2 = liftSing2 sing sing+ -- | An explicitly bidirectional pattern synonym for implicit singletons. -- -- As an __expression__: Constructs a singleton @Sing a@ given a@@ -783,6 +829,20 @@ case toSing x of SomeSing x' -> f x' +-- | Convert a group of 'SingI1' and 'SingI' constraints (representing a+-- function to apply and its argument, respectively) into a single 'SingI'+-- constraint representing the application. You will likely need the+-- @ScopedTypeVariables@ extension to use this method the way you want.+usingSingI1 :: forall f x r. (SingI1 f, SingI x) => (SingI (f x) => r) -> r+usingSingI1 k = withSingI (sing1 @f @x) k++-- | Convert a group of 'SingI2' and 'SingI' constraints (representing a+-- function to apply and its arguments, respectively) into a single 'SingI'+-- constraint representing the application. You will likely need the+-- @ScopedTypeVariables@ extension to use this method the way you want.+usingSingI2 :: forall f x y r. (SingI2 f, SingI x, SingI y) => (SingI (f x y) => r) -> r+usingSingI2 k = withSingI (sing2 @f @x @y) k+ -- | A convenience function useful when we need to name a singleton value -- multiple times. Without this function, each use of 'sing' could potentially -- refer to a different singleton, and one has to use type signatures (often@@ -790,6 +850,22 @@ withSing :: SingI a => (Sing a -> b) -> b withSing f = f sing +-- | A convenience function useful when we need to name a singleton value for a+-- unary type constructor multiple times. Without this function, each use of+-- 'sing1' could potentially refer to a different singleton, and one has to use+-- type signatures (often with @ScopedTypeVariables@) to ensure that they are+-- the same.+withSing1 :: (SingI1 f, SingI x) => (Sing (f x) -> b) -> b+withSing1 f = f sing1++-- | A convenience function useful when we need to name a singleton value for a+-- binary type constructor multiple times. Without this function, each use of+-- 'sing1' could potentially refer to a different singleton, and one has to use+-- type signatures (often with @ScopedTypeVariables@) to ensure that they are+-- the same.+withSing2 :: (SingI2 f, SingI x, SingI y) => (Sing (f x y) -> b) -> b+withSing2 f = f sing2+ -- | A convenience function that names a singleton satisfying a certain -- property. If the singleton does not satisfy the property, then the function -- returns 'Nothing'. The property is expressed in terms of the underlying@@ -798,14 +874,52 @@ => (Demote k -> Bool) -> Maybe (Sing a) singThat p = withSing $ \x -> if p (fromSing x) then Just x else Nothing +-- | A convenience function that names a singleton for a unary type constructor+-- satisfying a certain property. If the singleton does not satisfy the+-- property, then the function returns 'Nothing'. The property is expressed in+-- terms of the underlying representation of the singleton.+singThat1 :: forall k1 k2 (f :: k1 -> k2) (x :: k1).+ (SingKind k2, SingI1 f, SingI x)+ => (Demote k2 -> Bool) -> Maybe (Sing (f x))+singThat1 p = withSing1 $ \x -> if p (fromSing x) then Just x else Nothing++-- | A convenience function that names a singleton for a binary type constructor+-- satisfying a certain property. If the singleton does not satisfy the+-- property, then the function returns 'Nothing'. The property is expressed in+-- terms of the underlying representation of the singleton.+singThat2 :: forall k1 k2 k3 (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).+ (SingKind k3, SingI2 f, SingI x, SingI y)+ => (Demote k3 -> Bool) -> Maybe (Sing (f x y))+singThat2 p = withSing2 $ \x -> if p (fromSing x) then Just x else Nothing+ -- | Allows creation of a singleton when a proxy is at hand. singByProxy :: SingI a => proxy a -> Sing a singByProxy _ = sing +-- | Allows creation of a singleton for a unary type constructor when a proxy+-- is at hand.+singByProxy1 :: (SingI1 f, SingI x) => proxy (f x) -> Sing (f x)+singByProxy1 _ = sing1++-- | Allows creation of a singleton for a binary type constructor when a proxy+-- is at hand.+singByProxy2 :: (SingI2 f, SingI x, SingI y) => proxy (f x y) -> Sing (f x y)+singByProxy2 _ = sing2+ -- | Allows creation of a singleton when a @proxy#@ is at hand. singByProxy# :: SingI a => Proxy# a -> Sing a singByProxy# _ = sing +-- | Allows creation of a singleton for a unary type constructor when a+-- @proxy#@ is at hand.+singByProxy1# :: (SingI1 f, SingI x) => Proxy# (f x) -> Sing (f x)+singByProxy1# _ = sing1++-- | Allows creation of a singleton for a binary type constructor when a+-- @proxy#@ is at hand.+singByProxy2# :: (SingI2 f, SingI x, SingI y) => Proxy# (f x y) -> Sing (f x y)+singByProxy2# _ = sing2+ -- | A convenience function that takes a type as input and demotes it to its -- value-level counterpart as output. This uses 'SingKind' and 'SingI' behind -- the scenes, so @'demote' = 'fromSing' 'sing'@.@@ -817,6 +931,12 @@ -- -- >>> demote @(Nothing :: Maybe Ordering) -- Nothing+--+-- >>> demote @(Just EQ)+-- Just EQ+--+-- >>> demote @'(True,EQ)+-- (True,EQ) demote :: #if __GLASGOW_HASKELL__ >= 900 forall {k} (a :: k). (SingKind k, SingI a) => Demote k@@ -824,6 +944,51 @@ forall a. (SingKind (KindOf a), SingI a) => Demote (KindOf a) #endif demote = fromSing (sing @a)++-- | A convenience function that takes a unary type constructor and its+-- argument as input, applies them, and demotes the result to its+-- value-level counterpart as output. This uses 'SingKind', 'SingI1', and+-- 'SingI' behind the scenes, so @'demote1' = 'fromSing' 'sing1'@.+--+-- This function is intended to be used with @TypeApplications@. For example:+--+-- >>> demote1 @Just @EQ+-- Just EQ+--+-- >>> demote1 @('(,) True) @EQ+-- (True,EQ)+demote1 ::+#if __GLASGOW_HASKELL__ >= 900+ forall {k1} {k2} (f :: k1 -> k2) (x :: k1).+ (SingKind k2, SingI1 f, SingI x) =>+ Demote k2+#else+ forall f x.+ (SingKind (KindOf (f x)), SingI1 f, SingI x) =>+ Demote (KindOf (f x))+#endif+demote1 = fromSing (sing1 @f @x)++-- | A convenience function that takes a binary type constructor and its+-- arguments as input, applies them, and demotes the result to its+-- value-level counterpart as output. This uses 'SingKind', 'SingI2', and+-- 'SingI' behind the scenes, so @'demote2' = 'fromSing' 'sing2'@.+--+-- This function is intended to be used with @TypeApplications@. For example:+--+-- >>> demote2 @'(,) @True @EQ+-- (True,EQ)+demote2 ::+#if __GLASGOW_HASKELL__ >= 900+ forall {k1} {k2} {k3} (f :: k1 -> k2 -> k3) (x :: k1) (y :: k2).+ (SingKind k3, SingI2 f, SingI x, SingI y) =>+ Demote k3+#else+ forall f x y.+ (SingKind (KindOf (f x y)), SingI2 f, SingI x, SingI y) =>+ Demote (KindOf (f x y))+#endif+demote2 = fromSing (sing2 @f @x @y) ---------------------------------------------------------------------- ---- SingI TyCon{N} instances ----------------------------------------
tests/ByHand.hs view
@@ -135,6 +135,8 @@ sing = SZero instance SingI n => SingI (Succ n) where sing = SSucc sing+instance SingI1 Succ where+ liftSing = SSucc instance SingKind Nat where type Demote Nat = Nat fromSing SZero = Zero@@ -221,6 +223,8 @@ sing = SNothing instance SingI a => SingI (Just (a :: k)) where sing = SJust sing+instance SingI1 Just where+ liftSing = SJust instance SingKind k => SingKind (Maybe k) where type Demote (Maybe k) = Maybe (Demote k) fromSing SNothing = Nothing@@ -289,6 +293,10 @@ instance (SingI h, SingI t) => SingI (Cons (h :: k) (t :: List k)) where sing = SCons sing sing+instance SingI h => SingI1 (Cons (h :: k)) where+ liftSing = SCons sing+instance SingI2 Cons where+ liftSing2 = SCons instance SingKind k => SingKind (List k) where type Demote (List k) = List (Demote k) fromSing SNil = Nil@@ -311,8 +319,12 @@ instance (SingI a) => SingI (Left (a :: k)) where sing = SLeft sing+instance SingI1 Left where+ liftSing = SLeft instance (SingI b) => SingI (Right (b :: k)) where sing = SRight sing+instance SingI1 Right where+ liftSing = SRight instance (SingKind k1, SingKind k2) => SingKind (Either k1 k2) where type Demote (Either k1 k2) = Either (Demote k1) (Demote k2) fromSing (SLeft x) = Left (fromSing x)@@ -353,6 +365,8 @@ instance SingI a => SingI (MkComp (a :: Either (Maybe k1) k2)) where sing = SMkComp sing+instance SingI1 MkComp where+ liftSing = SMkComp instance (SingKind k1, SingKind k2) => SingKind (Composite k1 k2) where type Demote (Composite k1 k2) = Composite (Demote k1) (Demote k2)@@ -412,8 +426,14 @@ sing = SNat instance SingI a => SingI (Maybe a) where sing = SMaybe sing+instance SingI1 Maybe where+ liftSing = SMaybe instance (SingI a, SingI n) => SingI (Vec a n) where sing = SVec sing sing+instance SingI a => SingI1 (Vec a) where+ liftSing = SVec sing+instance SingI2 Vec where+ liftSing2 = SVec instance SingKind Type where type Demote Type = Rep