Data.Singletons.Sigma

Defines Sigma, a dependent pair data type, and related functions.

The Sigma type

data Sigma (s :: Type) :: (s ~> Type) -> Type where

A dependent pair.

Constructors

(:&:) :: forall s t fst. Sing (fst :: s) -> (t @@ fst) -> Sigma s t infixr 4

Instances

(ShowSing s, ShowApply t) => Show (Sigma s t)

Defined in Data.Singletons.Sigma

Methods

showsPrec :: Int -> Sigma s t -> ShowS

show :: Sigma s t -> String

showList :: [Sigma s t] -> ShowS

(SingI fst, SingI b) => SingI (a :&: b :: Sigma s t)

Defined in Data.Singletons.Sigma

Methods

sing :: Sing (a :&: b)

type Sing

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type

type Σ = Sigma

Unicode shorthand for Sigma.

type family Sing :: k -> Type

The singleton kind-indexed type family.

Instances

type Sing

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type

type Sing

Defined in Data.Singletons

type Sing = SWrappedSing :: WrappedSing a -> Type

type Sing

Defined in Data.Singletons.Sigma

type Sing = SSigma :: Sigma s t -> Type

data SSigma :: forall s t. Sigma s t -> Type where

The singleton type for Sigma.

Constructors

(:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst :&: snd :: Sigma s t) infixr 4

Instances

(ShowSing s, ShowSingApply t) => Show (SSigma sig)

Defined in Data.Singletons.Sigma

Methods

showsPrec :: Int -> SSigma sig -> ShowS

show :: SSigma sig -> String

showList :: [SSigma sig] -> ShowS

type SΣ = SSigma

Unicode shorthand for SSigma.

Operations over Sigma

fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s

Project the first element out of a dependent pair.

type family FstSigma (sig :: Sigma s t) :: s where ...

Project the first element out of a dependent pair.

Equations

FstSigma ((_ :: Sing fst) :&: _) = fst

sndSigma :: forall s t (sig :: Sigma s t). SingKind (t @@ FstSigma sig) => SSigma sig -> Demote (t @@ FstSigma sig)

Project the second element out of a dependent pair.

type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig where ...

Project the second element out of a dependent pair.

Equations

SndSigma (_ :&: b) = b

projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r

Project the first element out of a dependent pair using continuation-passing style.

projSigma2 :: forall s t r. (forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r

Project the second element out of a dependent pair using continuation-passing style.

mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). (p @@ x) -> q @@ (f @@ x)) -> Sigma a p -> Sigma b q

Map across a Sigma value in a dependent fashion.

zipSigma :: Sing (f :: a ~> (b ~> c)) -> (forall (x :: a) (y :: b). (p @@ x) -> (q @@ y) -> r @@ ((f @@ x) @@ y)) -> Sigma a p -> Sigma b q -> Sigma c r

Zip two Sigma values together in a dependent fashion.

currySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (p :: Sigma a b). SSigma p -> c @@ p) -> forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx :&: y)

Convert an uncurried function on Sigma to a curried one.

Together, currySigma and uncurrySigma witness an isomorphism such that the following identities hold:

id1 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
       (forall (p :: Sigma a b). SSigma p -> c @ p)
    -> (forall (p :: Sigma a b). SSigma p -> c  p)
id1 f = uncurrySigma a b c (currySigma a b c f)

id2 :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type).
       (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (WrapSing sx) -> Sing y -> c  (sx :&: y))
    -> (forall (x :: a) (sx :: Sing x) (y :: b  x). Sing (WrapSing sx) -> Sing y -> c  (sx :&: y))
id2 f = currySigma a b c (uncurrySigma a b @c f)

uncurrySigma :: forall a (b :: a ~> Type) (c :: Sigma a b ~> Type). (forall (x :: a) (sx :: Sing x) (y :: b @@ x). Sing ('WrapSing sx) -> Sing y -> c @@ (sx :&: y)) -> forall (p :: Sigma a b). SSigma p -> c @@ p

Convert a curried function on Sigma to an uncurried one.

Together, currySigma and uncurrySigma witness an isomorphism. (Refer to the documentation for currySigma for more details.)

Internal utilities

class (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)

Instances

(forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)

Defined in Data.Singletons.Sigma

class (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)

Instances

(forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)

Defined in Data.Singletons.Sigma

class Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)

Instances

Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)

Defined in Data.Singletons.Sigma

class Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)

Instances

Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)

Defined in Data.Singletons.Sigma