Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (eir@cis.upenn.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. 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 t. Sing t -> Sing t -> Sing (Apply (Apply (:&&$) t) t :: Bool)
- (%:||) :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply (:||$) t) t :: Bool)
- bool_ :: forall a. a -> a -> Bool -> a
- type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ...
- sBool_ :: forall t t t. 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
- type NotSym1 t = Not t
- data (:&&$) l
- data l :&&$$ l
- type (:&&$$$) t t = (:&&) t t
- data (:||$) l
- data l :||$$ l
- type (:||$$$) t t = (:||) t t
- data Bool_Sym0 l
- data Bool_Sym1 l l
- data Bool_Sym2 l l l
- type Bool_Sym3 t t t = 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 [a0] # | |
data Sing (Maybe a0) # | |
data Sing (NonEmpty a0) # | |
data Sing (Either a0 b0) # | |
data Sing (a0, b0) # | |
data Sing ((~>) k1 k2) # | |
data Sing (a0, b0, c0) # | |
data Sing (a0, b0, c0, d0) # | |
data Sing (a0, b0, c0, d0, e0) # | |
data Sing (a0, b0, c0, d0, e0, f0) # | |
data Sing (a0, b0, c0, d0, e0, f0, g0) # | |
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
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 t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a) #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) #
Defunctionalization symbols
Instances
SuppressUnusedWarnings (TyFun a6989586621679698428 (TyFun a6989586621679698428 (TyFun Bool a6989586621679698428 -> Type) -> Type) -> *) (Bool_Sym0 a6989586621679698428) # | |
type Apply a6989586621679698428 (TyFun a6989586621679698428 (TyFun Bool a6989586621679698428 -> Type) -> Type) (Bool_Sym0 a6989586621679698428) l0 # | |
type OtherwiseSym0 = Otherwise #