Data.Singletons.Tuple

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.

Singleton definitions

See Sing for more info.

data family Sing a

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 = SNat Integer

data Sing Symbol = SSym String

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 (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

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

Singletons from Data.Tuple

type family Fst a :: a

Equations

Fst `(x, z)` = x

sFst :: forall t. Sing t -> Sing (Fst t)

type family Snd a :: b

Equations

Snd `(z, y)` = y

sSnd :: forall t. Sing t -> Sing (Snd t)

type family Curry a a a :: c

Equations

Curry f x y = f `(x, y)`

sCurry :: forall t t t. (forall t. Sing t -> Sing (t t)) -> Sing t -> Sing t -> Sing (Curry t t t)

type family Uncurry a a :: c

Equations

Uncurry f p = f (Fst p) (Snd p)

sUncurry :: forall t t. (forall t. Sing t -> forall t. Sing t -> Sing (t t t)) -> Sing t -> Sing (Uncurry t t)

type family Swap a :: (b, a)

Equations

Swap `(a, b)` = `(b, a)`

sSwap :: forall t. Sing t -> Sing (Swap t)