Copyright	(C) 2017 Ryan Scott
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	Safe-Inferred
Language	Haskell2010

Data.Singletons.Sigma

Contents

The Sigma type
Operations over Sigma
Internal utilities

Description

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

Synopsis

data Sigma (s :: Type) :: (s ~> Type) -> Type where
- (:&:) :: forall s t fst. Sing (fst :: s) -> (t @@ fst) -> Sigma s t
type Σ = Sigma
type family Sing :: k -> Type
data SSigma :: forall s t. Sigma s t -> Type where
- (:%&:) :: forall s t (fst :: s) (sfst :: Sing fst) (snd :: t @@ fst). Sing ('WrapSing sfst) -> Sing snd -> SSigma (sfst ':&: snd :: Sigma s t)
type SΣ = SSigma
fstSigma :: forall s t. SingKind s => Sigma s t -> Demote s
type family FstSigma (sig :: Sigma s t) :: s where ...
sndSigma :: forall s t (sig :: Sigma s t). SingKind (t @@ FstSigma sig) => SSigma sig -> Demote (t @@ FstSigma sig)
type family SndSigma (sig :: Sigma s t) :: t @@ FstSigma sig where ...
projSigma1 :: (forall (fst :: s). Sing fst -> r) -> Sigma s t -> r
projSigma2 :: forall s t r. (forall (fst :: s). (t @@ fst) -> r) -> Sigma s t -> r
mapSigma :: Sing (f :: a ~> b) -> (forall (x :: a). (p @@ x) -> q @@ (f @@ x)) -> Sigma a p -> Sigma b q
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
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)
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
class (forall (x :: a). ShowApply' f x) => ShowApply (f :: a ~> Type)
class (forall (x :: a) (z :: Apply f x). ShowSingApply' f x z) => ShowSingApply (f :: a ~> Type)
class Show (Apply f x) => ShowApply' (f :: a ~> Type) (x :: a)
class Show (Sing z) => ShowSingApply' (f :: a ~> Type) (x :: a) (z :: Apply f x)

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 = SWrappedSing :: WrappedSing a -> Type
type Sing Source #
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
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 SΣ = 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

The Sigma type

Instances

Instances

Instances

Operations over Sigma

Internal utilities

Instances

Instances

Instances

Instances

The `Sigma` type

Operations over `Sigma`