singletons-2.7: A framework for generating singleton types

Data.Singletons.Prelude.Base

Description

Implements singletonized versions of functions from GHC.Base module.

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.Tuple. Also, please excuse the apparent repeated variable names. This is due to an interaction between Template Haskell and Haddock.

Synopsis

# Basic functions

type family Foldr a a a where ... Source #

Equations

 Foldr k z a_6989586621679534224 = Apply (Let6989586621679534236GoSym3 k z a_6989586621679534224) a_6989586621679534224

sFoldr :: forall a b (t :: (~>) a ((~>) b b)) (t :: b) (t :: [a]). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t :: b) Source #

type family Map a a where ... Source #

Equations

 Map _ '[] = NilSym0 Map f ('(:) x xs) = Apply (Apply (:@#@$) (Apply f x)) (Apply (Apply MapSym0 f) xs) sMap :: forall a b (t :: (~>) a b) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply MapSym0 t) t :: [b]) Source # type family a ++ a where ... infixr 5 Source # Equations  '[] ++ ys = ys ('(:) x xs) ++ ys = Apply (Apply (:@#@$) x) (Apply (Apply (++@#@$) xs) ys) (%++) :: forall a (t :: [a]) (t :: [a]). Sing t -> Sing t -> Sing (Apply (Apply (++@#@$) t) t :: [a]) infixr 5 Source #

type family Otherwise where ... Source #

Equations

 Otherwise = TrueSym0

type family Id a where ... Source #

Equations

 Id x = x

sId :: forall a (t :: a). Sing t -> Sing (Apply IdSym0 t :: a) Source #

type family Const a a where ... Source #

Equations

 Const x _ = x

sConst :: forall a b (t :: a) (t :: b). Sing t -> Sing t -> Sing (Apply (Apply ConstSym0 t) t :: a) Source #

type family (a . a) a where ... infixr 9 Source #

Equations

 (f . g) a_6989586621679534181 = Apply (Apply (Apply (Apply Lambda_6989586621679534193Sym0 f) g) a_6989586621679534181) a_6989586621679534181

(%.) :: forall b c a (t :: (~>) b c) (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply (.@#@$) t) t) t :: c) infixr 9 Source # type family a$ a where ... infixr 0 Source #

Equations

 f $x = Apply f x type family a$! a where ... infixr 0 Source #

Equations

 f $! x = Apply f (Let6989586621679534151VxSym2 f x) (%$) :: forall a b (t :: (~>) a b) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply ($@#@$) t) t :: b) infixr 0 Source #

#### Instances

Instances details
 SingI ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) (a6989586621679534210 :: [a]) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply ((++@#@$) :: TyFun [a] ([a] ~> [a]) -> Type) (a6989586621679534210 :: [a]) = (++@#@$$) a6989586621679534210 data a6989586621679534210 ++@#@$$ a6989586621679534211 infixr 5 Source #

#### Instances

Instances details

#### Instances

Instances details
 SingI ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (a6989586621679534187 :: b ~> c) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply ((.@#@$) :: TyFun (b ~> c) ((a ~> b) ~> (a ~> c)) -> Type) (a6989586621679534187 :: b ~> c) = (.@#@$$) a6989586621679534187 :: TyFun (a ~> b) (a ~> c) -> Type data a6989586621679534187 .@#@$$ a6989586621679534188 infixr 9 Source #

#### Instances

Instances details

data a6989586621679534147 $!@#@$$a6989586621679534148 infixr 0 Source # #### Instances Instances details  SingI d => SingI ((!@#@$$) d :: TyFun a b -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (($!@#@$$) a6989586621679534147 :: TyFun a b -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply ((!@#@$$) a6989586621679534147 :: TyFun a b -> Type) (a6989586621679534148 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (($!@#@$$) a6989586621679534147 :: TyFun a b -> Type) (a6989586621679534148 :: a) = a6989586621679534147 !@#@$$$ a6989586621679534148

type ($!@#@$) (a6989586621679534147 :: (~>) a b) (a6989586621679534148 :: a) = (\$!) a6989586621679534147 a6989586621679534148 :: b infixr 0 Source #

data UntilSym0 a6989586621679534129 Source #

#### Instances

Instances details
 SingI (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) (a6989586621679534129 :: a ~> Bool) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (UntilSym0 :: TyFun (a ~> Bool) ((a ~> a) ~> (a ~> a)) -> Type) (a6989586621679534129 :: a ~> Bool) = UntilSym1 a6989586621679534129

data UntilSym1 a6989586621679534129 a6989586621679534130 Source #

#### Instances

Instances details
 SingI d => SingI (UntilSym1 d :: TyFun (a ~> a) (a ~> a) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (UntilSym1 a6989586621679534129 :: TyFun (a ~> a) (a ~> a) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (UntilSym1 a6989586621679534129 :: TyFun (a ~> a) (a ~> a) -> Type) (a6989586621679534130 :: a ~> a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (UntilSym1 a6989586621679534129 :: TyFun (a ~> a) (a ~> a) -> Type) (a6989586621679534130 :: a ~> a) = UntilSym2 a6989586621679534129 a6989586621679534130

data UntilSym2 a6989586621679534129 a6989586621679534130 a6989586621679534131 Source #

#### Instances

Instances details
 (SingI d1, SingI d2) => SingI (UntilSym2 d1 d2 :: TyFun a a -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methodssing :: Sing (UntilSym2 d1 d2) Source # SuppressUnusedWarnings (UntilSym2 a6989586621679534129 a6989586621679534130 :: TyFun a a -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (UntilSym2 a6989586621679534129 a6989586621679534130 :: TyFun a a -> Type) (a6989586621679534131 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (UntilSym2 a6989586621679534129 a6989586621679534130 :: TyFun a a -> Type) (a6989586621679534131 :: a) = UntilSym3 a6989586621679534129 a6989586621679534130 a6989586621679534131

type UntilSym3 (a6989586621679534129 :: (~>) a Bool) (a6989586621679534130 :: (~>) a a) (a6989586621679534131 :: a) = Until a6989586621679534129 a6989586621679534130 a6989586621679534131 :: a Source #

data FlipSym0 a6989586621679534175 Source #

#### Instances

Instances details
 SingI (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (a6989586621679534175 :: a ~> (b ~> c)) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (FlipSym0 :: TyFun (a ~> (b ~> c)) (b ~> (a ~> c)) -> Type) (a6989586621679534175 :: a ~> (b ~> c)) = FlipSym1 a6989586621679534175

data FlipSym1 a6989586621679534175 a6989586621679534176 Source #

#### Instances

Instances details
 SingI d => SingI (FlipSym1 d :: TyFun b (a ~> c) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (FlipSym1 a6989586621679534175 :: TyFun b (a ~> c) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (FlipSym1 a6989586621679534175 :: TyFun b (a ~> c) -> Type) (a6989586621679534176 :: b) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (FlipSym1 a6989586621679534175 :: TyFun b (a ~> c) -> Type) (a6989586621679534176 :: b) = FlipSym2 a6989586621679534175 a6989586621679534176

data FlipSym2 a6989586621679534175 a6989586621679534176 a6989586621679534177 Source #

#### Instances

Instances details
 (SingI d1, SingI d2) => SingI (FlipSym2 d1 d2 :: TyFun a c -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methodssing :: Sing (FlipSym2 d1 d2) Source # SuppressUnusedWarnings (FlipSym2 a6989586621679534175 a6989586621679534176 :: TyFun a c -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (FlipSym2 a6989586621679534175 a6989586621679534176 :: TyFun a c -> Type) (a6989586621679534177 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (FlipSym2 a6989586621679534175 a6989586621679534176 :: TyFun a c -> Type) (a6989586621679534177 :: a) = FlipSym3 a6989586621679534175 a6989586621679534176 a6989586621679534177

type FlipSym3 (a6989586621679534175 :: (~>) a ((~>) b c)) (a6989586621679534176 :: b) (a6989586621679534177 :: a) = Flip a6989586621679534175 a6989586621679534176 a6989586621679534177 :: c Source #

data AsTypeOfSym0 a6989586621679534167 Source #

#### Instances

Instances details
 SingI (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679534167 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (AsTypeOfSym0 :: TyFun a (a ~> a) -> Type) (a6989586621679534167 :: a) = AsTypeOfSym1 a6989586621679534167

data AsTypeOfSym1 a6989586621679534167 a6989586621679534168 Source #

#### Instances

Instances details
 SingI d => SingI (AsTypeOfSym1 d :: TyFun a a -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (AsTypeOfSym1 a6989586621679534167 :: TyFun a a -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (AsTypeOfSym1 a6989586621679534167 :: TyFun a a -> Type) (a6989586621679534168 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (AsTypeOfSym1 a6989586621679534167 :: TyFun a a -> Type) (a6989586621679534168 :: a) = AsTypeOfSym2 a6989586621679534167 a6989586621679534168

type AsTypeOfSym2 (a6989586621679534167 :: a) (a6989586621679534168 :: a) = AsTypeOf a6989586621679534167 a6989586621679534168 :: a Source #

data SeqSym0 a6989586621679534120 infixr 0 Source #

#### Instances

Instances details
 SingI (SeqSym0 :: TyFun a (b ~> b) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (SeqSym0 :: TyFun a (b ~> b) -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (SeqSym0 :: TyFun a (b ~> b) -> Type) (a6989586621679534120 :: a) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (SeqSym0 :: TyFun a (b ~> b) -> Type) (a6989586621679534120 :: a) = SeqSym1 a6989586621679534120 :: TyFun b b -> Type

data SeqSym1 a6989586621679534120 a6989586621679534121 infixr 0 Source #

#### Instances

Instances details
 SingI d => SingI (SeqSym1 d :: TyFun b b -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods SuppressUnusedWarnings (SeqSym1 a6989586621679534120 :: TyFun b b -> Type) Source # Instance detailsDefined in Data.Singletons.Prelude.Base Methods type Apply (SeqSym1 a6989586621679534120 :: TyFun b b -> Type) (a6989586621679534121 :: b) Source # Instance detailsDefined in Data.Singletons.Prelude.Base type Apply (SeqSym1 a6989586621679534120 :: TyFun b b -> Type) (a6989586621679534121 :: b) = SeqSym2 a6989586621679534120 a6989586621679534121

type SeqSym2 (a6989586621679534120 :: a) (a6989586621679534121 :: b) = Seq a6989586621679534120 a6989586621679534121 :: b infixr 0 Source #