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 |
Exports the promoted and singled versions of the Identity
data type.
Synopsis
- data family Sing :: k -> Type
- type SIdentity = (Sing :: Identity a -> Type)
- type family RunIdentity (a :: Identity a) :: a where ...
- data IdentitySym0 :: forall (a6989586621679081595 :: Type). (~>) a6989586621679081595 (Identity (a6989586621679081595 :: Type))
- type IdentitySym1 (t6989586621679292147 :: a6989586621679081595) = Identity t6989586621679292147
- data RunIdentitySym0 :: forall a6989586621679081595. (~>) (Identity a6989586621679081595) a6989586621679081595
- type RunIdentitySym1 (a6989586621679292144 :: Identity a6989586621679081595) = RunIdentity a6989586621679292144
The Identity
singleton
data family Sing :: k -> Type Source #
The singleton kind-indexed data family.
Instances
SDecide k => TestCoercion (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
SDecide k => TestEquality (Sing :: k -> Type) Source # | |
Defined in Data.Singletons.Decide | |
Show (SSymbol s) Source # | |
Show (SNat n) Source # | |
Eq (Sing a) Source # | |
Ord (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
Show (Sing a) Source # | |
Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f) => Show (Sing z) Source # | |
(ShowSing a, ShowSing b, ShowSing c, ShowSing d, ShowSing e, ShowSing f, ShowSing g) => Show (Sing z) Source # | |
Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing b) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing m => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing (Maybe a) => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing Bool => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
ShowSing a => Show (Sing z) Source # | |
(ShowSing a, ShowSing [a]) => Show (Sing z) Source # | |
data Sing (a :: Bool) Source # | |
data Sing (a :: Ordering) Source # | |
data Sing (n :: Nat) Source # | |
data Sing (n :: Symbol) Source # | |
Defined in Data.Singletons.TypeLits.Internal | |
data Sing (a :: ()) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: Void) Source # | |
Defined in Data.Singletons.Prelude.Instances | |
data Sing (a :: All) Source # | |
data Sing (a :: Any) Source # | |
data Sing (a :: PErrorMessage) Source # | |
Defined in Data.Singletons.TypeError data Sing (a :: PErrorMessage) where
| |
data Sing (b :: [a]) Source # | |
data Sing (b :: Maybe a) Source # | |
data Sing (a :: TYPE rep) Source # | A choice of singleton for the kind Conceivably, one could generalize this instance to `Sing :: k -> Type` for
any kind We cannot produce explicit singleton values for everything in |
Defined in Data.Singletons.TypeRepTYPE | |
data Sing (b :: Min a) Source # | |
data Sing (b :: Max a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (a :: WrappedMonoid m) Source # | |
Defined in Data.Singletons.Prelude.Semigroup.Internal data Sing (a :: WrappedMonoid m) where
| |
data Sing (b :: Option a) Source # | |
data Sing (b :: Identity a) Source # | |
data Sing (b :: First a) Source # | |
data Sing (b :: Last a) Source # | |
data Sing (b :: Dual a) Source # | |
data Sing (b :: Sum a) Source # | |
data Sing (b :: Product a) Source # | |
data Sing (b :: Down a) Source # | |
data Sing (b :: NonEmpty a) Source # | |
data Sing (c :: Either a b) Source # | |
data Sing (c :: (a, b)) Source # | |
data Sing (c :: Arg a b) Source # | |
data Sing (f :: k1 ~> k2) Source # | |
data Sing (d :: (a, b, c)) Source # | |
data Sing (c :: Const a b) Source # | |
data Sing (e :: (a, b, c, d)) Source # | |
data Sing (f :: (a, b, c, d, e)) Source # | |
data Sing (g :: (a, b, c, d, e, f)) Source # | |
data Sing (h :: (a, b, c, d, e, f, g)) Source # | |
Defined in Data.Singletons.Prelude.Instances |
type family RunIdentity (a :: Identity a) :: a where ... Source #
RunIdentity (Identity field) = field |
Defunctionalization symbols
data IdentitySym0 :: forall (a6989586621679081595 :: Type). (~>) a6989586621679081595 (Identity (a6989586621679081595 :: Type)) Source #
Instances
SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances sing :: Sing IdentitySym0 Source # | |
SuppressUnusedWarnings (IdentitySym0 :: TyFun a6989586621679081595 (Identity a6989586621679081595) -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances suppressUnusedWarnings :: () Source # | |
type Apply (IdentitySym0 :: TyFun a (Identity a) -> Type) (t6989586621679292147 :: a) Source # | |
Defined in Data.Singletons.Prelude.Instances |
type IdentitySym1 (t6989586621679292147 :: a6989586621679081595) = Identity t6989586621679292147 Source #
data RunIdentitySym0 :: forall a6989586621679081595. (~>) (Identity a6989586621679081595) a6989586621679081595 Source #
Instances
SuppressUnusedWarnings (RunIdentitySym0 :: TyFun (Identity a6989586621679081595) a6989586621679081595 -> Type) Source # | |
Defined in Data.Singletons.Prelude.Instances suppressUnusedWarnings :: () Source # | |
type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679292144 :: Identity a) Source # | |
Defined in Data.Singletons.Prelude.Instances type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679292144 :: Identity a) = RunIdentity a6989586621679292144 |
type RunIdentitySym1 (a6989586621679292144 :: Identity a6989586621679081595) = RunIdentity a6989586621679292144 Source #