singletons-2.6: A framework for generating singleton types

Copyright | (C) 2013-2014 Richard Eisenberg Jan Stolarek
License | BSD-style (see LICENSE)
Maintainer | Ryan Scott
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.Prelude.Bool

Contents

- The `Bool` singleton
- Conditionals
- Singletons from `Data.Bool`
- Defunctionalization symbols

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.

Synopsis

- type family Sing :: k -> Type
- data SBool :: Bool -> Type where
  - SFalse :: SBool 'False
  - STrue :: SBool 'True
- 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 a (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 :: (~>) Bool Bool
- type NotSym1 (a6989586621679372951 :: Bool) = Not a6989586621679372951
- data (&&@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (&&@#@$$) (a6989586621679372419 :: Bool) :: (~>) Bool Bool
- type (&&@#@$$$) (a6989586621679372419 :: Bool) (b6989586621679372420 :: Bool) = (&&) a6989586621679372419 b6989586621679372420
- data (||@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (||@#@$$) (a6989586621679372657 :: Bool) :: (~>) Bool Bool
- type (||@#@$$$) (a6989586621679372657 :: Bool) (b6989586621679372658 :: Bool) = (||) a6989586621679372657 b6989586621679372658
- data Bool_Sym0 :: forall a6989586621679371657. (~>) a6989586621679371657 ((~>) a6989586621679371657 ((~>) Bool a6989586621679371657))
- data Bool_Sym1 (a6989586621679371663 :: a6989586621679371657) :: (~>) a6989586621679371657 ((~>) Bool a6989586621679371657)
- data Bool_Sym2 (a6989586621679371663 :: a6989586621679371657) (a6989586621679371664 :: a6989586621679371657) :: (~>) Bool a6989586621679371657
- type Bool_Sym3 (a6989586621679371663 :: a6989586621679371657) (a6989586621679371664 :: a6989586621679371657) (a6989586621679371665 :: Bool) = Bool_ a6989586621679371663 a6989586621679371664 a6989586621679371665
- type OtherwiseSym0 = Otherwise

# The `Bool` singleton

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

#### Instances

Instances details

type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SBool
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source # |
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source # |
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type

type Sing Source #

A choice of singleton for the kind ``TYPE` rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`.

Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks).

We cannot produce explicit singleton values for everything in ``TYPE` rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.

Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SBool :: Bool -> Type where Source #

Constructors

SFalse :: SBool 'False |
STrue :: SBool 'True |

#### Instances

Instances details

TestCoercion SBool Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (Coercion a b)
TestEquality SBool Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a :: k) (b :: k). SBool a -> SBool b -> Maybe (a :~: b)
Show (SBool z) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SBool z -> ShowS show :: SBool z -> String showList :: [SBool z] -> ShowS

# Conditionals

type family If (cond :: Bool) (tru :: k) (fls :: k) :: k where ... #

Equations

If 'True (tru :: k) (fls :: k) = tru |
If 'False (tru :: k) (fls :: k) = fls |

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) = (res :: Bool) | res -> a where ... #

Equations

Not 'False = 'True |
Not 'True = 'False |

sNot :: Sing a -> Sing (Not a) Source #

Negation of a singleton

type family (a :: Bool) && (b :: Bool) :: Bool where ... #

Equations

'False && a = 'False |
'True && a = a |
a && 'False = 'False |
a && 'True = a |
a && a = a |

type family (a :: Bool) || (b :: Bool) :: Bool where ... #

Equations

'False || a = a |
'True || a = 'True |
a || 'False = a |
a || 'True = 'True |
a || a = a |

(%&&) :: Sing a -> Sing b -> Sing (a && b) infixr 3 Source #

Conjunction of singletons

(%||) :: Sing a -> Sing b -> Sing (a || b) infixr 2 Source #

Disjunction of singletons

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

bool_ :: a -> a -> Bool -> a Source #

type family Bool_ (a :: a) (a :: a) (a :: Bool) :: a where ... Source #

Equations

Bool_ fls _tru 'False = fls |
Bool_ _fls tru 'True = tru |

sBool_ :: forall a (t :: a) (t :: a) (t :: Bool). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Bool_Sym0 t) t) t :: a) Source #

type family Otherwise :: Bool where ... Source #

Equations

Otherwise = TrueSym0 |

sOtherwise :: Sing (OtherwiseSym0 :: Bool) Source #

# Defunctionalization symbols

type TrueSym0 = 'True Source #

type FalseSym0 = 'False Source #

data NotSym0 :: (~>) Bool Bool Source #

#### Instances

Instances details

SingI NotSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing NotSym0 Source #
SuppressUnusedWarnings NotSym0 Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply NotSym0 (a6989586621679372951 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply NotSym0 (a6989586621679372951 :: Bool) = Not a6989586621679372951

type NotSym1 (a6989586621679372951 :: Bool) = Not a6989586621679372951 Source #

data (&&@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 3 Source #

#### Instances

Instances details

SingI (&&@#@$) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (&&@#@$) Source #
SuppressUnusedWarnings (&&@#@$) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (&&@#@$) (a6989586621679372419 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (&&@#@$) (a6989586621679372419 :: Bool) = (&&@#@$$) a6989586621679372419

data (&&@#@$$) (a6989586621679372419 :: Bool) :: (~>) Bool Bool infixr 3 Source #

#### Instances

Instances details

SingI x => SingI ((&&@#@$$) x :: TyFun Bool Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((&&@#@$$) x) Source #
SuppressUnusedWarnings ((&&@#@$$) a6989586621679372419 :: TyFun Bool Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply ((&&@#@$$) a6989586621679372419 :: TyFun Bool Bool -> Type) (b6989586621679372420 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply ((&&@#@$$) a6989586621679372419 :: TyFun Bool Bool -> Type) (b6989586621679372420 :: Bool) = a6989586621679372419 && b6989586621679372420

type (&&@#@$$$) (a6989586621679372419 :: Bool) (b6989586621679372420 :: Bool) = (&&) a6989586621679372419 b6989586621679372420 Source #

data (||@#@$) :: (~>) Bool ((~>) Bool Bool) infixr 2 Source #

#### Instances

Instances details

SingI (||@#@$) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (||@#@$) Source #
SuppressUnusedWarnings (||@#@$) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (||@#@$) (a6989586621679372657 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (||@#@$) (a6989586621679372657 :: Bool) = (||@#@$$) a6989586621679372657

data (||@#@$$) (a6989586621679372657 :: Bool) :: (~>) Bool Bool infixr 2 Source #

#### Instances

Instances details

SingI x => SingI ((||@#@$$) x :: TyFun Bool Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing ((||@#@$$) x) Source #
SuppressUnusedWarnings ((||@#@$$) a6989586621679372657 :: TyFun Bool Bool -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply ((||@#@$$) a6989586621679372657 :: TyFun Bool Bool -> Type) (b6989586621679372658 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply ((||@#@$$) a6989586621679372657 :: TyFun Bool Bool -> Type) (b6989586621679372658 :: Bool) = a6989586621679372657 || b6989586621679372658

type (||@#@$$$) (a6989586621679372657 :: Bool) (b6989586621679372658 :: Bool) = (||) a6989586621679372657 b6989586621679372658 Source #

data Bool_Sym0 :: forall a6989586621679371657. (~>) a6989586621679371657 ((~>) a6989586621679371657 ((~>) Bool a6989586621679371657)) Source #

#### Instances

Instances details

SingI (Bool_Sym0 :: TyFun a (a ~> (Bool ~> a)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing Bool_Sym0 Source #
SuppressUnusedWarnings (Bool_Sym0 :: TyFun a6989586621679371657 (a6989586621679371657 ~> (Bool ~> a6989586621679371657)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym0 :: TyFun a6989586621679371657 (a6989586621679371657 ~> (Bool ~> a6989586621679371657)) -> Type) (a6989586621679371663 :: a6989586621679371657) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym0 :: TyFun a6989586621679371657 (a6989586621679371657 ~> (Bool ~> a6989586621679371657)) -> Type) (a6989586621679371663 :: a6989586621679371657) = Bool_Sym1 a6989586621679371663

data Bool_Sym1 (a6989586621679371663 :: a6989586621679371657) :: (~>) a6989586621679371657 ((~>) Bool a6989586621679371657) Source #

#### Instances

Instances details

SingI d => SingI (Bool_Sym1 d :: TyFun a (Bool ~> a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym1 d) Source #
SuppressUnusedWarnings (Bool_Sym1 a6989586621679371663 :: TyFun a6989586621679371657 (Bool ~> a6989586621679371657) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym1 a6989586621679371663 :: TyFun a6989586621679371657 (Bool ~> a6989586621679371657) -> Type) (a6989586621679371664 :: a6989586621679371657) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym1 a6989586621679371663 :: TyFun a6989586621679371657 (Bool ~> a6989586621679371657) -> Type) (a6989586621679371664 :: a6989586621679371657) = Bool_Sym2 a6989586621679371663 a6989586621679371664

data Bool_Sym2 (a6989586621679371663 :: a6989586621679371657) (a6989586621679371664 :: a6989586621679371657) :: (~>) Bool a6989586621679371657 Source #

#### Instances

Instances details

(SingI d1, SingI d2) => SingI (Bool_Sym2 d1 d2 :: TyFun Bool a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods sing :: Sing (Bool_Sym2 d1 d2) Source #
SuppressUnusedWarnings (Bool_Sym2 a6989586621679371664 a6989586621679371663 :: TyFun Bool a6989586621679371657 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym2 a6989586621679371664 a6989586621679371663 :: TyFun Bool a -> Type) (a6989586621679371665 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym2 a6989586621679371664 a6989586621679371663 :: TyFun Bool a -> Type) (a6989586621679371665 :: Bool) = Bool_ a6989586621679371664 a6989586621679371663 a6989586621679371665

type Bool_Sym3 (a6989586621679371663 :: a6989586621679371657) (a6989586621679371664 :: a6989586621679371657) (a6989586621679371665 :: Bool) = Bool_ a6989586621679371663 a6989586621679371664 a6989586621679371665 Source #

type OtherwiseSym0 = Otherwise Source #