singletons-2.5.1: 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

- data family Sing :: k -> Type
- 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 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 (a6989586621679366606 :: Bool) = Not a6989586621679366606
- data (&&@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (&&@#@$$) (a6989586621679366065 :: Bool) :: (~>) Bool Bool
- type (&&@#@$$$) (a6989586621679366065 :: Bool) (b6989586621679366066 :: Bool) = (&&) a6989586621679366065 b6989586621679366066
- data (||@#@$) :: (~>) Bool ((~>) Bool Bool)
- data (||@#@$$) (a6989586621679366306 :: Bool) :: (~>) Bool Bool
- type (||@#@$$$) (a6989586621679366306 :: Bool) (b6989586621679366307 :: Bool) = (||) a6989586621679366306 b6989586621679366307
- data Bool_Sym0 :: forall a6989586621679365314. (~>) a6989586621679365314 ((~>) a6989586621679365314 ((~>) Bool a6989586621679365314))
- data Bool_Sym1 (a6989586621679365320 :: a6989586621679365314) :: (~>) a6989586621679365314 ((~>) Bool a6989586621679365314)
- data Bool_Sym2 (a6989586621679365320 :: a6989586621679365314) (a6989586621679365321 :: a6989586621679365314) :: (~>) Bool a6989586621679365314
- type Bool_Sym3 (a6989586621679365320 :: a6989586621679365314) (a6989586621679365321 :: a6989586621679365314) (a6989586621679365322 :: Bool) = Bool_ a6989586621679365320 a6989586621679365321 a6989586621679365322
- type OtherwiseSym0 = Otherwise

# The `Bool` singleton

data family Sing :: k -> Type Source #

The singleton kind-indexed data family.

Instances

SDecide k => TestCoercion (Sing :: k -> Type) Source # |
Instance details Defined in Data.Singletons.Decide Methods testCoercion :: Sing a -> Sing b -> Maybe (Coercion a b) Source #
SDecide k => TestEquality (Sing :: k -> Type) Source # |
Instance details Defined in Data.Singletons.Decide Methods testEquality :: Sing a -> Sing b -> Maybe (a :~: b) Source #
Show (SSymbol s) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SSymbol s -> ShowS Source # show :: SSymbol s -> String Source # showList :: [SSymbol s] -> ShowS Source #
Show (SNat n) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SNat n -> ShowS Source # show :: SNat n -> String Source # showList :: [SNat n] -> ShowS Source #
Eq (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods (==) :: Sing a -> Sing a -> Bool Source # (/=) :: Sing a -> Sing a -> Bool Source #
Ord (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods compare :: Sing a -> Sing a -> Ordering Source # (<) :: Sing a -> Sing a -> Bool Source # (<=) :: Sing a -> Sing a -> Bool Source # (>) :: Sing a -> Sing a -> Bool Source # (>=) :: Sing a -> Sing a -> Bool Source # max :: Sing a -> Sing a -> Sing a Source # min :: Sing a -> Sing a -> Sing a Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing a) Source # |
Instance details Defined in Data.Singletons.TypeRepTYPE Methods showsPrec :: Int -> Sing a -> ShowS Source # show :: Sing a -> String Source # showList :: [Sing a] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing b) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing m => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing (Maybe a) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Monoid Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing Bool => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing Bool => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
ShowSing a => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.Prelude.Semigroup Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> Sing z -> ShowS Source # show :: Sing z -> String Source # showList :: [Sing z] -> ShowS Source #
data Sing (a :: Bool) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

- SFalse :: forall (a :: Bool). Sing False
- STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

- SLT :: forall (a :: Ordering). Sing LT
- SEQ :: forall (a :: Ordering). Sing EQ
- SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

- SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol) Source # |

Instance details

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

- SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ()) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

- STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances data Sing (a :: Void)
data Sing (a :: All) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

- SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

- SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (a :: PErrorMessage) Source # |

Instance details

Defined in Data.Singletons.TypeError

data Sing (a :: PErrorMessage) where

- SText :: forall (a :: PErrorMessage) (t :: Symbol). Sing t -> Sing (Text t)
- SShowType :: forall (a :: PErrorMessage) t (ty :: t). Sing ty -> Sing (ShowType ty :: ErrorMessage' Symbol)
- (:%<>:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :<>: e2)
- (:%$$:) :: forall (a :: PErrorMessage) (e1 :: ErrorMessage' Symbol) (e2 :: ErrorMessage' Symbol). Sing e1 -> Sing e2 -> Sing (e1 :$$: e2)

data Sing (b :: [a]) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

- SNil :: forall k (b :: [k]). Sing ([] :: [k])
- SCons :: forall a (b :: [a]) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n ': n)

data Sing (b :: Maybe a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

- SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
- SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

newtype Sing (a :: TYPE rep) 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 -> Type` 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 newtype Sing (a :: TYPE rep) = STypeRep (TypeRep a)
data Sing (b :: Min a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

- SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

- SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

- SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

- SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

- SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

- SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

- SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

- SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

- SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

- SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

- SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

- SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

- SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

- (:%|) :: forall a (b :: NonEmpty a) (n :: a) (n :: [a]). Sing n -> Sing n -> Sing (n :| n)

data Sing (c :: Either a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

- SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
- SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

- STuple2 :: forall a b (c :: (a, b)) (n :: a) (n :: b). Sing n -> Sing n -> Sing ((,) n n)

data Sing (c :: Arg a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

- SArg :: forall a b (c :: Arg a b) (n :: a) (n :: b). Sing n -> Sing n -> Sing (Arg n n)

newtype Sing (f :: k1 ~> k2) Source # |

Instance details

Defined in Data.Singletons.Internal

newtype Sing (f :: k1 ~> k2) = SLambda {

- applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (d :: (a, b, c)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

- STuple3 :: forall a b c (d :: (a, b, c)) (n :: a) (n :: b) (n :: c). Sing n -> Sing n -> Sing n -> Sing ((,,) n n n)

data Sing (c :: Const a b) Source # |

Instance details

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

- SConst :: forall k a (b :: k) (c :: Const a b) (a :: a). {..} -> Sing (Const a :: Const a b)

data Sing (e :: (a, b, c, d)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

- STuple4 :: forall a b c d (e :: (a, b, c, d)) (n :: a) (n :: b) (n :: c) (n :: d). Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,) n n n n)

data Sing (f :: (a, b, c, d, e)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

- STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,) n n n n n)

data Sing (g :: (a, b, c, d, e, f)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

- STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,) n n n n n n)

data Sing (h :: (a, b, c, d, e, f, g)) Source # |

Instance details

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

- STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n :: a) (n :: b) (n :: c) (n :: d) (n :: e) (n :: f) (n :: g). Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing n -> Sing ((,,,,,,) n n n n n n n)

Though Haddock doesn't show it, the `Sing` instance above declares constructors

    SFalse :: Sing False
    STrue  :: Sing True

type SBool = (Sing :: Bool -> Type) Source #

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

# Conditionals

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

Type-level If. `If True a b` ==> `a`; `If False a b` ==> `b`

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 ... Source #

Type-level "not". An injective type family since `4.10.0.0`.

Since: base-4.7.0.0

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 ... infixr 3 Source #

Type-level "and"

Equations

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

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

Type-level "or"

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

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 (a6989586621679366606 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply NotSym0 (a6989586621679366606 :: Bool) = Not a6989586621679366606

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

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

Instances

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 (&&@#@$) (a6989586621679366065 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (&&@#@$) (a6989586621679366065 :: Bool) = (&&@#@$$) a6989586621679366065

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

Instances

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

type (&&@#@$$$) (a6989586621679366065 :: Bool) (b6989586621679366066 :: Bool) = (&&) a6989586621679366065 b6989586621679366066 Source #

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

Instances

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 (||@#@$) (a6989586621679366306 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (||@#@$) (a6989586621679366306 :: Bool) = (||@#@$$) a6989586621679366306

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

Instances

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

type (||@#@$$$) (a6989586621679366306 :: Bool) (b6989586621679366307 :: Bool) = (||) a6989586621679366306 b6989586621679366307 Source #

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

Instances

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 a6989586621679365314 (a6989586621679365314 ~> (Bool ~> a6989586621679365314)) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym0 :: TyFun a6989586621679365314 (a6989586621679365314 ~> (Bool ~> a6989586621679365314)) -> Type) (a6989586621679365320 :: a6989586621679365314) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym0 :: TyFun a6989586621679365314 (a6989586621679365314 ~> (Bool ~> a6989586621679365314)) -> Type) (a6989586621679365320 :: a6989586621679365314) = Bool_Sym1 a6989586621679365320

data Bool_Sym1 (a6989586621679365320 :: a6989586621679365314) :: (~>) a6989586621679365314 ((~>) Bool a6989586621679365314) Source #

Instances

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 a6989586621679365320 :: TyFun a6989586621679365314 (Bool ~> a6989586621679365314) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym1 a6989586621679365320 :: TyFun a6989586621679365314 (Bool ~> a6989586621679365314) -> Type) (a6989586621679365321 :: a6989586621679365314) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym1 a6989586621679365320 :: TyFun a6989586621679365314 (Bool ~> a6989586621679365314) -> Type) (a6989586621679365321 :: a6989586621679365314) = Bool_Sym2 a6989586621679365320 a6989586621679365321

data Bool_Sym2 (a6989586621679365320 :: a6989586621679365314) (a6989586621679365321 :: a6989586621679365314) :: (~>) Bool a6989586621679365314 Source #

Instances

(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 a6989586621679365321 a6989586621679365320 :: TyFun Bool a6989586621679365314 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool Methods suppressUnusedWarnings :: () Source #
type Apply (Bool_Sym2 a6989586621679365321 a6989586621679365320 :: TyFun Bool a -> Type) (a6989586621679365322 :: Bool) Source # |
Instance details Defined in Data.Singletons.Prelude.Bool type Apply (Bool_Sym2 a6989586621679365321 a6989586621679365320 :: TyFun Bool a -> Type) (a6989586621679365322 :: Bool) = Bool_ a6989586621679365321 a6989586621679365320 a6989586621679365322

type Bool_Sym3 (a6989586621679365320 :: a6989586621679365314) (a6989586621679365321 :: a6989586621679365314) (a6989586621679365322 :: Bool) = Bool_ a6989586621679365320 a6989586621679365321 a6989586621679365322 Source #

type OtherwiseSym0 = Otherwise Source #