| Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
|---|---|
| License | BSD-style (see LICENSE) |
| Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
| Stability | experimental |
| Portability | non-portable |
| Safe Haskell | None |
| Language | Haskell2010 |
Data.Singletons.Prelude.Bool
Description
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.
- data family Sing (a :: k)
- type SBool = (Sing :: Bool -> Type)
- type family If k (cond :: Bool) (tru :: k) (fls :: k) :: k where ...
- sIf :: Sing a -> Sing b -> Sing c -> Sing (If a b c)
- type family Not (a :: Bool) :: Bool where ...
- sNot :: forall (t :: Bool). Sing t -> Sing (Apply NotSym0 t :: Bool)
- type family (a :: Bool) :&& (a :: Bool) :: Bool where ...
- type family (a :: Bool) :|| (a :: Bool) :: Bool where ...
- (%:&&) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (:&&$) t) t :: Bool)
- (%:||) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (:||$) t) t :: Bool)
- bool_ :: a -> a -> Bool -> a
- type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ...
- sBool_ :: forall (t :: a) (t :: a) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a)
- type family Otherwise :: Bool where ...
- sOtherwise :: Sing (OtherwiseSym0 :: Bool)
- type TrueSym0 = True
- type FalseSym0 = False
- data NotSym0 (l :: TyFun Bool Bool)
- type NotSym1 (t :: Bool) = Not t
- data (:&&$) (l :: TyFun Bool (TyFun Bool Bool -> Type))
- data (l :: Bool) :&&$$ (l :: TyFun Bool Bool)
- type (:&&$$$) (t :: Bool) (t :: Bool) = (:&&) t t
- data (:||$) (l :: TyFun Bool (TyFun Bool Bool -> Type))
- data (l :: Bool) :||$$ (l :: TyFun Bool Bool)
- type (:||$$$) (t :: Bool) (t :: Bool) = (:||) t t
- data Bool_Sym0 (l :: TyFun a1627668507 (TyFun a1627668507 (TyFun Bool a1627668507 -> Type) -> Type))
- data Bool_Sym1 (l :: a1627668507) (l :: TyFun a1627668507 (TyFun Bool a1627668507 -> Type))
- data Bool_Sym2 (l :: a1627668507) (l :: a1627668507) (l :: TyFun Bool a1627668507)
- type Bool_Sym3 (t :: a1627668507) (t :: a1627668507) (t :: Bool) = Bool_ t t t
- type OtherwiseSym0 = Otherwise
The Bool singleton
The singleton kind-indexed data family.
Instances
| data Sing Bool # | |
| data Sing Ordering # | |
| data Sing * # | |
| data Sing Nat # | |
| data Sing Symbol # | |
| data Sing () # | |
| data Sing [a] # | |
| data Sing (Maybe a) # | |
| data Sing (NonEmpty a) # | |
| data Sing (Either a b) # | |
| data Sing (a, b) # | |
| data Sing ((~>) k1 k2) # | |
| data Sing (a, b, c) # | |
| data Sing (a, b, c, d) # | |
| data Sing (a, b, c, d, e) # | |
| data Sing (a, b, c, d, e, f) # | |
| data Sing (a, b, c, d, e, f, g) # | |
Though Haddock doesn't show it, the Sing instance above declares
constructors
SFalse :: Sing False STrue :: Sing True
Conditionals
type family If k (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #
Type-level If. If True a b ==> a; If False a b ==> b
Singletons from Data.Bool
(%:&&) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (:&&$) t) t :: Bool) infixr 3 #
(%:||) :: forall (t :: Bool) (t :: Bool). Sing t -> Sing t -> Sing (Apply (Apply (:||$) t) t :: Bool) infixr 2 #
The following are derived from the function bool in Data.Bool. The extra
underscore is to avoid name clashes with the type Bool.
sBool_ :: forall (t :: a) (t :: a) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a) #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) #
Defunctionalization symbols
data Bool_Sym0 (l :: TyFun a1627668507 (TyFun a1627668507 (TyFun Bool a1627668507 -> Type) -> Type)) #
type OtherwiseSym0 = Otherwise #