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 |
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.
Synopsis
- data family Sing (a :: k)
- type SBool = (Sing :: Bool -> Type)
- type family If (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) = (res :: Bool) | res -> a where ...
- sNot :: Sing a -> Sing (Not a)
- type family (a :: Bool) && (b :: Bool) :: Bool where ...
- type family (a :: Bool) || (b :: Bool) :: Bool where ...
- (%&&) :: Sing a -> Sing b -> Sing (a && b)
- (%||) :: Sing a -> Sing b -> Sing (a || b)
- 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 a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type))
- data Bool_Sym1 (l :: a6989586621679289682) (l :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type))
- data Bool_Sym2 (l :: a6989586621679289682) (l :: a6989586621679289682) (l :: TyFun Bool a6989586621679289682)
- type Bool_Sym3 (t :: a6989586621679289682) (t :: a6989586621679289682) (t :: Bool) = Bool_ t t t
- type OtherwiseSym0 = Otherwise
The Bool
singleton
data family Sing (a :: k) Source #
The singleton kind-indexed data family.
Instances
data Sing (z :: Bool) Source # | |
data Sing (z :: Ordering) Source # | |
data Sing (a :: Type) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
data Sing (z :: ()) Source # | |
data Sing (z :: Void) Source # | |
data Sing (z :: [a]) Source # | |
data Sing (z :: Maybe a) Source # | |
data Sing (z :: NonEmpty a) Source # | |
data Sing (z :: Either a b) Source # | |
data Sing (z :: (a, b)) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (z :: (a, b, c)) Source # | |
data Sing (z :: (a, b, c, d)) Source # | |
data Sing (z :: (a, b, c, d, e)) Source # | |
data Sing (z :: (a, b, c, d, e, f)) Source # | |
data Sing (z :: (a, b, c, d, e, f, g)) Source # | |
Though Haddock doesn't show it, the Sing
instance above declares
constructors
SFalse :: Sing False STrue :: Sing True
Conditionals
type family If (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
type family Not (a :: Bool) = (res :: Bool) | res -> a where ... #
Type-level "not". An injective type family since 4.10.0.0
.
Since: 4.7.0.0
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) Source #
sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #
Defunctionalization symbols
data Bool_Sym0 (l :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type)) Source #
Instances
SuppressUnusedWarnings (Bool_Sym0 :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type) -> *) Source # | |
suppressUnusedWarnings :: () Source # | |
type Apply (Bool_Sym0 :: TyFun a6989586621679289682 (TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> Type) -> *) (l :: a6989586621679289682) Source # | |
data Bool_Sym1 (l :: a6989586621679289682) (l :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type)) Source #
Instances
SuppressUnusedWarnings (Bool_Sym1 :: a6989586621679289682 -> TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> *) Source # | |
suppressUnusedWarnings :: () Source # | |
type Apply (Bool_Sym1 l1 :: TyFun a6989586621679289682 (TyFun Bool a6989586621679289682 -> Type) -> *) (l2 :: a6989586621679289682) Source # | |
data Bool_Sym2 (l :: a6989586621679289682) (l :: a6989586621679289682) (l :: TyFun Bool a6989586621679289682) Source #
type Bool_Sym3 (t :: a6989586621679289682) (t :: a6989586621679289682) (t :: Bool) = Bool_ t t t Source #
type OtherwiseSym0 = Otherwise Source #