singletons-2.6: A framework for generating singleton types

Copyright | (C) 2018 Ryan Scott
License | BSD-style (see LICENSE)
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu)
Stability | experimental
Portability | non-portable
Safe Haskell | None
Language | Haskell2010

Data.Singletons.Prelude.Identity

Contents

- The `Identity` singleton
- Defunctionalization symbols
- Orphan instances

Description

Exports the promoted and singled versions of the `Identity` data type.

Synopsis

- type family Sing :: k -> Type
- data SIdentity :: forall a. Identity a -> Type where
  - SIdentity :: forall a (n :: a). {..} -> SIdentity ('Identity n)
- type family RunIdentity (a :: Identity (a :: Type)) :: a where ...
- data IdentitySym0 :: forall (a6989586621679082654 :: Type). (~>) a6989586621679082654 (Identity (a6989586621679082654 :: Type))
- type IdentitySym1 (t6989586621679311417 :: a6989586621679082654) = 'Identity t6989586621679311417
- data RunIdentitySym0 :: forall (a6989586621679082654 :: Type). (~>) (Identity (a6989586621679082654 :: Type)) a6989586621679082654
- type RunIdentitySym1 (a6989586621679311414 :: Identity (a6989586621679082654 :: Type)) = RunIdentity a6989586621679311414

# The `Identity` singleton

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 SIdentity :: forall a. Identity a -> Type where Source #

Constructors

SIdentity |

Fields

- :: forall a (n :: a). { sRunIdentity :: (Sing (n :: a))
- } -> SIdentity ('Identity n)

#### Instances

Instances details

SDecide a => TestCoercion (SIdentity :: Identity a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testCoercion :: forall (a0 :: k) (b :: k). SIdentity a0 -> SIdentity b -> Maybe (Coercion a0 b)
SDecide a => TestEquality (SIdentity :: Identity a -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods testEquality :: forall (a0 :: k) (b :: k). SIdentity a0 -> SIdentity b -> Maybe (a0 :~: b)
ShowSing a => Show (SIdentity z) |
Instance details Defined in Data.Singletons.ShowSing Methods showsPrec :: Int -> SIdentity z -> ShowS show :: SIdentity z -> String showList :: [SIdentity z] -> ShowS

type family RunIdentity (a :: Identity (a :: Type)) :: a where ... Source #

Equations

RunIdentity ('Identity field) = field |

# Defunctionalization symbols

data IdentitySym0 :: forall (a6989586621679082654 :: Type). (~>) a6989586621679082654 (Identity (a6989586621679082654 :: Type)) Source #

#### Instances

Instances details

SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods sing :: Sing IdentitySym0 Source #
SuppressUnusedWarnings (IdentitySym0 :: TyFun a6989586621679082654 (Identity a6989586621679082654) -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (IdentitySym0 :: TyFun a (Identity a) -> Type) (t6989586621679311417 :: a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Apply (IdentitySym0 :: TyFun a (Identity a) -> Type) (t6989586621679311417 :: a) = 'Identity t6989586621679311417

type IdentitySym1 (t6989586621679311417 :: a6989586621679082654) = 'Identity t6989586621679311417 Source #

data RunIdentitySym0 :: forall (a6989586621679082654 :: Type). (~>) (Identity (a6989586621679082654 :: Type)) a6989586621679082654 Source #

#### Instances

Instances details

SuppressUnusedWarnings (RunIdentitySym0 :: TyFun (Identity a6989586621679082654) a6989586621679082654 -> Type) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances Methods suppressUnusedWarnings :: () Source #
type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679311414 :: Identity a) Source # |
Instance details Defined in Data.Singletons.Prelude.Instances type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679311414 :: Identity a) = RunIdentity a6989586621679311414

type RunIdentitySym1 (a6989586621679311414 :: Identity (a6989586621679082654 :: Type)) = RunIdentity a6989586621679311414 Source #

# Orphan instances

SMonad Identity Source # |
Instance details Methods (%>>=) :: forall a b (t :: Identity a) (t :: a ~> Identity b). Sing t -> Sing t -> Sing (Apply (Apply (>>=@#@$) t) t) Source # (%>>) :: forall a b (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (>>@#@$) t) t) Source # sReturn :: forall a (t :: a). Sing t -> Sing (Apply ReturnSym0 t) Source #
SApplicative Identity Source # |

Instance details

Methods

sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source #

(%<*>) :: forall a b (t :: Identity (a ~> b)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<*>@#@$) t) t) Source #

sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source #

(%*>) :: forall a b (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (*>@#@$) t) t) Source #

(%<*) :: forall a b (t :: Identity a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (<*@#@$) t) t) Source #

SFunctor Identity Source # |
Instance details Methods sFmap :: forall a b (t :: a ~> b) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Identity b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
PMonad Identity Source # |
Instance details Associated Types type arg >>= arg :: m b Source # type arg >> arg :: m b Source # type Return arg :: m a Source #
PApplicative Identity Source # |
Instance details Associated Types type Pure arg :: f a Source # type arg <*> arg :: f b Source # type LiftA2 arg arg arg :: f c Source # type arg *> arg :: f b Source # type arg <* arg :: f a Source #
PFunctor Identity Source # |
Instance details Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
SFoldable Identity Source # |

Instance details

Methods

sFold :: forall m (t :: Identity m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source #

sFoldMap :: forall a m (t :: a ~> m) (t :: Identity a). SMonoid m => Sing t -> Sing t -> Sing (Apply (Apply FoldMapSym0 t) t) Source #

sFoldr :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldrSym0 t) t) t) Source #

sFoldr' :: forall a b (t :: a ~> (b ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldr'Sym0 t) t) t) Source #

sFoldl :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply FoldlSym0 t) t) t) Source #

sFoldl' :: forall b a (t :: b ~> (a ~> b)) (t :: b) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply Foldl'Sym0 t) t) t) Source #

sFoldr1 :: forall a (t :: a ~> (a ~> a)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source #

sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source #

sToList :: forall a (t :: Identity a). Sing t -> Sing (Apply ToListSym0 t) Source #

sNull :: forall a (t :: Identity a). Sing t -> Sing (Apply NullSym0 t) Source #

sLength :: forall a (t :: Identity a). Sing t -> Sing (Apply LengthSym0 t) Source #

sElem :: forall a (t :: a) (t :: Identity a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source #

sMaximum :: forall a (t :: Identity a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source #

sMinimum :: forall a (t :: Identity a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source #

sSum :: forall a (t :: Identity a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source #

sProduct :: forall a (t :: Identity a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source #

PFoldable Identity Source # |

Instance details

Associated Types

type Fold arg :: m Source #

type FoldMap arg arg :: m Source #

type Foldr arg arg arg :: b Source #

type Foldr' arg arg arg :: b Source #

type Foldl arg arg arg :: b Source #

type Foldl' arg arg arg :: b Source #

type Foldr1 arg arg :: a Source #

type Foldl1 arg arg :: a Source #

type ToList arg :: [a] Source #

type Null arg :: Bool Source #

type Length arg :: Nat Source #

type Elem arg arg :: Bool Source #

type Maximum arg :: a Source #

type Minimum arg :: a Source #

type Sum arg :: a Source #

type Product arg :: a Source #

SNum a => SNum (Identity a) Source # |

Instance details

Methods

(%+) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (+@#@$) t) t) Source #

(%-) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (-@#@$) t) t) Source #

(%*) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (*@#@$) t) t) Source #

sNegate :: forall (t :: Identity a). Sing t -> Sing (Apply NegateSym0 t) Source #

sAbs :: forall (t :: Identity a). Sing t -> Sing (Apply AbsSym0 t) Source #

sSignum :: forall (t :: Identity a). Sing t -> Sing (Apply SignumSym0 t) Source #

sFromInteger :: forall (t :: Nat). Sing t -> Sing (Apply FromIntegerSym0 t) Source #

PNum (Identity a) Source # |
Instance details Associated Types type arg + arg :: a Source # type arg - arg :: a Source # type arg * arg :: a Source # type Negate arg :: a Source # type Abs arg :: a Source # type Signum arg :: a Source # type FromInteger arg :: a Source #
SEnum a => SEnum (Identity a) Source # |

Instance details

Methods

sSucc :: forall (t :: Identity a). Sing t -> Sing (Apply SuccSym0 t) Source #

sPred :: forall (t :: Identity a). Sing t -> Sing (Apply PredSym0 t) Source #

sToEnum :: forall (t :: Nat). Sing t -> Sing (Apply ToEnumSym0 t) Source #

sFromEnum :: forall (t :: Identity a). Sing t -> Sing (Apply FromEnumSym0 t) Source #

sEnumFromTo :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t) Source #

sEnumFromThenTo :: forall (t :: Identity a) (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t) Source #

PEnum (Identity a) Source # |
Instance details Associated Types type Succ arg :: a Source # type Pred arg :: a Source # type ToEnum arg :: a Source # type FromEnum arg :: Nat Source # type EnumFromTo arg arg :: [a] Source # type EnumFromThenTo arg arg arg :: [a] Source #
SSemigroup a => SSemigroup (Identity a) Source # |
Instance details Methods (%<>) :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sSconcat :: forall (t :: NonEmpty (Identity a)). Sing t -> Sing (Apply SconcatSym0 t) Source #
PSemigroup (Identity a) Source # |
Instance details Associated Types type arg <> arg :: a Source # type Sconcat arg :: a Source #
SShow a => SShow (Identity a) Source # |
Instance details Methods sShowsPrec :: forall (t :: Nat) (t :: Identity a) (t :: Symbol). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply ShowsPrecSym0 t) t) t) Source # sShow_ :: forall (t :: Identity a). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t :: [Identity a]) (t :: Symbol). Sing t -> Sing t -> Sing (Apply (Apply ShowListSym0 t) t) Source #
PShow (Identity a) Source # |
Instance details Associated Types type ShowsPrec arg arg arg :: Symbol Source # type Show_ arg :: Symbol Source # type ShowList arg arg :: Symbol Source #
SMonoid a => SMonoid (Identity a) Source # |
Instance details Methods sMempty :: Sing MemptySym0 Source # sMappend :: forall (t :: Identity a) (t :: Identity a). Sing t -> Sing t -> Sing (Apply (Apply MappendSym0 t) t) Source # sMconcat :: forall (t :: [Identity a]). Sing t -> Sing (Apply MconcatSym0 t) Source #
PMonoid (Identity a) Source # |
Instance details Associated Types type Mempty :: a Source # type Mappend arg arg :: a Source # type Mconcat arg :: a Source #