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 Const
data type.
Synopsis
- type family Sing :: k -> Type
- data SConst :: Const a b -> Type where
- type family GetConst (a :: Const a b) :: a where ...
- sGetConst :: forall (t :: Const a b). Sing t -> Sing (Apply GetConstSym0 t :: a) :: Type
- data ConstSym0 z
- type family ConstSym1 x where ...
- data GetConstSym0 :: (~>) (Const a b) a
- type family GetConstSym1 (a6989586621680716643 :: Const a b) :: a where ...
The Const
singleton
type family Sing :: k -> Type Source #
The singleton kind-indexed type family.
Instances
data SConst :: Const a b -> Type where Source #
Instances
SDecide a => TestCoercion (SConst :: Const a b -> Type) Source # | |
Defined in Data.Functor.Const.Singletons | |
SDecide a => TestEquality (SConst :: Const a b -> Type) Source # | |
Defined in Data.Functor.Const.Singletons |
Defunctionalization symbols
data GetConstSym0 :: (~>) (Const a b) a Source #
Instances
SingI (GetConstSym0 :: TyFun (Const a b) a -> Type) Source # | |
Defined in Data.Functor.Const.Singletons sing :: Sing GetConstSym0 Source # | |
SuppressUnusedWarnings (GetConstSym0 :: TyFun (Const a b) a -> Type) Source # | |
Defined in Data.Functor.Const.Singletons suppressUnusedWarnings :: () Source # | |
type Apply (GetConstSym0 :: TyFun (Const a b) a -> Type) (a6989586621680716643 :: Const a b) Source # | |
Defined in Data.Functor.Const.Singletons |
type family GetConstSym1 (a6989586621680716643 :: Const a b) :: a where ... Source #
GetConstSym1 a6989586621680716643 = GetConst a6989586621680716643 |
Orphan instances
SingI1 ('Const :: k1 -> Const k1 b) Source # | |
PApplicative (Const m :: Type -> Type) Source # | |
PFunctor (Const m :: Type -> Type) Source # | |
SMonoid m => SApplicative (Const m :: Type -> Type) Source # | |
sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<*>) :: forall a b (t1 :: Const m (a ~> b)) (t2 :: Const m a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<*>@#@$) t1) t2) Source # sLiftA2 :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: Const m a) (t3 :: Const m b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply LiftA2Sym0 t1) t2) t3) Source # (%*>) :: forall a b (t1 :: Const m a) (t2 :: Const m b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*>@#@$) t1) t2) Source # (%<*) :: forall a b (t1 :: Const m a) (t2 :: Const m b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<*@#@$) t1) t2) Source # | |
SFunctor (Const m :: Type -> Type) Source # | |
PFoldable (Const m :: Type -> Type) Source # | |
type FoldMap arg arg1 :: m Source # type Foldr arg arg1 arg2 :: b Source # type Foldr' arg arg1 arg2 :: b Source # type Foldl arg arg1 arg2 :: b Source # type Foldl' arg arg1 arg2 :: b Source # type Foldr1 arg arg1 :: a Source # type Foldl1 arg arg1 :: a Source # type ToList arg :: [a] Source # type Null arg :: Bool Source # type Length arg :: Natural Source # type Elem arg arg1 :: Bool Source # type Maximum arg :: a Source # | |
SFoldable (Const m :: Type -> Type) Source # | |
sFold :: forall m0 (t1 :: Const m m0). SMonoid m0 => Sing t1 -> Sing (Apply FoldSym0 t1) Source # sFoldMap :: forall a m0 (t1 :: a ~> m0) (t2 :: Const m a). SMonoid m0 => Sing t1 -> Sing t2 -> Sing (Apply (Apply FoldMapSym0 t1) t2) Source # sFoldr :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Const m a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply FoldrSym0 t1) t2) t3) Source # sFoldr' :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Const m a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply Foldr'Sym0 t1) t2) t3) Source # sFoldl :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Const m a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply FoldlSym0 t1) t2) t3) Source # sFoldl' :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Const m a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply Foldl'Sym0 t1) t2) t3) Source # sFoldr1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Const m a). Sing t1 -> Sing t2 -> Sing (Apply (Apply Foldr1Sym0 t1) t2) Source # sFoldl1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Const m a). Sing t1 -> Sing t2 -> Sing (Apply (Apply Foldl1Sym0 t1) t2) Source # sToList :: forall a (t1 :: Const m a). Sing t1 -> Sing (Apply ToListSym0 t1) Source # sNull :: forall a (t1 :: Const m a). Sing t1 -> Sing (Apply NullSym0 t1) Source # sLength :: forall a (t1 :: Const m a). Sing t1 -> Sing (Apply LengthSym0 t1) Source # sElem :: forall a (t1 :: a) (t2 :: Const m a). SEq a => Sing t1 -> Sing t2 -> Sing (Apply (Apply ElemSym0 t1) t2) Source # sMaximum :: forall a (t1 :: Const m a). SOrd a => Sing t1 -> Sing (Apply MaximumSym0 t1) Source # sMinimum :: forall a (t1 :: Const m a). SOrd a => Sing t1 -> Sing (Apply MinimumSym0 t1) Source # sSum :: forall a (t1 :: Const m a). SNum a => Sing t1 -> Sing (Apply SumSym0 t1) Source # sProduct :: forall a (t1 :: Const m a). SNum a => Sing t1 -> Sing (Apply ProductSym0 t1) Source # | |
SingKind a => SingKind (Const a b) Source # | |
SDecide a => SDecide (Const a b) Source # | |
PEq (Const a b) Source # | |
SEq a => SEq (Const a b) Source # | |
PMonoid (Const a b) Source # | |
SMonoid a => SMonoid (Const a b) Source # | |
POrd (Const a b) Source # | |
SOrd a => SOrd (Const a b) Source # | |
sCompare :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply CompareSym0 t1) t2) Source # (%<) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<@#@$) t1) t2) Source # (%<=) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (<=@#@$) t1) t2) Source # (%>) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>@#@$) t1) t2) Source # (%>=) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (>=@#@$) t1) t2) Source # sMax :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply MaxSym0 t1) t2) Source # sMin :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply MinSym0 t1) t2) Source # | |
PSemigroup (Const a b) Source # | |
SSemigroup a => SSemigroup (Const a b) Source # | |
PBounded (Const a b) Source # | |
PEnum (Const a b) Source # | |
SBounded a => SBounded (Const a b) Source # | |
SEnum a => SEnum (Const a b) Source # | |
sSucc :: forall (t :: Const a b). Sing t -> Sing (Apply SuccSym0 t) Source # sPred :: forall (t :: Const a b). Sing t -> Sing (Apply PredSym0 t) Source # sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t) Source # sFromEnum :: forall (t :: Const a b). Sing t -> Sing (Apply FromEnumSym0 t) Source # sEnumFromTo :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply EnumFromToSym0 t1) t2) Source # sEnumFromThenTo :: forall (t1 :: Const a b) (t2 :: Const a b) (t3 :: Const a b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t1) t2) t3) Source # | |
PNum (Const a b) Source # | |
SNum a => SNum (Const a b) Source # | |
(%+) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (+@#@$) t1) t2) Source # (%-) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (-@#@$) t1) t2) Source # (%*) :: forall (t1 :: Const a b) (t2 :: Const a b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (*@#@$) t1) t2) Source # sNegate :: forall (t :: Const a b). Sing t -> Sing (Apply NegateSym0 t) Source # sAbs :: forall (t :: Const a b). Sing t -> Sing (Apply AbsSym0 t) Source # sSignum :: forall (t :: Const a b). Sing t -> Sing (Apply SignumSym0 t) Source # sFromInteger :: forall (t :: Natural). Sing t -> Sing (Apply FromIntegerSym0 t) Source # | |
PShow (Const a b) Source # | |
SShow a => SShow (Const a b) Source # | |
sShowsPrec :: forall (t1 :: Natural) (t2 :: Const a b) (t3 :: Symbol). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply ShowsPrecSym0 t1) t2) t3) Source # sShow_ :: forall (t :: Const a b). Sing t -> Sing (Apply Show_Sym0 t) Source # sShowList :: forall (t1 :: [Const a b]) (t2 :: Symbol). Sing t1 -> Sing t2 -> Sing (Apply (Apply ShowListSym0 t1) t2) Source # | |
SingI a => SingI ('Const a :: Const a b) Source # | |