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

Data.Functor.Product.Singletons

Contents

The Product singleton
Defunctionalization symbols
Orphan instances

Description

Exports the promoted and singled versions of the Product data type.

Synopsis

type family Sing :: k -> Type
data SProduct :: Product f g a -> Type where
- SPair :: forall f g a (x :: f a) (y :: g a). Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)
data PairSym0 z
data PairSym1 fa z
type family PairSym2 x y where ...

The `Product` singleton

type family Sing :: k -> Type #

Instances

Instances details

type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAll
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SAny
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SVoid
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SOrdering
type Sing Source #
Instance details Defined in Data.Singletons.Base.TypeError type Sing = SErrorMessage
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SNat
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple0
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SBool
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SChar
type Sing Source #
Instance details Defined in GHC.TypeLits.Singletons.Internal type Sing = SSymbol
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SIdentity :: Identity a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Monoid.Singletons type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Ord.Singletons type Sing = SDown :: Down a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SFirst :: First a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SLast :: Last a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMax :: Max a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SMin :: Min a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SWrappedMonoid :: WrappedMonoid m -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SDual :: Dual a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SProduct :: Product a -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons.Internal type Sing = SSum :: Sum a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SNonEmpty :: NonEmpty a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.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.Base.TypeRepTYPE type Sing = TypeRep :: TYPE rep -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SList :: [a] -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = SEither :: Either a b -> Type
type Sing Source #
Instance details Defined in Data.Proxy.Singletons type Sing = SProxy :: Proxy t -> Type
type Sing Source #
Instance details Defined in Data.Semigroup.Singletons type Sing = SArg :: Arg a b -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SWrappedSing :: WrappedSing a -> Type
type Sing
Instance details Defined in Data.Singletons type Sing = SLambda :: (k1 ~> k2) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple2 :: (a, b) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Const.Singletons type Sing = SConst :: Const a b -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple3 :: (a, b, c) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Product.Singletons type Sing = SProduct :: Product f g a -> Type
type Sing Source #
Instance details Defined in Data.Functor.Sum.Singletons type Sing = SSum :: Sum f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple4 :: (a, b, c, d) -> Type
type Sing Source #
Instance details Defined in Data.Functor.Compose.Singletons type Sing = SCompose :: Compose f g a -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple5 :: (a, b, c, d, e) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple6 :: (a, b, c, d, e, f) -> Type
type Sing Source #
Instance details Defined in Data.Singletons.Base.Instances type Sing = STuple7 :: (a, b, c, d, e, f, g) -> Type

data SProduct :: Product f g a -> Type where Source #

Constructors

SPair :: forall f g a (x :: f a) (y :: g a). Sing x -> Sing y -> SProduct ('Pair @f @g @a x y)

Defunctionalization symbols

data PairSym0 z Source #

Instances

Instances details

SingI (PairSym0 :: TyFun (f a) (g a ~> Product f g a) -> Type) Source #
Instance details Defined in Data.Functor.Product.Singletons Methods sing :: Sing PairSym0
type Apply (PairSym0 :: TyFun (f a) (g a ~> Product f g a) -> Type) (x :: f a) Source #
Instance details Defined in Data.Functor.Product.Singletons type Apply (PairSym0 :: TyFun (f a) (g a ~> Product f g a) -> Type) (x :: f a) = PairSym1 x :: TyFun (g a) (Product f g a) -> Type

data PairSym1 fa z Source #

Instances

Instances details

SingI1 (PairSym1 :: f a -> TyFun (g a) (Product f g a) -> Type) Source #
Instance details Defined in Data.Functor.Product.Singletons Methods liftSing :: forall (x :: k1). Sing x -> Sing (PairSym1 x)
SingI x => SingI (PairSym1 x :: TyFun (g a) (Product f g a) -> Type) Source #
Instance details Defined in Data.Functor.Product.Singletons Methods sing :: Sing (PairSym1 x)
type Apply (PairSym1 x :: TyFun (g a) (Product f g a) -> Type) (y :: g a) Source #
Instance details Defined in Data.Functor.Product.Singletons type Apply (PairSym1 x :: TyFun (g a) (Product f g a) -> Type) (y :: g a) = 'Pair x y

type family PairSym2 x y where ... Source #

Equations

PairSym2 x y = 'Pair x y

Orphan instances

PAlternative (Product f g :: k -> Type) Source #
Instance details Associated Types type Empty :: f a Source # type arg <\|> arg :: f a Source #
PMonadPlus (Product f g :: k -> Type) Source #
Instance details Associated Types type Mzero :: m a Source # type Mplus arg arg :: m a Source #
SingI2 ('Pair :: f a -> g a -> Product f g a) Source #
Instance details Methods liftSing2 :: forall (x :: k1) (y :: k2). Sing x -> Sing y -> Sing ('Pair x y)
SingI x => SingI1 ('Pair x :: g a -> Product f g a) Source #
Instance details Methods liftSing :: forall (x0 :: k1). Sing x0 -> Sing ('Pair x x0)
PApplicative (Product f g) 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 (Product f g) Source #
Instance details Associated Types type Fmap arg arg :: f b Source # type arg <$ arg :: f a Source #
PMonad (Product f g) Source #
Instance details Associated Types type arg >>= arg :: m b Source # type arg >> arg :: m b Source # type Return arg :: m a Source #
(SAlternative f, SAlternative g) => SAlternative (Product f g) Source #
Instance details Methods sEmpty :: Sing EmptySym0 Source # (%<\|>) :: forall a (t :: Product f g a) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply (<\|>@#@$) t) t) Source #
(SApplicative f, SApplicative g) => SApplicative (Product f g) Source #
Instance details Methods sPure :: forall a (t :: a). Sing t -> Sing (Apply PureSym0 t) Source # (%<>) :: forall a b (t :: Product f g (a ~> b)) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply (<>@#@$) t) t) Source # sLiftA2 :: forall a b c (t :: a ~> (b ~> c)) (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply LiftA2Sym0 t) t) t) Source # (%>) :: forall a b (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (>@#@$) t) t) Source # (%<) :: forall a b (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (<@#@$) t) t) Source #
(SFunctor f, SFunctor g) => SFunctor (Product f g) Source #
Instance details Methods sFmap :: forall a b (t :: a ~> b) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply FmapSym0 t) t) Source # (%<$) :: forall a b (t :: a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (<$@#@$) t) t) Source #
(SMonad f, SMonad g) => SMonad (Product f g) Source #
Instance details Methods (%>>=) :: forall a b (t :: Product f g a) (t :: a ~> Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (>>=@#@$) t) t) Source # (%>>) :: forall a b (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply (>>@#@$) t) t) Source # sReturn :: forall a (t :: a). Sing t -> Sing (Apply ReturnSym0 t) Source #
(SMonadPlus f, SMonadPlus g) => SMonadPlus (Product f g) Source #
Instance details Methods sMzero :: Sing MzeroSym0 Source # sMplus :: forall a (t :: Product f g a) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply MplusSym0 t) t) Source #
PMonadZip (Product f g) Source #
Instance details Associated Types type Mzip arg arg :: m (a, b) Source # type MzipWith arg arg arg :: m c Source # type Munzip arg :: (m a, m b) Source #
(SMonadZip f, SMonadZip g) => SMonadZip (Product f g) Source #
Instance details Methods sMzip :: forall a b (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing (Apply (Apply MzipSym0 t) t) Source # sMzipWith :: forall a b c (t :: a ~> (b ~> c)) (t :: Product f g a) (t :: Product f g b). Sing t -> Sing t -> Sing t -> Sing (Apply (Apply (Apply MzipWithSym0 t) t) t) Source # sMunzip :: forall a b (t :: Product f g (a, b)). Sing t -> Sing (Apply MunzipSym0 t) Source #
PFoldable (Product f g) 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 :: Natural 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 #
(SFoldable f, SFoldable g) => SFoldable (Product f g) Source #
Instance details Methods sFold :: forall m (t :: Product f g m). SMonoid m => Sing t -> Sing (Apply FoldSym0 t) Source # sFoldMap :: forall a m (t :: a ~> m) (t :: Product f g 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 :: Product f g 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 :: Product f g 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 :: Product f g 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 :: Product f g 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 :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply Foldr1Sym0 t) t) Source # sFoldl1 :: forall a (t :: a ~> (a ~> a)) (t :: Product f g a). Sing t -> Sing t -> Sing (Apply (Apply Foldl1Sym0 t) t) Source # sToList :: forall a (t :: Product f g a). Sing t -> Sing (Apply ToListSym0 t) Source # sNull :: forall a (t :: Product f g a). Sing t -> Sing (Apply NullSym0 t) Source # sLength :: forall a (t :: Product f g a). Sing t -> Sing (Apply LengthSym0 t) Source # sElem :: forall a (t :: a) (t :: Product f g a). SEq a => Sing t -> Sing t -> Sing (Apply (Apply ElemSym0 t) t) Source # sMaximum :: forall a (t :: Product f g a). SOrd a => Sing t -> Sing (Apply MaximumSym0 t) Source # sMinimum :: forall a (t :: Product f g a). SOrd a => Sing t -> Sing (Apply MinimumSym0 t) Source # sSum :: forall a (t :: Product f g a). SNum a => Sing t -> Sing (Apply SumSym0 t) Source # sProduct :: forall a (t :: Product f g a). SNum a => Sing t -> Sing (Apply ProductSym0 t) Source #
PTraversable (Product f g) Source #
Instance details Associated Types type Traverse arg arg :: f (t b) Source # type SequenceA arg :: f (t a) Source # type MapM arg arg :: m (t b) Source # type Sequence arg :: m (t a) Source #
(STraversable f, STraversable g) => STraversable (Product f g) Source #
Instance details Methods sTraverse :: forall a (f0 :: Type -> Type) b (t :: a ~> f0 b) (t :: Product f g a). SApplicative f0 => Sing t -> Sing t -> Sing (Apply (Apply TraverseSym0 t) t) Source # sSequenceA :: forall (f0 :: Type -> Type) a (t :: Product f g (f0 a)). SApplicative f0 => Sing t -> Sing (Apply SequenceASym0 t) Source # sMapM :: forall a (m :: Type -> Type) b (t :: a ~> m b) (t :: Product f g a). SMonad m => Sing t -> Sing t -> Sing (Apply (Apply MapMSym0 t) t) Source # sSequence :: forall (m :: Type -> Type) a (t :: Product f g (m a)). SMonad m => Sing t -> Sing (Apply SequenceSym0 t) Source #
(SingI x, SingI y) => SingI ('Pair x y :: Product f g a) Source #
Instance details Methods sing :: Sing ('Pair x y)

The Product singleton

Instances

Defunctionalization symbols

Instances

Instances

Orphan instances

The `Product` singleton