Data.Singletons.Bool

Defines functions and datatypes relating to the singleton for Bool, including a singletons version of all the definitions in Data.Bool.

Because many of these definitions are produced by Template Haskell, it is not possible to create proper Haddock documentation. Please look up the corresponding operation in Data.Bool. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

The Bool singleton

data family Sing a

The singleton kind-indexed data family.

Though Haddock doesn't show it, the Sing instance above declares constructors

 SFalse :: Sing False
 STrue  :: Sing True

type SBool z = Sing z

SBool is a kind-restricted synonym for Sing: type SBool (a :: Bool) = Sing a

Conditionals

type family If cond tru fls :: k

Type-level If. If True a b ==> a; If False a b ==> b

sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)

Conditional over singletons

Singletons from Data.Bool

type family Not a :: Bool

Type-level not

sNot :: SBool a -> SBool (Not a)

type :&& a b = a && b

type :|| a b = a || b

(%:&&) :: SBool a -> SBool b -> SBool (a :&& b)

(%:||) :: SBool a -> SBool b -> SBool (a :|| b)

The following are derived from the function bool in Data.Bool. The extra underscore is to avoid name clashes with the type Bool.

type family Bool_ a a a :: a

sBool_ :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Bool_ t t t)

type Otherwise = True

sOtherwise :: Sing Otherwise