Copyright | (C) 2018 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Exports the promoted and singled versions of the Identity
data type.
Synopsis
- type family Sing :: k -> Type
- data SIdentity :: forall (a :: Type). Identity a -> Type where
- type family RunIdentity (a :: Identity (a :: Type)) :: a where ...
- sRunIdentity :: forall (a :: Type) (t :: Identity (a :: Type)). Sing t -> Sing (Apply RunIdentitySym0 t :: a)
- data IdentitySym0 :: (~>) a (Identity (a :: Type))
- type family IdentitySym1 (a6989586621679052461 :: a) :: Identity (a :: Type) where ...
- data RunIdentitySym0 :: (~>) (Identity (a :: Type)) a
- type family RunIdentitySym1 (a6989586621679052464 :: Identity (a :: Type)) :: a where ...
The Identity
singleton
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SIdentity :: forall (a :: Type). Identity a -> Type where Source #
SIdentity :: forall (a :: Type) (n :: a). (Sing n) -> SIdentity ('Identity n :: Identity (a :: Type)) |
type family RunIdentity (a :: Identity (a :: Type)) :: a where ... Source #
RunIdentity ('Identity field) = field |
sRunIdentity :: forall (a :: Type) (t :: Identity (a :: Type)). Sing t -> Sing (Apply RunIdentitySym0 t :: a) Source #
Defunctionalization symbols
data IdentitySym0 :: (~>) a (Identity (a :: Type)) Source #
Instances
SingI (IdentitySym0 :: TyFun a (Identity a) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances sing :: Sing IdentitySym0 Source # | |
SuppressUnusedWarnings (IdentitySym0 :: TyFun a (Identity a) -> Type) Source # | |
Defined in Data.Singletons.Base.Instances suppressUnusedWarnings :: () Source # | |
type Apply (IdentitySym0 :: TyFun a (Identity a) -> Type) (a6989586621679052461 :: a) Source # | |
Defined in Data.Singletons.Base.Instances |
type family IdentitySym1 (a6989586621679052461 :: a) :: Identity (a :: Type) where ... Source #
IdentitySym1 a6989586621679052461 = 'Identity a6989586621679052461 |
data RunIdentitySym0 :: (~>) (Identity (a :: Type)) a Source #
Instances
SingI (RunIdentitySym0 :: TyFun (Identity a) a -> Type) Source # | |
Defined in Data.Singletons.Base.Instances | |
SuppressUnusedWarnings (RunIdentitySym0 :: TyFun (Identity a) a -> Type) Source # | |
Defined in Data.Singletons.Base.Instances suppressUnusedWarnings :: () Source # | |
type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679052464 :: Identity a) Source # | |
Defined in Data.Singletons.Base.Instances type Apply (RunIdentitySym0 :: TyFun (Identity a) a -> Type) (a6989586621679052464 :: Identity a) = RunIdentity a6989586621679052464 |
type family RunIdentitySym1 (a6989586621679052464 :: Identity (a :: Type)) :: a where ... Source #
RunIdentitySym1 a6989586621679052464 = RunIdentity a6989586621679052464 |