singletons-0.10.0: A framework for generating singleton types

Copyright(C) 2013 Richard Eisenberg
LicenseBSD-style (see LICENSE)
MaintainerRichard Eisenberg (eir@cis.upenn.edu)
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Tuple

Contents

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

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 (Fst t) Source

type family Snd a :: b Source

Equations

Snd `(z, y)` = y 

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

type family Curry a a a :: c Source

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) Source

type family Uncurry a a :: c Source

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) Source

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

Equations

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

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