singleton-bool-0.1.8: Type level booleans

Safe Haskell | None
Language | Haskell2010

Data.Singletons.Bool

Contents

- Data.Type.Dec
- Data.Type.Bool and .Equality

Description

Additions to Data.Type.Bool.

Synopsis

- data SBool (b :: Bool) where
  - STrue :: SBool 'True
  - SFalse :: SBool 'False
- class SBoolI (b :: Bool) where
  - sbool :: SBool b
- fromSBool :: forall (b :: Bool). SBool b -> Bool
- withSomeSBool :: Bool -> (forall (b :: Bool). SBool b -> r) -> r
- reflectBool :: forall (b :: Bool) proxy. SBoolI b => proxy b -> Bool
- reifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r
- discreteBool :: forall (a :: Bool) (b :: Bool). (SBoolI a, SBoolI b) => Dec (a :~: b)
- sboolAnd :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a && b)
- sboolOr :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a || b)
- sboolNot :: forall (a :: Bool). SBool a -> SBool (Not a)
- eqToRefl :: forall {k} (a :: k) (b :: k). (a == b) ~ 'True => a :~: b
- eqCast :: (a == b) ~ 'True => a -> b
- sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b)
- trivialRefl :: () :~: ()

# Documentation

data SBool (b :: Bool) where Source #

Constructors

STrue :: SBool 'True |
SFalse :: SBool 'False |

#### Instances

Instances details

EqP SBool Source # | Since: 0.1.7
Instance details Defined in Data.Singletons.Bool Methods eqp :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Bool Source #
GNFData SBool Source # | Since: 0.1.6
Instance details Defined in Data.Singletons.Bool Methods grnf :: forall (a :: Bool). SBool a -> () Source #
GCompare SBool Source # | Since: 0.1.6
Instance details Defined in Data.Singletons.Bool Methods gcompare :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> GOrdering a b Source #

GEq SBool Source #

    >>> geq STrue STrue
    Just Refl

    >>> geq STrue SFalse
    Nothing

Since: 0.1.6

Instance details Defined in Data.Singletons.Bool Methods geq :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Maybe (a :~: b) Source #

GRead SBool Source #

    >>> readsPrec 0 "Some STrue" :: [(Some SBool, String)]
    [(Some STrue,"")]

    >>> readsPrec 0 "Some SFalse" :: [(Some SBool, String)]
    [(Some SFalse,"")]

    >>> readsPrec 0 "Some Else" :: [(Some SBool, String)]
    []

Since: 0.1.6

Instance details Defined in Data.Singletons.Bool Methods greadsPrec :: Int -> GReadS SBool Source #

GShow SBool Source #

    >>> showsPrec 0 STrue ""
    "STrue"

Since: 0.1.6

Instance details Defined in Data.Singletons.Bool Methods gshowsPrec :: forall (a :: Bool). Int -> SBool a -> ShowS Source #
OrdP SBool Source # | Since: 0.1.7
Instance details Defined in Data.Singletons.Bool Methods comparep :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> Ordering Source #
SBoolI b => Boring (SBool b) Source # | Since: 0.1.6
Instance details Defined in Data.Singletons.Bool Methods boring :: SBool b Source #
NFData (SBool b) Source # | Since: 0.1.6
Instance details Defined in Data.Singletons.Bool Methods rnf :: SBool b -> () Source #
Show (SBool b) Source # | Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods showsPrec :: Int -> SBool b -> ShowS Source # show :: SBool b -> String Source # showList :: [SBool b] -> ShowS Source #
Eq (SBool b) Source # | Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods (==) :: SBool b -> SBool b -> Bool Source # (/=) :: SBool b -> SBool b -> Bool Source #
Ord (SBool b) Source # | Since: 0.1.5
Instance details Defined in Data.Singletons.Bool Methods compare :: SBool b -> SBool b -> Ordering Source # (<) :: SBool b -> SBool b -> Bool Source # (<=) :: SBool b -> SBool b -> Bool Source # (>) :: SBool b -> SBool b -> Bool Source # (>=) :: SBool b -> SBool b -> Bool Source # max :: SBool b -> SBool b -> SBool b Source # min :: SBool b -> SBool b -> SBool b Source #

class SBoolI (b :: Bool) where Source #

Methods

sbool :: SBool b Source #

#### Instances

Instances details

SBoolI 'False Source # |
Instance details Defined in Data.Singletons.Bool Methods sbool :: SBool 'False Source #
SBoolI 'True Source # |
Instance details Defined in Data.Singletons.Bool Methods sbool :: SBool 'True Source #

fromSBool :: forall (b :: Bool). SBool b -> Bool Source #

Convert an `SBool` to the corresponding `Bool`.

Since: 0.1.4

withSomeSBool :: Bool -> (forall (b :: Bool). SBool b -> r) -> r Source #

Convert a normal `Bool` to an `SBool`, passing it into a continuation.

    >>> withSomeSBool True fromSBool
    True

Since: 0.1.4

reflectBool :: forall (b :: Bool) proxy. SBoolI b => proxy b -> Bool Source #

Reflect to term-level.

    >>> reflectBool (Proxy :: Proxy 'True)
    True

reifyBool :: Bool -> (forall (b :: Bool). SBoolI b => Proxy b -> r) -> r Source #

Reify `Bool` to type-level.

    >>> reifyBool True reflectBool
    True

# Data.Type.Dec

`discreteBool` is available with `base >= 4.7` (GHC-7.8)

discreteBool :: forall (a :: Bool) (b :: Bool). (SBoolI a, SBoolI b) => Dec (a :~: b) Source #

Decidable equality.

    >>> decShow (discreteBool :: Dec ('True :~: 'True))
    "Yes Refl"

Since: 0.1.5

# Data.Type.Bool and .Equality

These are only defined with `base >= 4.7`

sboolAnd :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a && b) Source #

    >>> sboolAnd STrue SFalse
    SFalse

sboolOr :: forall (a :: Bool) (b :: Bool). SBool a -> SBool b -> SBool (a || b) Source #

sboolNot :: forall (a :: Bool). SBool a -> SBool (Not a) Source #

eqToRefl :: forall {k} (a :: k) (b :: k). (a == b) ~ 'True => a :~: b Source #

Since: 0.1.1.0

eqCast :: (a == b) ~ 'True => a -> b Source #

Since: 0.1.1.0

sboolEqRefl :: forall k (a :: k) (b :: k). SBoolI (a == b) => Maybe (a :~: b) Source #

Useful combination of `sbool` and `eqToRefl`

Since: 0.1.2.0

trivialRefl :: () :~: () Source #

Since: 0.1.1.0