singletons-1.1: A framework for generating singleton types

Data.Singletons.Prelude.Tuple

Description

Defines functions and datatypes relating to the singleton for tuples, including a singletons version of all the definitions in Data.Tuple.

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

# Singleton definitions

data family Sing a Source

The singleton kind-indexed data family.

Instances

 TestCoercion * (Sing *) SDecide k (KProxy k) => TestEquality k (Sing k) data Sing Bool whereSFalse :: (~) Bool z False => Sing Bool zSTrue :: (~) Bool z True => Sing Bool z data Sing Ordering whereSLT :: (~) Ordering z LT => Sing Ordering zSEQ :: (~) Ordering z EQ => Sing Ordering zSGT :: (~) Ordering z GT => Sing Ordering z data Sing * whereSTypeRep :: Typeable * a => Sing * a data Sing Nat whereSNat :: KnownNat n => Sing Nat n data Sing Symbol whereSSym :: KnownSymbol n => Sing Symbol n data Sing () whereSTuple0 :: (~) () z () => Sing () z data Sing [a0] whereSNil :: (~) [a] z ([] a) => Sing [a] zSCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z data Sing (Maybe a0) whereSNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) zSJust :: (~) (Maybe a) z (Just a n) => Sing a n -> Sing (Maybe a) z data Sing (TyFun k1 k2 -> *) = SLambda {applySing :: forall t. Sing k1 t -> Sing k2 ((@@) k2 k1 f t)} data Sing (Either a0 b0) whereSLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) zSRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z data Sing ((,) a0 b0) whereSTuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z data Sing ((,,) a0 b0 c0) whereSTuple3 :: (~) ((,,) a b c) z ((,,) a b c n n n) => Sing a n -> Sing b n -> Sing c n -> Sing ((,,) a b c) z data Sing ((,,,) a0 b0 c0 d0) whereSTuple4 :: (~) ((,,,) a b c d) z ((,,,) a b c d n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing ((,,,) a b c d) z data Sing ((,,,,) a0 b0 c0 d0 e0) whereSTuple5 :: (~) ((,,,,) a b c d e) z ((,,,,) a b c d e n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing ((,,,,) a b c d e) z data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) whereSTuple6 :: (~) ((,,,,,) a b c d e f) z ((,,,,,) a b c d e f n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing ((,,,,,) a b c d e f) z data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) whereSTuple7 :: (~) ((,,,,,,) a b c d e f g) z ((,,,,,,) a b c d e f g n n n n n n n) => Sing a n -> Sing b n -> Sing c n -> Sing d n -> Sing e n -> Sing f n -> Sing g n -> Sing ((,,,,,,) a b c d e f g) z

type STuple0 z = Sing z Source

type STuple2 z = Sing z Source

type STuple3 z = Sing z Source

type STuple4 z = Sing z Source

type STuple5 z = Sing z Source

type STuple6 z = Sing z Source

type STuple7 z = Sing z Source

# Singletons from Data.Tuple

type family Fst a :: a Source

Equations

 Fst ((,) x z) = x

sFst :: forall t. Sing t -> Sing (Apply FstSym0 t) Source

type family Snd a :: b Source

Equations

 Snd ((,) z y) = y

sSnd :: forall t. Sing t -> Sing (Apply SndSym0 t) Source

type family Curry a a a :: c Source

Equations

 Curry f x y = Apply f (Apply (Apply Tuple2Sym0 x) y)

sCurry :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t) Source

type family Uncurry a a :: c Source

Equations

 Uncurry f p = Apply (Apply f (Apply FstSym0 p)) (Apply SndSym0 p)

sUncurry :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t) Source

type family Swap a :: (,) b a Source

Equations

 Swap ((,) a b) = Apply (Apply Tuple2Sym0 b) a

sSwap :: forall t. Sing t -> Sing (Apply SwapSym0 t) Source

# Defunctionalization symbols

data Tuple2Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k ((,) k k) -> *) -> *) (Tuple2Sym0 k k) type Apply (TyFun k1 ((,) k k1) -> *) k (Tuple2Sym0 k k1) l0 = Tuple2Sym1 k k1 l0

data Tuple2Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k ((,) k k) -> *) (Tuple2Sym1 k k) type Apply ((,) k1 k) k (Tuple2Sym1 k1 k l1) l0 = Tuple2Sym2 k1 k l1 l0

type Tuple2Sym2 t t = (,) t t Source

data Tuple3Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k ((,,) k k k) -> *) -> *) -> *) (Tuple3Sym0 k k k) type Apply (TyFun k1 (TyFun k2 ((,,) k k1 k2) -> *) -> *) k (Tuple3Sym0 k k1 k2) l0 = Tuple3Sym1 k k1 k2 l0

data Tuple3Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k (TyFun k ((,,) k k k) -> *) -> *) (Tuple3Sym1 k k k) type Apply (TyFun k1 ((,,) k2 k k1) -> *) k (Tuple3Sym1 k2 k k1 l1) l0 = Tuple3Sym2 k2 k k1 l1 l0

data Tuple3Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> TyFun k ((,,) k k k) -> *) (Tuple3Sym2 k k k) type Apply ((,,) k1 k2 k) k (Tuple3Sym2 k1 k2 k l1 l2) l0 = Tuple3Sym3 k1 k2 k l1 l2 l0

type Tuple3Sym3 t t t = (,,) t t t Source

data Tuple4Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k (TyFun k ((,,,) k k k k) -> *) -> *) -> *) -> *) (Tuple4Sym0 k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 ((,,,) k k1 k2 k3) -> *) -> *) -> *) k (Tuple4Sym0 k k1 k2 k3) l0 = Tuple4Sym1 k k1 k2 k3 l0

data Tuple4Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k ((,,,) k k k k) -> *) -> *) -> *) (Tuple4Sym1 k k k k) type Apply (TyFun k1 (TyFun k2 ((,,,) k3 k k1 k2) -> *) -> *) k (Tuple4Sym1 k3 k k1 k2 l1) l0 = Tuple4Sym2 k3 k k1 k2 l1 l0

data Tuple4Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> TyFun k (TyFun k ((,,,) k k k k) -> *) -> *) (Tuple4Sym2 k k k k) type Apply (TyFun k1 ((,,,) k2 k3 k k1) -> *) k (Tuple4Sym2 k2 k3 k k1 l1 l2) l0 = Tuple4Sym3 k2 k3 k k1 l1 l2 l0

data Tuple4Sym3 l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> TyFun k ((,,,) k k k k) -> *) (Tuple4Sym3 k k k k) type Apply ((,,,) k1 k2 k3 k) k (Tuple4Sym3 k1 k2 k3 k l1 l2 l3) l0 = Tuple4Sym4 k1 k2 k3 k l1 l2 l3 l0

type Tuple4Sym4 t t t t = (,,,) t t t t Source

data Tuple5Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) -> *) -> *) -> *) (Tuple5Sym0 k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 ((,,,,) k k1 k2 k3 k4) -> *) -> *) -> *) -> *) k (Tuple5Sym0 k k1 k2 k3 k4) l0 = Tuple5Sym1 k k1 k2 k3 k4 l0

data Tuple5Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) -> *) -> *) (Tuple5Sym1 k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 ((,,,,) k4 k k1 k2 k3) -> *) -> *) -> *) k (Tuple5Sym1 k4 k k1 k2 k3 l1) l0 = Tuple5Sym2 k4 k k1 k2 k3 l1 l0

data Tuple5Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> TyFun k (TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) -> *) (Tuple5Sym2 k k k k k) type Apply (TyFun k1 (TyFun k2 ((,,,,) k3 k4 k k1 k2) -> *) -> *) k (Tuple5Sym2 k3 k4 k k1 k2 l1 l2) l0 = Tuple5Sym3 k3 k4 k k1 k2 l1 l2 l0

data Tuple5Sym3 l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) (Tuple5Sym3 k k k k k) type Apply (TyFun k1 ((,,,,) k2 k3 k4 k k1) -> *) k (Tuple5Sym3 k2 k3 k4 k k1 l1 l2 l3) l0 = Tuple5Sym4 k2 k3 k4 k k1 l1 l2 l3 l0

data Tuple5Sym4 l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> TyFun k ((,,,,) k k k k k) -> *) (Tuple5Sym4 k k k k k) type Apply ((,,,,) k1 k2 k3 k4 k) k (Tuple5Sym4 k1 k2 k3 k4 k l1 l2 l3 l4) l0 = Tuple5Sym5 k1 k2 k3 k4 k l1 l2 l3 l4 l0

type Tuple5Sym5 t t t t t = (,,,,) t t t t t Source

data Tuple6Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,) k k k k k k) -> *) -> *) -> *) -> *) -> *) -> *) (Tuple6Sym0 k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 (TyFun k5 ((,,,,,) k k1 k2 k3 k4 k5) -> *) -> *) -> *) -> *) -> *) k (Tuple6Sym0 k k1 k2 k3 k4 k5) l0 = Tuple6Sym1 k k1 k2 k3 k4 k5 l0

data Tuple6Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,) k k k k k k) -> *) -> *) -> *) -> *) -> *) (Tuple6Sym1 k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 ((,,,,,) k5 k k1 k2 k3 k4) -> *) -> *) -> *) -> *) k (Tuple6Sym1 k5 k k1 k2 k3 k4 l1) l0 = Tuple6Sym2 k5 k k1 k2 k3 k4 l1 l0

data Tuple6Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,) k k k k k k) -> *) -> *) -> *) -> *) (Tuple6Sym2 k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 ((,,,,,) k4 k5 k k1 k2 k3) -> *) -> *) -> *) k (Tuple6Sym2 k4 k5 k k1 k2 k3 l1 l2) l0 = Tuple6Sym3 k4 k5 k k1 k2 k3 l1 l2 l0

data Tuple6Sym3 l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> TyFun k (TyFun k (TyFun k ((,,,,,) k k k k k k) -> *) -> *) -> *) (Tuple6Sym3 k k k k k k) type Apply (TyFun k1 (TyFun k2 ((,,,,,) k3 k4 k5 k k1 k2) -> *) -> *) k (Tuple6Sym3 k3 k4 k5 k k1 k2 l1 l2 l3) l0 = Tuple6Sym4 k3 k4 k5 k k1 k2 l1 l2 l3 l0

data Tuple6Sym4 l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> TyFun k (TyFun k ((,,,,,) k k k k k k) -> *) -> *) (Tuple6Sym4 k k k k k k) type Apply (TyFun k1 ((,,,,,) k2 k3 k4 k5 k k1) -> *) k (Tuple6Sym4 k2 k3 k4 k5 k k1 l1 l2 l3 l4) l0 = Tuple6Sym5 k2 k3 k4 k5 k k1 l1 l2 l3 l4 l0

data Tuple6Sym5 l l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> k -> TyFun k ((,,,,,) k k k k k k) -> *) (Tuple6Sym5 k k k k k k) type Apply ((,,,,,) k1 k2 k3 k4 k5 k) k (Tuple6Sym5 k1 k2 k3 k4 k5 k l1 l2 l3 l4 l5) l0 = Tuple6Sym6 k1 k2 k3 k4 k5 k l1 l2 l3 l4 l5 l0

type Tuple6Sym6 t t t t t t = (,,,,,) t t t t t t Source

data Tuple7Sym0 l Source

Instances

 SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) -> *) -> *) -> *) -> *) -> *) (Tuple7Sym0 k k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 (TyFun k5 (TyFun k6 ((,,,,,,) k k1 k2 k3 k4 k5 k6) -> *) -> *) -> *) -> *) -> *) -> *) k (Tuple7Sym0 k k1 k2 k3 k4 k5 k6) l0 = Tuple7Sym1 k k1 k2 k3 k4 k5 k6 l0

data Tuple7Sym1 l l Source

Instances

 SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) -> *) -> *) -> *) -> *) (Tuple7Sym1 k k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 (TyFun k5 ((,,,,,,) k6 k k1 k2 k3 k4 k5) -> *) -> *) -> *) -> *) -> *) k (Tuple7Sym1 k6 k k1 k2 k3 k4 k5 l1) l0 = Tuple7Sym2 k6 k k1 k2 k3 k4 k5 l1 l0

data Tuple7Sym2 l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> TyFun k (TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) -> *) -> *) -> *) (Tuple7Sym2 k k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 ((,,,,,,) k5 k6 k k1 k2 k3 k4) -> *) -> *) -> *) -> *) k (Tuple7Sym2 k5 k6 k k1 k2 k3 k4 l1 l2) l0 = Tuple7Sym3 k5 k6 k k1 k2 k3 k4 l1 l2 l0

data Tuple7Sym3 l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> TyFun k (TyFun k (TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) -> *) -> *) (Tuple7Sym3 k k k k k k k) type Apply (TyFun k1 (TyFun k2 (TyFun k3 ((,,,,,,) k4 k5 k6 k k1 k2 k3) -> *) -> *) -> *) k (Tuple7Sym3 k4 k5 k6 k k1 k2 k3 l1 l2 l3) l0 = Tuple7Sym4 k4 k5 k6 k k1 k2 k3 l1 l2 l3 l0

data Tuple7Sym4 l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> TyFun k (TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) -> *) (Tuple7Sym4 k k k k k k k) type Apply (TyFun k1 (TyFun k2 ((,,,,,,) k3 k4 k5 k6 k k1 k2) -> *) -> *) k (Tuple7Sym4 k3 k4 k5 k6 k k1 k2 l1 l2 l3 l4) l0 = Tuple7Sym5 k3 k4 k5 k6 k k1 k2 l1 l2 l3 l4 l0

data Tuple7Sym5 l l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> k -> TyFun k (TyFun k ((,,,,,,) k k k k k k k) -> *) -> *) (Tuple7Sym5 k k k k k k k) type Apply (TyFun k1 ((,,,,,,) k2 k3 k4 k5 k6 k k1) -> *) k (Tuple7Sym5 k2 k3 k4 k5 k6 k k1 l1 l2 l3 l4 l5) l0 = Tuple7Sym6 k2 k3 k4 k5 k6 k k1 l1 l2 l3 l4 l5 l0

data Tuple7Sym6 l l l l l l l Source

Instances

 SuppressUnusedWarnings (k -> k -> k -> k -> k -> k -> TyFun k ((,,,,,,) k k k k k k k) -> *) (Tuple7Sym6 k k k k k k k) type Apply ((,,,,,,) k1 k2 k3 k4 k5 k6 k) k (Tuple7Sym6 k1 k2 k3 k4 k5 k6 k l1 l2 l3 l4 l5 l6) l0 = Tuple7Sym7 k1 k2 k3 k4 k5 k6 k l1 l2 l3 l4 l5 l6 l0

type Tuple7Sym7 t t t t t t t = (,,,,,,) t t t t t t t Source

data FstSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun ((,) k k) k -> *) (FstSym0 k k) type Apply k ((,) k k1) (FstSym0 k k1) l0 = FstSym1 k k1 l0

type FstSym1 t = Fst t Source

data SndSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun ((,) k k) k -> *) (SndSym0 k k) type Apply k ((,) k1 k) (SndSym0 k1 k) l0 = SndSym1 k1 k l0

type SndSym1 t = Snd t Source

data CurrySym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun ((,) k k) k -> *) (TyFun k (TyFun k k -> *) -> *) -> *) (CurrySym0 k k k) type Apply (TyFun k (TyFun k1 k2 -> *) -> *) (TyFun ((,) k k1) k2 -> *) (CurrySym0 k k1 k2) l0 = CurrySym1 k k1 k2 l0

data CurrySym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun ((,) k k) k -> *) -> TyFun k (TyFun k k -> *) -> *) (CurrySym1 k k k) type Apply (TyFun k1 k2 -> *) k (CurrySym1 k k1 k2 l1) l0 = CurrySym2 k k1 k2 l1 l0

data CurrySym2 l l l Source

Instances

 SuppressUnusedWarnings ((TyFun ((,) k k) k -> *) -> k -> TyFun k k -> *) (CurrySym2 k k k) type Apply k2 k (CurrySym2 k1 k k2 l1 l2) l0 = CurrySym3 k1 k k2 l1 l2 l0

type CurrySym3 t t t = Curry t t t Source

data UncurrySym0 l Source

Instances

 SuppressUnusedWarnings (TyFun (TyFun k (TyFun k k -> *) -> *) (TyFun ((,) k k) k -> *) -> *) (UncurrySym0 k k k) type Apply (TyFun ((,) k k1) k2 -> *) (TyFun k (TyFun k1 k2 -> *) -> *) (UncurrySym0 k k1 k2) l0 = UncurrySym1 k k1 k2 l0

data UncurrySym1 l l Source

Instances

 SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> TyFun ((,) k k) k -> *) (UncurrySym1 k k k) type Apply k2 ((,) k k1) (UncurrySym1 k k1 k2 l1) l0 = UncurrySym2 k k1 k2 l1 l0

type UncurrySym2 t t = Uncurry t t Source

data SwapSym0 l Source

Instances

 SuppressUnusedWarnings (TyFun ((,) k k) ((,) k k) -> *) (SwapSym0 k k) type Apply ((,) k1 k) ((,) k k1) (SwapSym0 k k1) l0 = SwapSym1 k k1 l0

type SwapSym1 t = Swap t Source