Copyright	(C) 2017 Ryan Scott
License	BSD-style (see LICENSE)
Maintainer	Ryan Scott
Stability	experimental
Portability	non-portable
Safe Haskell	None
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 :: s ~> Type). 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.Prelude.Instances type Sing = SBool
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.TypeLits.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SMaybe :: Maybe a -> Type
type Sing Source #	A choice of singleton for the kind `TYPE rep` (for some `RuntimeRep` `rep`), an instantiation of which is the famous kind `Type`. Conceivably, one could generalize this instance to `Sing @k` for any kind `k`, and remove all other `Sing` instances. We don't adopt this design, however, since it is far more convenient in practice to work with explicit singleton values than `TypeRep`s (for instance, `TypeRep`s are more difficult to pattern match on, and require extra runtime checks). We cannot produce explicit singleton values for everything in `TYPE rep`, however, since it is an open kind, so we reach for `TypeRep` in this one particular case.
Instance details Defined in Data.Singletons.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SOption :: Option a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Monoid type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Ord type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Semigroup type Sing = SArg :: Arg a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Internal type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Sigma type Sing = SSigma :: Sigma s t -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Const type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Prelude.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SSigma :: forall s (t :: s ~> Type). 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`