singletons-2.6: A framework for generating singleton types

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.Instances type Sing = SNonEmpty :: NonEmpty 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 = SIdentity :: Identity 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 = SMax :: Max a -> 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 = SOption :: Option 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 = SDual :: Dual 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.Semigroup.Internal type Sing = SSum :: Sum 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.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.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.Prelude.Semigroup type Sing = SArg :: Arg a b -> 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