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

- Defunctionalization symbols

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 Σ (s :: Type) (t :: s ~> Type) = Sigma s t
- projSigma1 :: forall s t. SingKind s => Sigma s t -> Demote s
- 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
- data ΣSym0 s6989586621679363791
- data ΣSym1 (s6989586621679363791 :: Type) t6989586621679363792
- type ΣSym2 (s6989586621679363791 :: Type) (t6989586621679363792 :: (~>) s6989586621679363791 Type) = Σ s6989586621679363791 t6989586621679363792

# Documentation

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 |

type Σ (s :: Type) (t :: s ~> Type) = Sigma s t Source #

Unicode shorthand for `Sigma`.

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

Project the first element out of a dependent pair.

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.

In an ideal setting, the type of `projSigma2` would be closer to:

    projSigma2 :: Sing (sig :: Sigma s t) -> t @@ ProjSigma1 sig

But promoting `projSigma1` to a type family is not a simple task. Instead, we do the next-best thing, which is to use Church-style elimination.

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.

# Defunctionalization symbols

data ΣSym0 s6989586621679363791 Source #

Instances

SuppressUnusedWarnings (ΣSym0 :: TyFun Type (TyFun (s6989586621679363791 ~> Type) Type -> Type) -> Type) Source # |
Instance details Defined in Data.Singletons.Sigma Methods suppressUnusedWarnings :: () Source #
type Apply (ΣSym0 :: TyFun Type (TyFun (s1 ~> Type) Type -> Type) -> Type) (s2 :: Type) Source # |
Instance details Defined in Data.Singletons.Sigma type Apply (ΣSym0 :: TyFun Type (TyFun (s1 ~> Type) Type -> Type) -> Type) (s2 :: Type) = (ΣSym1 s2 :: TyFun (s1 ~> Type) Type -> Type)

data ΣSym1 (s6989586621679363791 :: Type) t6989586621679363792 Source #

Instances

SuppressUnusedWarnings (ΣSym1 s2 :: TyFun (s1 ~> Type) Type -> Type) Source # |
Instance details Defined in Data.Singletons.Sigma Methods suppressUnusedWarnings :: () Source #
type Apply (ΣSym1 s6989586621679363791 :: TyFun (s6989586621679363791 ~> Type) Type -> Type) (t6989586621679363792 :: s6989586621679363791 ~> Type) Source # |
Instance details Defined in Data.Singletons.Sigma type Apply (ΣSym1 s6989586621679363791 :: TyFun (s6989586621679363791 ~> Type) Type -> Type) (t6989586621679363792 :: s6989586621679363791 ~> Type) = Σ s6989586621679363791 t6989586621679363792

type ΣSym2 (s6989586621679363791 :: Type) (t6989586621679363792 :: (~>) s6989586621679363791 Type) = Σ s6989586621679363791 t6989586621679363792 Source #