Modulesingletons-3.0.3Haskell2010

Data.Singletons.Sigma

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

4 types
4 classes
8 values

Packagesingletons-3.0.3
Exports19
LanguageHaskell2010
LicenceBSD-3-Clause
SourceSigma.hs

The Sigma type

5 declarations

datadata Sigma s (a :: s ~> Type) where

A dependent pair.

Constructors

(:&:) :: Sing fst -> a @@ fst -> Sigma s ainfixr 4

Instances3Show, SingI, Sing

(ShowSing s, ShowApply t) => Show (Sigma s t)Defined in singletons-3.0.3 · Data.Singletons.Sigma
(SingI fst, SingI b) => SingI (a ':&: b)Defined in singletons-3.0.3 · Data.Singletons.Sigma
type Sing = SSigmaDefined in singletons-3.0.3 · Data.Singletons.Sigma

typetype Σ = Sigma

Unicode shorthand for Sigma.

familytype family Sing :: k -> Type

The singleton kind-indexed type family.

Instances3Sing

type Sing = SLambdaDefined in singletons-3.0.3 · Data.Singletons
type Sing = SWrappedSingDefined in singletons-3.0.3 · Data.Singletons
type Sing = SSigmaDefined in singletons-3.0.3 · Data.Singletons.Sigma

datadata SSigma (a :: Sigma s t) where

The singleton type for Sigma.

Constructors

(:%&:) :: Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd)infixr 4

Instances1Show

(ShowSing s, ShowSingApply t) => Show (SSigma sig)Defined in singletons-3.0.3 · Data.Singletons.Sigma

typetype SΣ = SSigma

Unicode shorthand for SSigma.

Operations over Sigma

10 declarations

valuefstSigma :: SingKind s => Sigma s t -> Demote s

Project the first element out of a dependent pair.

familytype family FstSigma (sig :: Sigma s t) :: s where

Project the first element out of a dependent pair.

Equations

FstSigma (_1 ':&: _2) = fst

valuesndSigma

:: SingKind (t @@ FstSigma sig)
=> SSigma sig
-> Demote (t @@ FstSigma sig)

Project the second element out of a dependent pair.

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

Project the second element out of a dependent pair.

Equations

SndSigma (_1 ':&: b) = b

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

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

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

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

valuemapSigma

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

Map across a Sigma value in a dependent fashion.

valuezipSigma

:: Sing f
-> 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.

valuecurrySigma

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

valueuncurrySigma

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

4 declarations

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

Instances1ShowApply

(forall (x :: a). ShowApply' f x) => ShowApply fDefined in singletons-3.0.3 · Data.Singletons.Sigma

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

Instances1ShowSingApply

(forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply fDefined in singletons-3.0.3 · Data.Singletons.Sigma

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

Instances1ShowApply'

Show (Apply f x) => ShowApply' f xDefined in singletons-3.0.3 · Data.Singletons.Sigma

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

Instances1ShowSingApply'

Show (Sing z) => ShowSingApply' f x zDefined in singletons-3.0.3 · Data.Singletons.Sigma