singletons-3.0.2: Basic singleton types and definitions
Copyright(C) 2017 Ryan Scott
LicenseBSD-style (see LICENSE)
MaintainerRyan Scott
Stabilityexperimental
Portabilitynon-portable
Safe HaskellNone
LanguageHaskell2010

Data.Singletons.Sigma

Description

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

Synopsis

The Sigma type

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

A dependent pair.

Constructors

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

Instances

Instances details
(ShowSing s, ShowApply t) => Show (Sigma s t) Source # 
Instance details

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) Source # 
Instance details

Defined in Data.Singletons.Sigma

Methods

sing :: Sing (a :&: b) Source #

type Sing Source # 
Instance details

Defined in Data.Singletons.Sigma

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

type Σ = Sigma Source #

Unicode shorthand for Sigma.

type family Sing :: k -> Type Source #

The singleton kind-indexed type family.

Instances

Instances details
type Sing Source # 
Instance details

Defined in Data.Singletons

type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source # 
Instance details

Defined in Data.Singletons

type Sing Source # 
Instance details

Defined in Data.Singletons.Sigma

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

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

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

Instances details
(ShowSing s, ShowSingApply t) => Show (SSigma sig) Source # 
Instance details

Defined in Data.Singletons.Sigma

Methods

showsPrec :: Int -> SSigma sig -> ShowS #

show :: SSigma sig -> String #

showList :: [SSigma sig] -> ShowS #

type = SSigma Source #

Unicode shorthand for SSigma.

Operations over Sigma

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

Project the first element out of a dependent pair.

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

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

Project the second element out of a dependent pair.

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

Project the second element out of a dependent pair.

Equations

SndSigma (_ :&: b) = b 

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

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

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

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

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

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

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

Instances

Instances details
(forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type) Source # 
Instance details

Defined in Data.Singletons.Sigma

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

Instances

Instances details
(forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type) Source # 
Instance details

Defined in Data.Singletons.Sigma

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

Instances

Instances details
Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a) Source # 
Instance details

Defined in Data.Singletons.Sigma

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

Instances

Instances details
Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x) Source # 
Instance details

Defined in Data.Singletons.Sigma