singleton-bool 0.1.4 → 0.1.5
raw patch · 3 files changed
+101/−38 lines, 3 filesdep +decdep ~base
Dependencies added: dec
Dependency ranges changed: base
Files
- CHANGELOG.md +4/−0
- singleton-bool.cabal +31/−31
- src/Data/Singletons/Bool.hs +66/−7
CHANGELOG.md view
@@ -1,3 +1,7 @@+- 0.1.5+ - Add `discreteBool :: Dec (a :~: b)` (GHC-7.8+)+ - Add `Show`, `Eq`, `Ord` `SBool b` instances.+ - 0.1.4 - Add `fromSBool` and `withSomeSBool`.
singleton-bool.cabal view
@@ -1,44 +1,44 @@-name: singleton-bool-version: 0.1.4-synopsis: Type level booleans-description: Type level booleans.- .- @singletons@ package provides similar functionality,- but it has tight dependency constraints.-category: Web-homepage: https://github.com/phadej/singleton-bool#readme-bug-reports: https://github.com/phadej/singleton-bool/issues-author: Oleg Grenrus <oleg.grenrus@iki.fi>-maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>-license: BSD3-license-file: LICENSE-build-type: Simple-cabal-version: >= 1.10+cabal-version: >=1.10+name: singleton-bool+version: 0.1.5+synopsis: Type level booleans+description:+ Type level booleans.+ .+ @singletons@ package provides similar functionality,+ but it has tight dependency constraints.++category: Web+homepage: https://github.com/phadej/singleton-bool#readme+bug-reports: https://github.com/phadej/singleton-bool/issues+author: Oleg Grenrus <oleg.grenrus@iki.fi>+maintainer: Oleg Grenrus <oleg.grenrus@iki.fi>+license: BSD3+license-file: LICENSE+build-type: Simple tested-with:- GHC==7.6.3,- GHC==7.8.4,- GHC==7.10.3,- GHC==8.0.2,- GHC==8.2.2,- GHC==8.4.1+ GHC ==8.8.1 || ==8.6.5 || ==8.4.4 || ==8.2.2 || ==8.0.2 || ==7.10.3 || ==7.8.4 || ==7.6.3 extra-source-files: CHANGELOG.md README.md source-repository head- type: git+ type: git location: https://github.com/phadej/singleton-bool library- hs-source-dirs:- src- ghc-options: -Wall+ hs-source-dirs: src+ ghc-options: -Wall build-depends:- base >=4.6 && <4.12- exposed-modules:- Data.Singletons.Bool+ base >=4.6 && <4.13++ if impl(ghc >= 7.8)+ build-depends:+ dec >=0.0.3 && <0.1++ exposed-modules: Data.Singletons.Bool default-language: Haskell2010 - if !impl(ghc >= 7.8)- build-depends: tagged >= 0.8.5 && <0.9+ if !impl(ghc >=7.8)+ build-depends: tagged >=0.8.5 && <0.9
src/Data/Singletons/Bool.hs view
@@ -10,6 +10,7 @@ {-# OPTIONS_GHC -Wno-redundant-constraints #-} #endif #if MIN_VERSION_base(4,7,0)+{-# LANGUAGE EmptyCase #-} {-# LANGUAGE FlexibleContexts #-} #endif -- | Additions to "Data.Type.Bool".@@ -20,6 +21,11 @@ withSomeSBool, reflectBool, reifyBool,+ -- * Data.Type.Dec+#if MIN_VERSION_base(4,7,0)+ -- | 'discreteBool' is available with @base >= 4.7@ (GHC-7.8)+ discreteBool,+#endif -- * Data.Type.Bool and .Equality -- | These are only defined with @base >= 4.7@ #if MIN_VERSION_base(4,7,0)@@ -31,12 +37,17 @@ #if MIN_VERSION_base(4,7,0) import Data.Type.Bool+import Data.Type.Dec (Dec (..)) import Data.Type.Equality import Unsafe.Coerce (unsafeCoerce) #endif import Data.Proxy (Proxy (..)) +-- $setup+-- >>> :set -XDataKinds -XTypeOperators+-- >>> import Data.Type.Dec (decShow)+ data SBool (b :: Bool) where STrue :: SBool 'True SFalse :: SBool 'False@@ -45,13 +56,26 @@ instance SBoolI 'True where sbool = STrue instance SBoolI 'False where sbool = SFalse +-- | @since 0.1.5+instance Show (SBool b) where+ showsPrec _ STrue = showString "STrue"+ showsPrec _ SFalse = showString "SFalse"++-- | @since 0.1.5+instance Eq (SBool b) where+ _ == _ = True++-- | @since 0.1.5+instance Ord (SBool b) where+ compare _ _ = EQ+ ------------------------------------------------------------------------------- -- conversion to and from explicit SBool values ------------------------------------------------------------------------------- -- | Convert an 'SBool' to the corresponding 'Bool'. ----- @since next+-- @since 0.1.4 fromSBool :: SBool b -> Bool fromSBool STrue = True fromSBool SFalse = False@@ -61,7 +85,7 @@ -- >>> withSomeSBool True fromSBool -- True ----- @since next+-- @since 0.1.4 withSomeSBool :: Bool -> (forall b. SBool b -> r) -> r withSomeSBool True f = f STrue withSomeSBool False f = f SFalse@@ -70,7 +94,7 @@ -- reify & reflect ------------------------------------------------------------------------------- --- | Reify 'Bool'.+-- | Reify 'Bool' to type-level. -- -- >>> reifyBool True reflectBool -- True@@ -79,16 +103,39 @@ reifyBool True f = f (Proxy :: Proxy 'True) reifyBool False f = f (Proxy :: Proxy 'False) +-- | Reflect to term-level.+--+-- >>> reflectBool (Proxy :: Proxy 'True)+-- True reflectBool :: forall b proxy. SBoolI b => proxy b -> Bool-reflectBool _ = case sbool :: SBool b of- STrue -> True- SFalse -> False+reflectBool _ = fromSBool (sbool :: SBool b) -------------------------------------------------------------------------------+-- Discrete+-------------------------------------------------------------------------------++#if MIN_VERSION_base(4,7,0)+-- | Decidable equality.+--+-- >>> decShow (discreteBool :: Dec ('True :~: 'True))+-- "Yes Refl"+--+-- @since 0.1.5+discreteBool :: forall a b. (SBoolI a, SBoolI b) => Dec (a :~: b)+discreteBool = case (sbool :: SBool a, sbool :: SBool b) of+ (STrue, STrue) -> Yes Refl+ (STrue, SFalse) -> No $ \p -> case p of {}+ (SFalse, STrue) -> No $ \p -> case p of {}+ (SFalse, SFalse) -> Yes Refl+#endif++------------------------------------------------------------------------------- -- Witnesses ------------------------------------------------------------------------------- #if MIN_VERSION_base(4,7,0)+-- | >>> sboolAnd STrue SFalse+-- SFalse sboolAnd :: SBool a -> SBool b -> SBool (a && b) sboolAnd SFalse _ = SFalse sboolAnd STrue b = b@@ -113,10 +160,22 @@ trivialRefl :: () :~: () trivialRefl = Refl +-- GHC 8.10+ requires that all kind variables be explicitly quantified after+-- a `forall`. Technically, GHC has had the ability to do this since GHC 8.0,+-- but GHC 8.0-8.4 require enabling TypeInType to do. To avoid having to faff+-- around with CPP to enable TypeInType on certain GHC versions, we only+-- explicitly quantify kind variables on GHC 8.6 or later, since those versions+-- do not require TypeInType, only PolyKinds.+# if __GLASGOW_HASKELL__ >= 806+# define KVS(kvs) kvs+# else+# define KVS(kvs)+# endif+ -- | Useful combination of 'sbool' and 'eqToRefl' -- -- @since 0.1.2.0-sboolEqRefl :: forall (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)+sboolEqRefl :: forall KVS(k) (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b) sboolEqRefl = case sbool :: SBool (a == b) of STrue -> Just eqToRefl SFalse -> Nothing