Copyright | (C) 2014 Jan Stolarek Richard Eisenberg |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Jan Stolarek (jan.stolarek@p.lodz.pl) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | GHC2021 |
Defines the promoted and singleton version of the Bounded
and Enum
type
classes.
While Prelude.Singletons re-exports the promoted and singled versions of
Enum
, it deliberately avoids re-exporting Succ
and Pred
, as these are
names are likely to clash with code that deals with unary natural numbers.
As a result, this module exists to provide Succ
and Pred
for those who
want them.
Synopsis
- class PBounded a where
- class SBounded a where
- sMinBound :: Sing (MinBoundSym0 :: a) :: Type
- sMaxBound :: Sing (MaxBoundSym0 :: a) :: Type
- class PEnum a where
- type Succ (arg :: a) :: a
- type Pred (arg :: a) :: a
- type ToEnum (arg :: Natural) :: a
- type FromEnum (arg :: a) :: Natural
- type EnumFromTo (arg :: a) (arg :: a) :: [a]
- type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a]
- class SEnum a where
- sSucc :: forall (t :: a). Sing t -> Sing (Apply SuccSym0 t :: a) :: Type
- sPred :: forall (t :: a). Sing t -> Sing (Apply PredSym0 t :: a) :: Type
- sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t :: a) :: Type
- sFromEnum :: forall (t :: a). Sing t -> Sing (Apply FromEnumSym0 t :: Natural) :: Type
- sEnumFromTo :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) :: Type
- sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) :: Type
- type family MinBoundSym0 :: a where ...
- type family MaxBoundSym0 :: a where ...
- data SuccSym0 :: (~>) a a
- type family SuccSym1 (a6989586621679630955 :: a) :: a where ...
- data PredSym0 :: (~>) a a
- type family PredSym1 (a6989586621679630958 :: a) :: a where ...
- data ToEnumSym0 :: (~>) Natural a
- type family ToEnumSym1 (a6989586621679630961 :: Natural) :: a where ...
- data FromEnumSym0 :: (~>) a Natural
- type family FromEnumSym1 (a6989586621679630964 :: a) :: Natural where ...
- data EnumFromToSym0 :: (~>) a ((~>) a [a])
- data EnumFromToSym1 (a6989586621679630968 :: a) :: (~>) a [a]
- type family EnumFromToSym2 (a6989586621679630968 :: a) (a6989586621679630969 :: a) :: [a] where ...
- data EnumFromThenToSym0 :: (~>) a ((~>) a ((~>) a [a]))
- data EnumFromThenToSym1 (a6989586621679630974 :: a) :: (~>) a ((~>) a [a])
- data EnumFromThenToSym2 (a6989586621679630974 :: a) (a6989586621679630975 :: a) :: (~>) a [a]
- type family EnumFromThenToSym3 (a6989586621679630974 :: a) (a6989586621679630975 :: a) (a6989586621679630976 :: a) :: [a] where ...
Documentation
Instances
PBounded All Source # | |
PBounded Any Source # | |
PBounded Ordering Source # | |
PBounded () Source # | |
PBounded Bool Source # | |
PBounded Char Source # | |
PBounded (Identity a) Source # | |
PBounded (First a) Source # | |
PBounded (Last a) Source # | |
PBounded (Max a) Source # | |
PBounded (Min a) Source # | |
PBounded (WrappedMonoid m) Source # | |
PBounded (Dual a) Source # | |
PBounded (Product a) Source # | |
PBounded (Sum a) Source # | |
PBounded (Proxy s) Source # | |
PBounded (a, b) Source # | |
PBounded (Const a b) Source # | |
PBounded (a, b, c) Source # | |
PBounded (a, b, c, d) Source # | |
PBounded (a, b, c, d, e) Source # | |
PBounded (a, b, c, d, e, f) Source # | |
PBounded (a, b, c, d, e, f, g) Source # | |
class SBounded a where Source #
Instances
type Succ (arg :: a) :: a Source #
type Pred (arg :: a) :: a Source #
type ToEnum (arg :: Natural) :: a Source #
type FromEnum (arg :: a) :: Natural Source #
type EnumFromTo (arg :: a) (arg :: a) :: [a] Source #
type EnumFromTo a a = Apply (Apply EnumFromTo_6989586621679631001Sym0 a) a
type EnumFromThenTo (arg :: a) (arg :: a) (arg :: a) :: [a] Source #
type EnumFromThenTo a a a = Apply (Apply (Apply EnumFromThenTo_6989586621679631013Sym0 a) a) a
Instances
PEnum Ordering Source # | |
PEnum Natural Source # | |
PEnum () Source # | |
PEnum Bool Source # | |
PEnum Char Source # | |
PEnum (Identity a) Source # | |
PEnum (First a) Source # | |
PEnum (Last a) Source # | |
PEnum (Max a) Source # | |
PEnum (Min a) Source # | |
PEnum (WrappedMonoid a) Source # | |
PEnum (Proxy s) Source # | |
PEnum (Const a b) Source # | |
sSucc :: forall (t :: a). Sing t -> Sing (Apply SuccSym0 t :: a) :: Type Source #
default sSucc :: forall (t :: a). (Apply SuccSym0 t :: a) ~ Apply Succ_6989586621679630978Sym0 t => Sing t -> Sing (Apply SuccSym0 t :: a) :: Type Source #
sPred :: forall (t :: a). Sing t -> Sing (Apply PredSym0 t :: a) :: Type Source #
default sPred :: forall (t :: a). (Apply PredSym0 t :: a) ~ Apply Pred_6989586621679630991Sym0 t => Sing t -> Sing (Apply PredSym0 t :: a) :: Type Source #
sToEnum :: forall (t :: Natural). Sing t -> Sing (Apply ToEnumSym0 t :: a) :: Type Source #
sFromEnum :: forall (t :: a). Sing t -> Sing (Apply FromEnumSym0 t :: Natural) :: Type Source #
sEnumFromTo :: forall (t :: a) (t :: a). Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) :: Type Source #
default sEnumFromTo :: forall (t :: a) (t :: a). (Apply (Apply EnumFromToSym0 t) t :: [a]) ~ Apply (Apply EnumFromTo_6989586621679631001Sym0 t) t => Sing t -> Sing t -> Sing (Apply (Apply EnumFromToSym0 t) t :: [a]) :: Type Source #
sEnumFromThenTo :: forall (t :: a) (t :: a) (t :: a). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply EnumFromThenToSym0 t) t) t :: [a]) :: Type Source #
Instances
Defunctionalization symbols
type family MinBoundSym0 :: a where ... Source #
type family MaxBoundSym0 :: a where ... Source #
data ToEnumSym0 :: (~>) Natural a Source #
Instances
SEnum a => SingI (ToEnumSym0 :: TyFun Natural a -> Type) Source # | |
Defined in Data.Singletons.Base.Enum sing :: Sing ToEnumSym0 Source # | |
SuppressUnusedWarnings (ToEnumSym0 :: TyFun Natural a -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (ToEnumSym0 :: TyFun Natural k2 -> Type) (a6989586621679630961 :: Natural) Source # | |
Defined in Data.Singletons.Base.Enum |
type family ToEnumSym1 (a6989586621679630961 :: Natural) :: a where ... Source #
ToEnumSym1 a6989586621679630961 = ToEnum a6989586621679630961 |
data FromEnumSym0 :: (~>) a Natural Source #
Instances
SEnum a => SingI (FromEnumSym0 :: TyFun a Natural -> Type) Source # | |
Defined in Data.Singletons.Base.Enum sing :: Sing FromEnumSym0 Source # | |
SuppressUnusedWarnings (FromEnumSym0 :: TyFun a Natural -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (FromEnumSym0 :: TyFun a Natural -> Type) (a6989586621679630964 :: a) Source # | |
Defined in Data.Singletons.Base.Enum |
type family FromEnumSym1 (a6989586621679630964 :: a) :: Natural where ... Source #
FromEnumSym1 a6989586621679630964 = FromEnum a6989586621679630964 |
data EnumFromToSym0 :: (~>) a ((~>) a [a]) Source #
Instances
SEnum a => SingI (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
SuppressUnusedWarnings (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) (a6989586621679630968 :: a) Source # | |
Defined in Data.Singletons.Base.Enum type Apply (EnumFromToSym0 :: TyFun a (a ~> [a]) -> Type) (a6989586621679630968 :: a) = EnumFromToSym1 a6989586621679630968 |
data EnumFromToSym1 (a6989586621679630968 :: a) :: (~>) a [a] Source #
Instances
SEnum a => SingI1 (EnumFromToSym1 :: a -> TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
(SEnum a, SingI d) => SingI (EnumFromToSym1 d :: TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum sing :: Sing (EnumFromToSym1 d) Source # | |
SuppressUnusedWarnings (EnumFromToSym1 a6989586621679630968 :: TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (EnumFromToSym1 a6989586621679630968 :: TyFun a [a] -> Type) (a6989586621679630969 :: a) Source # | |
Defined in Data.Singletons.Base.Enum type Apply (EnumFromToSym1 a6989586621679630968 :: TyFun a [a] -> Type) (a6989586621679630969 :: a) = EnumFromTo a6989586621679630968 a6989586621679630969 |
type family EnumFromToSym2 (a6989586621679630968 :: a) (a6989586621679630969 :: a) :: [a] where ... Source #
EnumFromToSym2 a6989586621679630968 a6989586621679630969 = EnumFromTo a6989586621679630968 a6989586621679630969 |
data EnumFromThenToSym0 :: (~>) a ((~>) a ((~>) a [a])) Source #
Instances
SEnum a => SingI (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
SuppressUnusedWarnings (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) (a6989586621679630974 :: a) Source # | |
Defined in Data.Singletons.Base.Enum type Apply (EnumFromThenToSym0 :: TyFun a (a ~> (a ~> [a])) -> Type) (a6989586621679630974 :: a) = EnumFromThenToSym1 a6989586621679630974 |
data EnumFromThenToSym1 (a6989586621679630974 :: a) :: (~>) a ((~>) a [a]) Source #
Instances
SEnum a => SingI1 (EnumFromThenToSym1 :: a -> TyFun a (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
(SEnum a, SingI d) => SingI (EnumFromThenToSym1 d :: TyFun a (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum sing :: Sing (EnumFromThenToSym1 d) Source # | |
SuppressUnusedWarnings (EnumFromThenToSym1 a6989586621679630974 :: TyFun a (a ~> [a]) -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (EnumFromThenToSym1 a6989586621679630974 :: TyFun a (a ~> [a]) -> Type) (a6989586621679630975 :: a) Source # | |
Defined in Data.Singletons.Base.Enum type Apply (EnumFromThenToSym1 a6989586621679630974 :: TyFun a (a ~> [a]) -> Type) (a6989586621679630975 :: a) = EnumFromThenToSym2 a6989586621679630974 a6989586621679630975 |
data EnumFromThenToSym2 (a6989586621679630974 :: a) (a6989586621679630975 :: a) :: (~>) a [a] Source #
Instances
SEnum a => SingI2 (EnumFromThenToSym2 :: a -> a -> TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
(SEnum a, SingI d) => SingI1 (EnumFromThenToSym2 d :: a -> TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum | |
(SEnum a, SingI d1, SingI d2) => SingI (EnumFromThenToSym2 d1 d2 :: TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum sing :: Sing (EnumFromThenToSym2 d1 d2) Source # | |
SuppressUnusedWarnings (EnumFromThenToSym2 a6989586621679630974 a6989586621679630975 :: TyFun a [a] -> Type) Source # | |
Defined in Data.Singletons.Base.Enum suppressUnusedWarnings :: () Source # | |
type Apply (EnumFromThenToSym2 a6989586621679630974 a6989586621679630975 :: TyFun a [a] -> Type) (a6989586621679630976 :: a) Source # | |
Defined in Data.Singletons.Base.Enum type Apply (EnumFromThenToSym2 a6989586621679630974 a6989586621679630975 :: TyFun a [a] -> Type) (a6989586621679630976 :: a) = EnumFromThenTo a6989586621679630974 a6989586621679630975 a6989586621679630976 |
type family EnumFromThenToSym3 (a6989586621679630974 :: a) (a6989586621679630975 :: a) (a6989586621679630976 :: a) :: [a] where ... Source #
EnumFromThenToSym3 a6989586621679630974 a6989586621679630975 a6989586621679630976 = EnumFromThenTo a6989586621679630974 a6989586621679630975 a6989586621679630976 |