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 |
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.
- data family Sing a
- type STuple0 z = Sing z
- type STuple2 z = Sing z
- type STuple3 z = Sing z
- type STuple4 z = Sing z
- type STuple5 z = Sing z
- type STuple6 z = Sing z
- type STuple7 z = Sing z
- type family Fst a :: a
- sFst :: forall t. Sing t -> Sing (Apply FstSym0 t)
- type family Snd a :: b
- sSnd :: forall t. Sing t -> Sing (Apply SndSym0 t)
- type family Curry a a a :: c
- sCurry :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t)
- type family Uncurry a a :: c
- sUncurry :: forall t t. Sing t -> Sing t -> Sing (Apply (Apply UncurrySym0 t) t)
- type family Swap a :: (,) b a
- sSwap :: forall t. Sing t -> Sing (Apply SwapSym0 t)
- type Tuple0Sym0 = ()
- data Tuple2Sym0 l
- data Tuple2Sym1 l l
- type Tuple2Sym2 t t = (,) t t
- data Tuple3Sym0 l
- data Tuple3Sym1 l l
- data Tuple3Sym2 l l l
- type Tuple3Sym3 t t t = (,,) t t t
- data Tuple4Sym0 l
- data Tuple4Sym1 l l
- data Tuple4Sym2 l l l
- data Tuple4Sym3 l l l l
- type Tuple4Sym4 t t t t = (,,,) t t t t
- data Tuple5Sym0 l
- data Tuple5Sym1 l l
- data Tuple5Sym2 l l l
- data Tuple5Sym3 l l l l
- data Tuple5Sym4 l l l l l
- type Tuple5Sym5 t t t t t = (,,,,) t t t t t
- data Tuple6Sym0 l
- data Tuple6Sym1 l l
- data Tuple6Sym2 l l l
- data Tuple6Sym3 l l l l
- data Tuple6Sym4 l l l l l
- data Tuple6Sym5 l l l l l l
- type Tuple6Sym6 t t t t t t = (,,,,,) t t t t t t
- data Tuple7Sym0 l
- data Tuple7Sym1 l l
- data Tuple7Sym2 l l l
- data Tuple7Sym3 l l l l
- data Tuple7Sym4 l l l l l
- data Tuple7Sym5 l l l l l l
- data Tuple7Sym6 l l l l l l l
- type Tuple7Sym7 t t t t t t t = (,,,,,,) t t t t t t t
- data FstSym0 l
- type FstSym1 t = Fst t
- data SndSym0 l
- type SndSym1 t = Snd t
- data CurrySym0 l
- data CurrySym1 l l
- data CurrySym2 l l l
- type CurrySym3 t t t = Curry t t t
- data UncurrySym0 l
- data UncurrySym1 l l
- type UncurrySym2 t t = Uncurry t t
- data SwapSym0 l
- type SwapSym1 t = Swap t
Singleton definitions
See Sing
for more info.
The singleton kind-indexed data family.
TestCoercion * (Sing *) | |
SDecide k (KProxy k) => TestEquality k (Sing k) | |
data Sing Bool where | |
data Sing Ordering where | |
data Sing * where | |
data Sing Nat where | |
data Sing Symbol where
| |
data Sing () where | |
data Sing [a0] where | |
data Sing (Maybe a0) where | |
data Sing (TyFun k1 k2 -> *) = SLambda {} | |
data Sing (Either a0 b0) where | |
data Sing ((,) a0 b0) where | |
data Sing ((,,) a0 b0 c0) where | |
data Sing ((,,,) a0 b0 c0 d0) where | |
data Sing ((,,,,) a0 b0 c0 d0 e0) where | |
data Sing ((,,,,,) a0 b0 c0 d0 e0 f0) where | |
data Sing ((,,,,,,) a0 b0 c0 d0 e0 f0 g0) where |
Singletons from Data.Tuple
sCurry :: forall t t t. Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply CurrySym0 t) t) t) Source
Defunctionalization symbols
type Tuple0Sym0 = () Source
data Tuple2Sym0 l Source
SuppressUnusedWarnings (TyFun k (TyFun k ((,) k k) -> *) -> *) (Tuple2Sym0 k k) | |
type Apply (TyFun k1 ((,) k k1) -> *) k (Tuple2Sym0 k1 k) l0 = Tuple2Sym1 k k1 l0 |
data Tuple2Sym1 l l Source
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
SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k ((,,) k k k) -> *) -> *) -> *) (Tuple3Sym0 k k k) | |
type Apply (TyFun k2 (TyFun k ((,,) k1 k2 k) -> *) -> *) k1 (Tuple3Sym0 k2 k k1) l0 = Tuple3Sym1 k k1 k2 l0 |
data Tuple3Sym1 l l Source
SuppressUnusedWarnings (k -> TyFun k (TyFun k ((,,) k k k) -> *) -> *) (Tuple3Sym1 k k k) | |
type Apply (TyFun k1 ((,,) k2 k k1) -> *) k (Tuple3Sym1 k1 k2 k l1) l0 = Tuple3Sym2 k2 k k1 l1 l0 |
data Tuple3Sym2 l l l Source
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
SuppressUnusedWarnings (TyFun k (TyFun k (TyFun k (TyFun k ((,,,) k k k k) -> *) -> *) -> *) -> *) (Tuple4Sym0 k k k k) | |
type Apply (TyFun k3 (TyFun k (TyFun k1 ((,,,) k2 k3 k k1) -> *) -> *) -> *) k2 (Tuple4Sym0 k3 k k1 k2) l0 = Tuple4Sym1 k k1 k2 k3 l0 |
data Tuple4Sym1 l l Source
SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k ((,,,) k k k k) -> *) -> *) -> *) (Tuple4Sym1 k k k k) | |
type Apply (TyFun k2 (TyFun k ((,,,) k3 k1 k2 k) -> *) -> *) k1 (Tuple4Sym1 k2 k k3 k1 l1) l0 = Tuple4Sym2 k k3 k1 k2 l1 l0 |
data Tuple4Sym2 l l l Source
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 k1 k2 k3 k l1 l2) l0 = Tuple4Sym3 k2 k3 k k1 l1 l2 l0 |
data Tuple4Sym3 l l l l Source
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
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 k4 (TyFun k (TyFun k1 (TyFun k2 ((,,,,) k3 k4 k k1 k2) -> *) -> *) -> *) -> *) k3 (Tuple5Sym0 k4 k k1 k2 k3) l0 = Tuple5Sym1 k k1 k2 k3 k4 l0 |
data Tuple5Sym1 l l Source
SuppressUnusedWarnings (k -> TyFun k (TyFun k (TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) -> *) -> *) (Tuple5Sym1 k k k k k) | |
type Apply (TyFun k3 (TyFun k (TyFun k1 ((,,,,) k4 k2 k3 k k1) -> *) -> *) -> *) k2 (Tuple5Sym1 k3 k k1 k4 k2 l1) l0 = Tuple5Sym2 k k1 k4 k2 k3 l1 l0 |
data Tuple5Sym2 l l l Source
SuppressUnusedWarnings (k -> k -> TyFun k (TyFun k (TyFun k ((,,,,) k k k k k) -> *) -> *) -> *) (Tuple5Sym2 k k k k k) | |
type Apply (TyFun k2 (TyFun k ((,,,,) k3 k4 k1 k2 k) -> *) -> *) k1 (Tuple5Sym2 k2 k k3 k4 k1 l1 l2) l0 = Tuple5Sym3 k k3 k4 k1 k2 l1 l2 l0 |
data Tuple5Sym3 l l l l Source
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 k1 k2 k3 k4 k l1 l2 l3) l0 = Tuple5Sym4 k2 k3 k4 k k1 l1 l2 l3 l0 |
data Tuple5Sym4 l l l l l Source
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
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 k5 (TyFun k (TyFun k1 (TyFun k2 (TyFun k3 ((,,,,,) k4 k5 k k1 k2 k3) -> *) -> *) -> *) -> *) -> *) k4 (Tuple6Sym0 k5 k k1 k2 k3 k4) l0 = Tuple6Sym1 k k1 k2 k3 k4 k5 l0 |
data Tuple6Sym1 l l Source
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 k4 (TyFun k (TyFun k1 (TyFun k2 ((,,,,,) k5 k3 k4 k k1 k2) -> *) -> *) -> *) -> *) k3 (Tuple6Sym1 k4 k k1 k2 k5 k3 l1) l0 = Tuple6Sym2 k k1 k2 k5 k3 k4 l1 l0 |
data Tuple6Sym2 l l l Source
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 k3 (TyFun k (TyFun k1 ((,,,,,) k4 k5 k2 k3 k k1) -> *) -> *) -> *) k2 (Tuple6Sym2 k3 k k1 k4 k5 k2 l1 l2) l0 = Tuple6Sym3 k k1 k4 k5 k2 k3 l1 l2 l0 |
data Tuple6Sym3 l l l l Source
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 k2 (TyFun k ((,,,,,) k3 k4 k5 k1 k2 k) -> *) -> *) k1 (Tuple6Sym3 k2 k k3 k4 k5 k1 l1 l2 l3) l0 = Tuple6Sym4 k k3 k4 k5 k1 k2 l1 l2 l3 l0 |
data Tuple6Sym4 l l l l l Source
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 k1 k2 k3 k4 k5 k 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
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
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 k6 (TyFun k (TyFun k1 (TyFun k2 (TyFun k3 (TyFun k4 ((,,,,,,) k5 k6 k k1 k2 k3 k4) -> *) -> *) -> *) -> *) -> *) -> *) k5 (Tuple7Sym0 k6 k k1 k2 k3 k4 k5) l0 = Tuple7Sym1 k k1 k2 k3 k4 k5 k6 l0 |
data Tuple7Sym1 l l Source
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 k5 (TyFun k (TyFun k1 (TyFun k2 (TyFun k3 ((,,,,,,) k6 k4 k5 k k1 k2 k3) -> *) -> *) -> *) -> *) -> *) k4 (Tuple7Sym1 k5 k k1 k2 k3 k6 k4 l1) l0 = Tuple7Sym2 k k1 k2 k3 k6 k4 k5 l1 l0 |
data Tuple7Sym2 l l l Source
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 k4 (TyFun k (TyFun k1 (TyFun k2 ((,,,,,,) k5 k6 k3 k4 k k1 k2) -> *) -> *) -> *) -> *) k3 (Tuple7Sym2 k4 k k1 k2 k5 k6 k3 l1 l2) l0 = Tuple7Sym3 k k1 k2 k5 k6 k3 k4 l1 l2 l0 |
data Tuple7Sym3 l l l l Source
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 k3 (TyFun k (TyFun k1 ((,,,,,,) k4 k5 k6 k2 k3 k k1) -> *) -> *) -> *) k2 (Tuple7Sym3 k3 k k1 k4 k5 k6 k2 l1 l2 l3) l0 = Tuple7Sym4 k k1 k4 k5 k6 k2 k3 l1 l2 l3 l0 |
data Tuple7Sym4 l l l l l Source
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 k2 (TyFun k ((,,,,,,) k3 k4 k5 k6 k1 k2 k) -> *) -> *) k1 (Tuple7Sym4 k2 k k3 k4 k5 k6 k1 l1 l2 l3 l4) l0 = Tuple7Sym5 k k3 k4 k5 k6 k1 k2 l1 l2 l3 l4 l0 |
data Tuple7Sym5 l l l l l l Source
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 k1 k2 k3 k4 k5 k6 k 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
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 UncurrySym0 l Source
SuppressUnusedWarnings (TyFun (TyFun k (TyFun k k -> *) -> *) (TyFun ((,) k k) k -> *) -> *) (UncurrySym0 k k k) | |
type Apply (TyFun ((,) k1 k2) k -> *) (TyFun k1 (TyFun k2 k -> *) -> *) (UncurrySym0 k k1 k2) l0 = UncurrySym1 k k1 k2 l0 |
data UncurrySym1 l l Source
SuppressUnusedWarnings ((TyFun k (TyFun k k -> *) -> *) -> TyFun ((,) k k) k -> *) (UncurrySym1 k k k) | |
type Apply k ((,) k1 k2) (UncurrySym1 k k1 k2 l1) l0 = UncurrySym2 k k1 k2 l1 l0 |
type UncurrySym2 t t = Uncurry t t Source