Copyright | (C) 2021 Ryan Scott |
---|---|
License | BSD-style (see LICENSE) |
Maintainer | Richard Eisenberg (rae@cs.brynmawr.edu) |
Stability | experimental |
Portability | non-portable |
Safe Haskell | None |
Language | GHC2021 |
Exports the promoted and singled versions of the Product
data type.
The Product
singleton
type family Sing :: k -> Type #
Instances
data SProduct (a1 :: Product f g a) where Source #
SPair :: forall {k} (f :: k -> Type) (g :: k -> Type) (a :: k) (x :: f a) (y :: g a). Sing x -> Sing y -> SProduct ('Pair x y) |
Instances
(SDecide (f a), SDecide (g a)) => TestCoercion (SProduct :: Product f g a -> Type) Source # | |
Defined in Data.Functor.Product.Singletons | |
(SDecide (f a), SDecide (g a)) => TestEquality (SProduct :: Product f g a -> Type) Source # | |
Defined in Data.Functor.Product.Singletons | |
Eq (SProduct z) Source # | |
Ord (SProduct z) Source # | |
Defined in Data.Functor.Product.Singletons |
Defunctionalization symbols
data PairSym0 (z :: TyFun (f a) (g a ~> Product f g a)) Source #
data PairSym1 (fa :: f a) (z :: TyFun (g a) (Product f g a)) Source #
Orphan instances
PAlternative (Product f g :: k -> Type) Source # | |
PMonadPlus (Product f g :: k -> Type) Source # | |
SingI2 ('Pair :: f a -> g a -> Product f g a) Source # | |
SingI x => SingI1 ('Pair x :: g a -> Product f g a) Source # | |
PApplicative (Product f g) Source # | |
PFunctor (Product f g) Source # | |
PMonad (Product f g) Source # | |
(SAlternative f, SAlternative g) => SAlternative (Product f g) Source # | |
(SApplicative f, SApplicative g) => SApplicative (Product f g) Source # | |
sPure :: forall a (t :: a). Sing t -> Sing (Apply (PureSym0 :: TyFun a (Product f g a) -> Type) t) Source # (%<*>) :: forall a b (t1 :: Product f g (a ~> b)) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<*>@#@$) :: TyFun (Product f g (a ~> b)) (Product f g a ~> Product f g b) -> Type) t1) t2) Source # sLiftA2 :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: Product f g a) (t3 :: Product f g b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (LiftA2Sym0 :: TyFun (a ~> (b ~> c)) (Product f g a ~> (Product f g b ~> Product f g c)) -> Type) t1) t2) t3) Source # (%*>) :: forall a b (t1 :: Product f g a) (t2 :: Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((*>@#@$) :: TyFun (Product f g a) (Product f g b ~> Product f g b) -> Type) t1) t2) Source # (%<*) :: forall a b (t1 :: Product f g a) (t2 :: Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<*@#@$) :: TyFun (Product f g a) (Product f g b ~> Product f g a) -> Type) t1) t2) Source # | |
(SFunctor f, SFunctor g) => SFunctor (Product f g) Source # | |
sFmap :: forall a b (t1 :: a ~> b) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (FmapSym0 :: TyFun (a ~> b) (Product f g a ~> Product f g b) -> Type) t1) t2) Source # (%<$) :: forall a b (t1 :: a) (t2 :: Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<$@#@$) :: TyFun a (Product f g b ~> Product f g a) -> Type) t1) t2) Source # | |
(SMonad f, SMonad g) => SMonad (Product f g) Source # | |
(%>>=) :: forall a b (t1 :: Product f g a) (t2 :: a ~> Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>>=@#@$) :: TyFun (Product f g a) ((a ~> Product f g b) ~> Product f g b) -> Type) t1) t2) Source # (%>>) :: forall a b (t1 :: Product f g a) (t2 :: Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>>@#@$) :: TyFun (Product f g a) (Product f g b ~> Product f g b) -> Type) t1) t2) Source # sReturn :: forall a (t :: a). Sing t -> Sing (Apply (ReturnSym0 :: TyFun a (Product f g a) -> Type) t) Source # | |
(SMonadPlus f, SMonadPlus g) => SMonadPlus (Product f g) Source # | |
PMonadZip (Product f g) Source # | |
(SMonadZip f, SMonadZip g) => SMonadZip (Product f g) Source # | |
sMzip :: forall a b (t1 :: Product f g a) (t2 :: Product f g b). Sing t1 -> Sing t2 -> Sing (Apply (Apply (MzipSym0 :: TyFun (Product f g a) (Product f g b ~> Product f g (a, b)) -> Type) t1) t2) Source # sMzipWith :: forall a b c (t1 :: a ~> (b ~> c)) (t2 :: Product f g a) (t3 :: Product f g b). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (MzipWithSym0 :: TyFun (a ~> (b ~> c)) (Product f g a ~> (Product f g b ~> Product f g c)) -> Type) t1) t2) t3) Source # sMunzip :: forall a b (t :: Product f g (a, b)). Sing t -> Sing (Apply (MunzipSym0 :: TyFun (Product f g (a, b)) (Product f g a, Product f g b) -> Type) t) Source # | |
PFoldable (Product f g) Source # | |
(SFoldable f, SFoldable g) => SFoldable (Product f g) Source # | |
sFold :: forall m (t1 :: Product f g m). SMonoid m => Sing t1 -> Sing (Apply (FoldSym0 :: TyFun (Product f g m) m -> Type) t1) Source # sFoldMap :: forall a m (t1 :: a ~> m) (t2 :: Product f g a). SMonoid m => Sing t1 -> Sing t2 -> Sing (Apply (Apply (FoldMapSym0 :: TyFun (a ~> m) (Product f g a ~> m) -> Type) t1) t2) Source # sFoldr :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Product f g a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (FoldrSym0 :: TyFun (a ~> (b ~> b)) (b ~> (Product f g a ~> b)) -> Type) t1) t2) t3) Source # sFoldr' :: forall a b (t1 :: a ~> (b ~> b)) (t2 :: b) (t3 :: Product f g a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Foldr'Sym0 :: TyFun (a ~> (b ~> b)) (b ~> (Product f g a ~> b)) -> Type) t1) t2) t3) Source # sFoldl :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Product f g a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (FoldlSym0 :: TyFun (b ~> (a ~> b)) (b ~> (Product f g a ~> b)) -> Type) t1) t2) t3) Source # sFoldl' :: forall b a (t1 :: b ~> (a ~> b)) (t2 :: b) (t3 :: Product f g a). Sing t1 -> Sing t2 -> Sing t3 -> Sing (Apply (Apply (Apply (Foldl'Sym0 :: TyFun (b ~> (a ~> b)) (b ~> (Product f g a ~> b)) -> Type) t1) t2) t3) Source # sFoldr1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (Foldr1Sym0 :: TyFun (a ~> (a ~> a)) (Product f g a ~> a) -> Type) t1) t2) Source # sFoldl1 :: forall a (t1 :: a ~> (a ~> a)) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (Foldl1Sym0 :: TyFun (a ~> (a ~> a)) (Product f g a ~> a) -> Type) t1) t2) Source # sToList :: forall a (t1 :: Product f g a). Sing t1 -> Sing (Apply (ToListSym0 :: TyFun (Product f g a) [a] -> Type) t1) Source # sNull :: forall a (t1 :: Product f g a). Sing t1 -> Sing (Apply (NullSym0 :: TyFun (Product f g a) Bool -> Type) t1) Source # sLength :: forall a (t1 :: Product f g a). Sing t1 -> Sing (Apply (LengthSym0 :: TyFun (Product f g a) Natural -> Type) t1) Source # sElem :: forall a (t1 :: a) (t2 :: Product f g a). SEq a => Sing t1 -> Sing t2 -> Sing (Apply (Apply (ElemSym0 :: TyFun a (Product f g a ~> Bool) -> Type) t1) t2) Source # sMaximum :: forall a (t1 :: Product f g a). SOrd a => Sing t1 -> Sing (Apply (MaximumSym0 :: TyFun (Product f g a) a -> Type) t1) Source # sMinimum :: forall a (t1 :: Product f g a). SOrd a => Sing t1 -> Sing (Apply (MinimumSym0 :: TyFun (Product f g a) a -> Type) t1) Source # sSum :: forall a (t1 :: Product f g a). SNum a => Sing t1 -> Sing (Apply (SumSym0 :: TyFun (Product f g a) a -> Type) t1) Source # sProduct :: forall a (t1 :: Product f g a). SNum a => Sing t1 -> Sing (Apply (ProductSym0 :: TyFun (Product f g a) a -> Type) t1) Source # | |
PTraversable (Product f g) Source # | |
(STraversable f, STraversable g) => STraversable (Product f g) Source # | |
sTraverse :: forall a (f0 :: Type -> Type) b (t1 :: a ~> f0 b) (t2 :: Product f g a). SApplicative f0 => Sing t1 -> Sing t2 -> Sing (Apply (Apply (TraverseSym0 :: TyFun (a ~> f b) (Product f g a ~> f (Product f g b)) -> Type) t1) t2) Source # sSequenceA :: forall (f0 :: Type -> Type) a (t1 :: Product f g (f0 a)). SApplicative f0 => Sing t1 -> Sing (Apply (SequenceASym0 :: TyFun (Product f g (f a)) (f (Product f g a)) -> Type) t1) Source # sMapM :: forall a (m :: Type -> Type) b (t1 :: a ~> m b) (t2 :: Product f g a). SMonad m => Sing t1 -> Sing t2 -> Sing (Apply (Apply (MapMSym0 :: TyFun (a ~> m b) (Product f g a ~> m (Product f g b)) -> Type) t1) t2) Source # sSequence :: forall (m :: Type -> Type) a (t1 :: Product f g (m a)). SMonad m => Sing t1 -> Sing (Apply (SequenceSym0 :: TyFun (Product f g (m a)) (m (Product f g a)) -> Type) t1) Source # | |
(SDecide (f a), SDecide (g a)) => SDecide (Product f g a) Source # | |
PEq (Product f g a) Source # | |
(SEq (f a), SEq (g a)) => SEq (Product f g a) Source # | |
(%==) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((==@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # (%/=) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((/=@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # | |
POrd (Product f g a) Source # | |
(SOrd (f a), SOrd (g a)) => SOrd (Product f g a) Source # | |
sCompare :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (CompareSym0 :: TyFun (Product f g a) (Product f g a ~> Ordering) -> Type) t1) t2) Source # (%<) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # (%<=) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((<=@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # (%>) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # (%>=) :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply ((>=@#@$) :: TyFun (Product f g a) (Product f g a ~> Bool) -> Type) t1) t2) Source # sMax :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (MaxSym0 :: TyFun (Product f g a) (Product f g a ~> Product f g a) -> Type) t1) t2) Source # sMin :: forall (t1 :: Product f g a) (t2 :: Product f g a). Sing t1 -> Sing t2 -> Sing (Apply (Apply (MinSym0 :: TyFun (Product f g a) (Product f g a ~> Product f g a) -> Type) t1) t2) Source # | |
(SingI x, SingI y) => SingI ('Pair x y :: Product f g a) Source # | |