Copyright	(C) 2013 Richard Eisenberg
License	BSD-style (see LICENSE)
Maintainer	Richard Eisenberg (eir@cis.upenn.edu)
Stability	experimental
Portability	non-portable
Safe Haskell	None
Language	Haskell2010

Data.Singletons.Prelude.Tuple

Contents

Singleton definitions
Singletons from Data.Tuple
Defunctionalization symbols

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

See Sing for more info.

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 where SFalse :: (~) Bool z False => Sing Bool z STrue :: (~) Bool z True => Sing Bool z
data Sing Ordering where SLT :: (~) Ordering z LT => Sing Ordering z SEQ :: (~) Ordering z EQ => Sing Ordering z SGT :: (~) Ordering z GT => Sing Ordering z
data Sing * where STypeRep :: Typeable * a => Sing * a
data Sing Nat where SNat :: KnownNat n => Sing Nat n
data Sing Symbol where SSym :: KnownSymbol n => Sing Symbol n
data Sing () where STuple0 :: (~) () z () => Sing () z
data Sing [a0] where SNil :: (~) [a] z ([] a) => Sing [a] z SCons :: (~) [a] z ((:) a n n) => Sing a n -> Sing [a] n -> Sing [a] z
data Sing (Maybe a0) where SNothing :: (~) (Maybe a) z (Nothing a) => Sing (Maybe a) z SJust :: (~) (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) where SLeft :: (~) (Either a b) z (Left a b n) => Sing a n -> Sing (Either a b) z SRight :: (~) (Either a b) z (Right a b n) => Sing b n -> Sing (Either a b) z
data Sing ((,) a0 b0) where STuple2 :: (~) ((,) a b) z ((,) a b n n) => Sing a n -> Sing b n -> Sing ((,) a b) z
data Sing ((,,) a0 b0 c0) where STuple3 :: (~) ((,,) 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) where STuple4 :: (~) ((,,,) 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) where STuple5 :: (~) ((,,,,) 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) where STuple6 :: (~) ((,,,,,) 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) where STuple7 :: (~) ((,,,,,,) 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

type Tuple0Sym0 = `()` Source

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

Singleton definitions

Singletons from Data.Tuple

Defunctionalization symbols

Singletons from `Data.Tuple`