singletons-0.9.3: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
License(C) 2013 Richard Eisenberg
MaintainerRichard Eisenberg (
Safe HaskellNone




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 Source

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 zSource

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


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)Source

Conditional over singletons

Singletons from Data.Bool

type family Not a :: Bool

Type-level not

type :&& a b = a && bSource

type :|| a b = a || bSource

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

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

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 :: aSource

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