Copyright | (c) Justin Le 2018 |
---|---|
License | BSD3 |
Maintainer | justin@jle.im |
Stability | experimental |
Portability | non-portable |
Safe Haskell | Safe-Inferred |
Language | Haskell2010 |
Synopsis
- class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where
- type Elem f = (i :: f k -> k -> Type) | i -> f
- type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f
- singProd :: Sing as -> Prod f Sing as
- prodSing :: Prod f Sing as -> Sing as
- withIndices :: Prod f g as -> Prod f (Elem f as :*: g) as
- traverseProd :: forall g h as m. Applicative m => (forall a. g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
- zipWithProd :: (forall a. g a -> h a -> j a) -> Prod f g as -> Prod f h as -> Prod f j as
- htraverse :: Applicative m => Sing ff -> (forall a. g a -> m (h (ff @@ a))) -> Prod f g as -> m (Prod f h (Fmap ff as))
- ixProd :: Elem f as a -> Lens' (Prod f g as) (g a)
- toRec :: Prod f g as -> Rec g (ToList as)
- withPureProd :: Prod f g as -> (PureProd f as => r) -> r
- type Shape f = Prod f Proxy :: f k -> Type
- class PureProd f as where
- pureShape :: PureProd f as => Shape f as
- class PureProdC f c as where
- class ReifyConstraintProd f c g as where
- reifyConstraintProd :: Prod f g as -> Prod f (Dict c :. g) as
- type AllConstrainedProd c as = AllConstrained c (ToList as)
- indexProd :: FProd f => Elem f as a -> Prod f g as -> g a
- mapProd :: FProd f => (forall a. g a -> h a) -> Prod f g as -> Prod f h as
- foldMapProd :: (FProd f, Monoid m) => (forall a. g a -> m) -> Prod f g as -> m
- hmap :: FProd f => Sing ff -> (forall a. g a -> h (ff @@ a)) -> Prod f g as -> Prod f h (Fmap ff as)
- zipProd :: FProd f => Prod f g as -> Prod f h as -> Prod f (g :*: h) as
- imapProd :: FProd f => (forall a. Elem f as a -> g a -> h a) -> Prod f g as -> Prod f h as
- itraverseProd :: (FProd f, Applicative m) => (forall a. Elem f as a -> g a -> m (h a)) -> Prod f g as -> m (Prod f h as)
- ifoldMapProd :: (FProd f, Monoid m) => (forall a. Elem f as a -> g a -> m) -> Prod f g as -> m
- generateProd :: (FProd f, PureProd f as) => (forall a. Elem f as a -> g a) -> Prod f g as
- generateProdA :: (FProd f, PureProd f as, Applicative m) => (forall a. Elem f as a -> m (g a)) -> m (Prod f g as)
- selectProd :: FProd f => Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs
- indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as
- eqProd :: (FProd f, ReifyConstraintProd f Eq g as) => Prod f g as -> Prod f g as -> Bool
- compareProd :: (FProd f, ReifyConstraintProd f Ord g as) => Prod f g as -> Prod f g as -> Ordering
- indexSing :: forall f as a. FProd f => Elem f as a -> Sing as -> Sing a
- singShape :: FProd f => Sing as -> Shape f as
- foldMapSing :: forall f k (as :: f k) m. (FProd f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m
- ifoldMapSing :: forall f k (as :: f k) m. (FProd f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m
- data Rec (a :: u -> Type) (b :: [u]) where
- data Index :: [k] -> k -> Type where
- withPureProdList :: Rec f as -> ((RecApplicative as, PureProd List as) => r) -> r
- data PMaybe :: (k -> Type) -> Maybe k -> Type where
- data IJust :: Maybe k -> k -> Type where
- data PEither :: (k -> Type) -> Either j k -> Type where
- data IRight :: Either j k -> k -> Type where
- data NERec :: (k -> Type) -> NonEmpty k -> Type where
- data NEIndex :: NonEmpty k -> k -> Type where
- withPureProdNE :: f a -> Rec f as -> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r) -> r
- data PTup :: (k -> Type) -> (j, k) -> Type where
- data ISnd :: (j, k) -> k -> Type where
- data PIdentity :: (k -> Type) -> Identity k -> Type where
- data IIdentity :: Identity k -> k -> Type where
- sameIndexVal :: Index as a -> Index as b -> Maybe (a :~: b)
- sameNEIndexVal :: NEIndex as a -> NEIndex as b -> Maybe (a :~: b)
- rElemIndex :: forall r rs i. (RElem r rs i, PureProd List rs) => Index rs r
- indexRElem :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as) => Index as a -> (RElem a as (RIndex a as) => r) -> r
- toCoRec :: forall k (as :: [k]) a f. (RecApplicative as, FoldRec as as) => Index as a -> f a -> CoRec f as
- data SIndex (as :: [k]) (a :: k) :: Index as a -> Type where
- data SIJust (as :: Maybe k) (a :: k) :: IJust as a -> Type where
- data SIRight (as :: Either j k) (a :: k) :: IRight as a -> Type where
- data SNEIndex (as :: NonEmpty k) (a :: k) :: NEIndex as a -> Type where
- data SISnd (as :: (j, k)) (a :: k) :: ISnd as a -> Type where
- data SIIdentity (as :: Identity k) (a :: k) :: IIdentity as a -> Type where
- SIId :: SIIdentity ('Identity a) a 'IId
- data ElemSym0 (f :: Type -> Type) :: f k ~> (k ~> Type)
- data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type
- type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a
- data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> (f k ~> Type)
- data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type
- type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as
Classes
class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where Source #
Unify different functor products over a Foldable f
.
type Elem f = (i :: f k -> k -> Type) | i -> f Source #
type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f Source #
singProd :: Sing as -> Prod f Sing as Source #
You can convert a singleton of a foldable value into a foldable product of
singletons. This essentially "breaks up" the singleton into its
individual items. Should be an inverse with prodSing
.
prodSing :: Prod f Sing as -> Sing as Source #
Collect a collection of singletons back into a single singleton.
Should be an inverse with singProd
.
withIndices :: Prod f g as -> Prod f (Elem f as :*: g) as Source #
Pair up each item in a foldable product with its index.
traverseProd :: forall g h as m. Applicative m => (forall a. g a -> m (h a)) -> Prod f g as -> m (Prod f h as) Source #
Traverse a foldable functor product with a RankN applicative function, mapping over each value and sequencing the effects.
This is the generalization of rtraverse
.
zipWithProd :: (forall a. g a -> h a -> j a) -> Prod f g as -> Prod f h as -> Prod f j as Source #
Zip together two foldable functor products with a Rank-N function.
htraverse :: Applicative m => Sing ff -> (forall a. g a -> m (h (ff @@ a))) -> Prod f g as -> m (Prod f h (Fmap ff as)) Source #
Traverse a foldable functor product with a type-changing function.
ixProd :: Elem f as a -> Lens' (Prod f g as) (g a) Source #
toRec :: Prod f g as -> Rec g (ToList as) Source #
Fold a functor product into a Rec
.
withPureProd :: Prod f g as -> (PureProd f as => r) -> r Source #
Get a PureProd
instance from a foldable functor product
providing its shape.
Instances
FProd Identity Source # | |
Defined in Data.Type.Functor.Product type Elem Identity = (i :: f k -> k -> Type) Source # type Prod Identity = (p :: (k -> Type) -> f k -> Type) Source # singProd :: forall {k} (as :: Identity k). Sing as -> Prod Identity Sing as Source # prodSing :: forall {k} (as :: Identity k). Prod Identity Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: Identity k). Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as Source # traverseProd :: forall {k} g h (as :: Identity k) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod Identity g as -> m (Prod Identity h as) Source # zipWithProd :: forall {k} g h j (as :: Identity k). (forall (a :: k). g a -> h a -> j a) -> Prod Identity g as -> Prod Identity h as -> Prod Identity j as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: Identity a). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod Identity g as -> m (Prod Identity h (Fmap ff as)) Source # ixProd :: forall {k} (as :: Identity k) (a :: k) (g :: k -> Type). Elem Identity as a -> Lens' (Prod Identity g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: Identity a). Prod Identity g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: Identity k) r. Prod Identity g as -> (PureProd Identity as => r) -> r Source # | |
FProd NonEmpty Source # | |
Defined in Data.Type.Functor.Product type Elem NonEmpty = (i :: f k -> k -> Type) Source # type Prod NonEmpty = (p :: (k -> Type) -> f k -> Type) Source # singProd :: forall {k} (as :: NonEmpty k). Sing as -> Prod NonEmpty Sing as Source # prodSing :: forall {k} (as :: NonEmpty k). Prod NonEmpty Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: NonEmpty k). Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as Source # traverseProd :: forall {k} g h (as :: NonEmpty k) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod NonEmpty g as -> m (Prod NonEmpty h as) Source # zipWithProd :: forall {k} g h j (as :: NonEmpty k). (forall (a :: k). g a -> h a -> j a) -> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: NonEmpty a). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod NonEmpty g as -> m (Prod NonEmpty h (Fmap ff as)) Source # ixProd :: forall {k} (as :: NonEmpty k) (a :: k) (g :: k -> Type). Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: NonEmpty a). Prod NonEmpty g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: NonEmpty k) r. Prod NonEmpty g as -> (PureProd NonEmpty as => r) -> r Source # | |
FProd Maybe Source # | |
Defined in Data.Type.Functor.Product type Elem Maybe = (i :: f k -> k -> Type) Source # type Prod Maybe = (p :: (k -> Type) -> f k -> Type) Source # singProd :: forall {k} (as :: Maybe k). Sing as -> Prod Maybe Sing as Source # prodSing :: forall {k} (as :: Maybe k). Prod Maybe Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: Maybe k). Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as Source # traverseProd :: forall {k} g h (as :: Maybe k) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod Maybe g as -> m (Prod Maybe h as) Source # zipWithProd :: forall {k} g h j (as :: Maybe k). (forall (a :: k). g a -> h a -> j a) -> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: Maybe a). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod Maybe g as -> m (Prod Maybe h (Fmap ff as)) Source # ixProd :: forall {k} (as :: Maybe k) (a :: k) (g :: k -> Type). Elem Maybe as a -> Lens' (Prod Maybe g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: Maybe a). Prod Maybe g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: Maybe k) r. Prod Maybe g as -> (PureProd Maybe as => r) -> r Source # | |
FProd List Source # | |
Defined in Data.Type.Functor.Product singProd :: forall {k} (as :: [k]). Sing as -> Prod List Sing as Source # prodSing :: forall {k} (as :: [k]). Prod List Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: [k]). Prod List g as -> Prod List (Elem List as :*: g) as Source # traverseProd :: forall {k} g h (as :: [k]) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod List g as -> m (Prod List h as) Source # zipWithProd :: forall {k} g h j (as :: [k]). (forall (a :: k). g a -> h a -> j a) -> Prod List g as -> Prod List h as -> Prod List j as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: [a]). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod List g as -> m (Prod List h (Fmap ff as)) Source # ixProd :: forall {k} (as :: [k]) (a :: k) (g :: k -> Type). Elem List as a -> Lens' (Prod List g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: [a]). Prod List g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: [k]) r. Prod List g as -> (PureProd List as => r) -> r Source # | |
FProd (Either j) Source # | |
Defined in Data.Type.Functor.Product type Elem (Either j) = (i :: f k -> k -> Type) Source # type Prod (Either j) = (p :: (k -> Type) -> f k -> Type) Source # singProd :: forall {k} (as :: Either j k). Sing as -> Prod (Either j) Sing as Source # prodSing :: forall {k} (as :: Either j k). Prod (Either j) Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: Either j k). Prod (Either j) g as -> Prod (Either j) (Elem (Either j) as :*: g) as Source # traverseProd :: forall {k} g h (as :: Either j k) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod (Either j) g as -> m (Prod (Either j) h as) Source # zipWithProd :: forall {k} g h j0 (as :: Either j k). (forall (a :: k). g a -> h a -> j0 a) -> Prod (Either j) g as -> Prod (Either j) h as -> Prod (Either j) j0 as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: Either j a). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod (Either j) g as -> m (Prod (Either j) h (Fmap ff as)) Source # ixProd :: forall {k} (as :: Either j k) (a :: k) (g :: k -> Type). Elem (Either j) as a -> Lens' (Prod (Either j) g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: Either j a). Prod (Either j) g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: Either j k) r. Prod (Either j) g as -> (PureProd (Either j) as => r) -> r Source # | |
FProd ((,) j) Source # | |
Defined in Data.Type.Functor.Product type Elem ((,) j) = (i :: f k -> k -> Type) Source # type Prod ((,) j) = (p :: (k -> Type) -> f k -> Type) Source # singProd :: forall {k} (as :: (j, k)). Sing as -> Prod ((,) j) Sing as Source # prodSing :: forall {k} (as :: (j, k)). Prod ((,) j) Sing as -> Sing as Source # withIndices :: forall {k} (g :: k -> Type) (as :: (j, k)). Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as Source # traverseProd :: forall {k} g h (as :: (j, k)) m. Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod ((,) j) g as -> m (Prod ((,) j) h as) Source # zipWithProd :: forall {k} g h j0 (as :: (j, k)). (forall (a :: k). g a -> h a -> j0 a) -> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j0 as Source # htraverse :: forall {a} {k} m (ff :: a ~> k) g h (as :: (j, a)). Applicative m => Sing ff -> (forall (a1 :: a). g a1 -> m (h (ff @@ a1))) -> Prod ((,) j) g as -> m (Prod ((,) j) h (Fmap ff as)) Source # ixProd :: forall {k} (as :: (j, k)) (a :: k) (g :: k -> Type). Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a) Source # toRec :: forall {a} (g :: a -> Type) (as :: (j, a)). Prod ((,) j) g as -> Rec g (ToList as) Source # withPureProd :: forall {k} (g :: k -> Type) (as :: (j, k)) r. Prod ((,) j) g as -> (PureProd ((,) j) as => r) -> r Source # |
class PureProd f as where Source #
Create
if you can give a Prod
fg a
for every slot.
Instances
RecApplicative as => PureProd List (as :: [k]) Source # | |
PureProd Maybe ('Nothing :: Maybe k) Source # | |
PureProd Identity ('Identity a :: Identity k) Source # | |
PureProd Maybe ('Just a :: Maybe k) Source # | |
RecApplicative as => PureProd NonEmpty (a ':| as :: NonEmpty k) Source # | |
SingI e => PureProd (Either j) ('Left e :: Either j k) Source # | |
PureProd (Either j) ('Right a :: Either j k) Source # | |
SingI w => PureProd ((,) j) ('(w, a) :: (j, k)) Source # | |
class PureProdC f c as where Source #
Create
if you can give a Prod
fg a
for every slot, given some
constraint.
Instances
RPureConstrained c as => PureProdC List (c :: k -> Constraint) (as :: [k]) Source # | |
PureProdC Maybe (c :: k -> Constraint) ('Nothing :: Maybe k) Source # | |
c a2 => PureProdC Identity (c :: a1 -> Constraint) ('Identity a2 :: Identity a1) Source # | |
c a2 => PureProdC Maybe (c :: a1 -> Constraint) ('Just a2 :: Maybe a1) Source # | |
(c a2, RPureConstrained c as) => PureProdC NonEmpty (c :: a1 -> Constraint) (a2 ':| as :: NonEmpty a1) Source # | |
c a => PureProdC (Either j) (c :: b -> Constraint) ('Right a :: Either j b) Source # | |
SingI e => PureProdC (Either j) (c :: k -> Constraint) ('Left e :: Either j k) Source # | |
(SingI w, c a) => PureProdC ((,) j) (c :: k -> Constraint) ('(w, a) :: (j, k)) Source # | |
class ReifyConstraintProd f c g as where Source #
Pair up each item in a
with a witness that Prod
ff a
satisfies
some constraint.
Instances
ReifyConstraint c f as => ReifyConstraintProd List c (f :: k -> Type) (as :: [k]) Source # | |
Defined in Data.Type.Functor.Product | |
ReifyConstraintProd Maybe c (g :: k -> Type) ('Nothing :: Maybe k) Source # | |
c (g a2) => ReifyConstraintProd Identity c (g :: a1 -> Type) ('Identity a2 :: Identity a1) Source # | |
c (g a2) => ReifyConstraintProd Maybe c (g :: a1 -> Type) ('Just a2 :: Maybe a1) Source # | |
(c (g a2), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c (g :: a1 -> Type) (a2 ':| as :: NonEmpty a1) Source # | |
c (g a) => ReifyConstraintProd (Either j) c (g :: b -> Type) ('Right a :: Either j b) Source # | |
ReifyConstraintProd (Either j) c (g :: k -> Type) ('Left e :: Either j k) Source # | |
c (g a) => ReifyConstraintProd ((,) j) c (g :: k -> Type) ('(w, a) :: (j, k)) Source # | |
Defined in Data.Type.Functor.Product |
type AllConstrainedProd c as = AllConstrained c (ToList as) Source #
A convenient wrapper over AllConstrained
that works for any
Foldable f
.
Functions
hmap :: FProd f => Sing ff -> (forall a. g a -> h (ff @@ a)) -> Prod f g as -> Prod f h (Fmap ff as) Source #
Map a type-changing function over every item in a Prod
.
zipProd :: FProd f => Prod f g as -> Prod f h as -> Prod f (g :*: h) as Source #
Zip together the values in two Prod
s.
imapProd :: FProd f => (forall a. Elem f as a -> g a -> h a) -> Prod f g as -> Prod f h as Source #
mapProd
, but with access to the index at each element.
itraverseProd :: (FProd f, Applicative m) => (forall a. Elem f as a -> g a -> m (h a)) -> Prod f g as -> m (Prod f h as) Source #
traverseProd
, but with access to the index at each element.
ifoldMapProd :: (FProd f, Monoid m) => (forall a. Elem f as a -> g a -> m) -> Prod f g as -> m Source #
foldMapProd
, but with access to the index at each element.
generateProd :: (FProd f, PureProd f as) => (forall a. Elem f as a -> g a) -> Prod f g as Source #
Construct a Prod
purely by providing a generating function for each
index.
generateProdA :: (FProd f, PureProd f as, Applicative m) => (forall a. Elem f as a -> m (g a)) -> m (Prod f g as) Source #
Construct a Prod
in an Applicative
context by providing
a generating function for each index.
indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as Source #
Generate a Prod
of indices for an as
.
compareProd :: (FProd f, ReifyConstraintProd f Ord g as) => Prod f g as -> Prod f g as -> Ordering Source #
Over singletons
Extract the item from the container witnessed by the Elem
foldMapSing :: forall f k (as :: f k) m. (FProd f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m Source #
A foldMap
over all items in a collection.
ifoldMapSing :: forall f k (as :: f k) m. (FProd f, Monoid m) => (forall a. Elem f as a -> Sing a -> m) -> Sing as -> m Source #
foldMapSing
but with access to the index.
Instances
data Rec (a :: u -> Type) (b :: [u]) where #
A record is parameterized by a universe u
, an interpretation f
and a
list of rows rs
. The labels or indices of the record are given by
inhabitants of the kind u
; the type of values at any label r :: u
is
given by its interpretation f r :: *
.
RNil :: forall {u} (a :: u -> Type). Rec a ('[] :: [u]) | |
(:&) :: forall {u} (a :: u -> Type) (r :: u) (rs :: [u]). !(a r) -> !(Rec a rs) -> Rec a (r ': rs) infixr 7 |
Instances
RecSubset (Rec :: (k -> Type) -> [k] -> Type) ('[] :: [k]) (ss :: [k]) ('[] :: [Nat]) | |
Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f '[] -> g (Rec f '[])) -> Rec f ss -> g (Rec f ss) # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f '[] # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f '[] -> Rec f ss -> Rec f ss # | |
(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> Type) -> [k] -> Type) (r ': rs :: [k]) (ss :: [k]) (i ': is) | |
Defined in Data.Vinyl.Lens type RecSubsetFCtx Rec f # rsubsetC :: forall g (f :: k0 -> Type). (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) # rcastC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs) # rreplaceC :: forall (f :: k0 -> Type). RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss # | |
RecElem (Rec :: (a -> Type) -> [a] -> Type) (r :: a) (r' :: a) (r ': rs :: [a]) (r' ': rs :: [a]) 'Z | |
Defined in Data.Vinyl.Lens type RecElemFCtx Rec f # | |
(RIndex r (s ': rs) ~ 'S i, RecElem (Rec :: (a -> Type) -> [a] -> Type) r r' rs rs' i) => RecElem (Rec :: (a -> Type) -> [a] -> Type) (r :: a) (r' :: a) (s ': rs :: [a]) (s ': rs' :: [a]) ('S i) | |
Defined in Data.Vinyl.Lens type RecElemFCtx Rec f # | |
TestCoercion f => TestCoercion (Rec f :: [u] -> Type) | |
Defined in Data.Vinyl.Core | |
TestEquality f => TestEquality (Rec f :: [u] -> Type) | |
Defined in Data.Vinyl.Core | |
(Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) | |
Defined in Data.Vinyl.Core sizeOf :: Rec f (r ': rs) -> Int # alignment :: Rec f (r ': rs) -> Int # peekElemOff :: Ptr (Rec f (r ': rs)) -> Int -> IO (Rec f (r ': rs)) # pokeElemOff :: Ptr (Rec f (r ': rs)) -> Int -> Rec f (r ': rs) -> IO () # peekByteOff :: Ptr b -> Int -> IO (Rec f (r ': rs)) # pokeByteOff :: Ptr b -> Int -> Rec f (r ': rs) -> IO () # | |
Storable (Rec f ('[] :: [u])) | |
Defined in Data.Vinyl.Core | |
(Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) | |
Monoid (Rec f ('[] :: [u])) | |
(Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs)) | |
Semigroup (Rec f ('[] :: [u])) | |
Generic (Rec f rs) => Generic (Rec f (r ': rs)) | |
Generic (Rec f ('[] :: [u])) | |
(RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs) | Records may be shown insofar as their points may be shown.
|
ReifyConstraint NFData f xs => NFData (Rec f xs) | |
Defined in Data.Vinyl.Core | |
(Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) | |
Eq (Rec f ('[] :: [u])) | |
(Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) | |
Defined in Data.Vinyl.Core compare :: Rec f (r ': rs) -> Rec f (r ': rs) -> Ordering # (<) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (<=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (>) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (>=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # max :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) # min :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs) # | |
Ord (Rec f ('[] :: [u])) | |
Defined in Data.Vinyl.Core | |
type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) | |
Defined in Data.Vinyl.Lens | |
type RecSubsetFCtx (Rec :: (k -> Type) -> [k] -> Type) (f :: k -> Type) | |
Defined in Data.Vinyl.Lens | |
type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) | |
Defined in Data.Vinyl.Lens | |
type RecElemFCtx (Rec :: (a -> Type) -> [a] -> Type) (f :: a -> Type) | |
Defined in Data.Vinyl.Lens | |
type Rep (Rec f (r ': rs)) | |
Defined in Data.Vinyl.Core type Rep (Rec f (r ': rs)) = C1 ('MetaCons ":&" ('InfixI 'RightAssociative 7) 'False) (S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'SourceStrict 'DecidedStrict) (Rec0 (f r)) :*: S1 ('MetaSel ('Nothing :: Maybe Symbol) 'NoSourceUnpackedness 'NoSourceStrictness 'DecidedLazy) (Rep (Rec f rs))) | |
type Rep (Rec f ('[] :: [u])) | |
Defined in Data.Vinyl.Core |
data Index :: [k] -> k -> Type where Source #
Witness an item in a type-level list by providing its index.
The number of IS
s correspond to the item's position in the list.
IZ
::Index
'[5,10,2] 5IS
IZ
::Index
'[5,10,2] 10IS
(IS
IZ
) ::Index
'[5,10,2] 2
Instances
Show (Index as a) Source # | |
Eq (Index as a) Source # | |
Ord (Index as a) Source # | |
SingKind (Index as a) Source # | |
SDecide (Index as a) Source # | |
SingI ('IZ :: Index (a ': as) a) Source # | |
Defined in Data.Type.Functor.Product | |
SingI i => SingI ('IS i :: Index (b ': bs) a) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (Index as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
withPureProdList :: Rec f as -> ((RecApplicative as, PureProd List as) => r) -> r Source #
A stronger version of withPureProd
for Rec
, providing
a RecApplicative
instance as well.
data PMaybe :: (k -> Type) -> Maybe k -> Type where Source #
A
contains nothing, and a PMaybe
f 'Nothing
contains an PMaybe
f ('Just a)f a
.
In practice this can be useful to write polymorphic functions/abstractions that contain an argument that can be "turned off" for different instances.
Instances
ReifyConstraintProd Maybe Show f as => Show (PMaybe f as) Source # | |
ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as) Source # | |
(ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as) Source # | |
Defined in Data.Type.Functor.Product |
data IJust :: Maybe k -> k -> Type where Source #
Instances
Read (IJust ('Just a) a) Source # | |
Show (IJust as a) Source # | |
Eq (IJust as a) Source # | |
Ord (IJust as a) Source # | |
SingKind (IJust as a) Source # | |
SDecide (IJust as a) Source # | |
SingI ('IJust :: IJust ('Just a) a) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (IJust as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
data PEither :: (k -> Type) -> Either j k -> Type where Source #
data IRight :: Either j k -> k -> Type where Source #
Instances
Read (IRight ('Right a :: Either j k) a) Source # | |
Show (IRight as a) Source # | |
Eq (IRight as a) Source # | |
Ord (IRight as a) Source # | |
Defined in Data.Type.Functor.Product | |
SingKind (IRight as a) Source # | |
SDecide (IRight as a) Source # | |
SingI ('IRight :: IRight ('Right a :: Either j k) a) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (IRight as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
data NERec :: (k -> Type) -> NonEmpty k -> Type where Source #
A non-empty version of Rec
.
Instances
(Show (f a2), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a2 ':| as)) Source # | |
(Eq (f a2), Eq (Rec f as)) => Eq (NERec f (a2 ':| as)) Source # | |
(Ord (f a2), Ord (Rec f as)) => Ord (NERec f (a2 ':| as)) Source # | |
Defined in Data.Type.Functor.Product compare :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> Ordering # (<) :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> Bool # (<=) :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> Bool # (>) :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> Bool # (>=) :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> Bool # max :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> NERec f (a2 ':| as) # min :: NERec f (a2 ':| as) -> NERec f (a2 ':| as) -> NERec f (a2 ':| as) # |
data NEIndex :: NonEmpty k -> k -> Type where Source #
Witness an item in a type-level NonEmpty
by either indicating that
it is the "head", or by providing an index in the "tail".
Instances
Show (NEIndex as a) Source # | |
Eq (NEIndex as a) Source # | |
Ord (NEIndex as a) Source # | |
Defined in Data.Type.Functor.Product | |
SingKind (NEIndex as a) Source # | |
SDecide (NEIndex as a) Source # | |
SingI ('NEHead :: NEIndex (a ':| as) a) Source # | |
Defined in Data.Type.Functor.Product | |
SingI i => SingI ('NETail i :: NEIndex (b ':| as) a) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (NEIndex as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
withPureProdNE :: f a -> Rec f as -> ((RecApplicative as, PureProd NonEmpty (a ':| as)) => r) -> r Source #
A stronger version of withPureProd
for NERec
, providing
a RecApplicative
instance as well.
data PTup :: (k -> Type) -> (j, k) -> Type where Source #
A PTup
tuples up some singleton with some value; a
contains a PTup
f '(w,
a)
and an Sing
wf a
.
This can be useful for carrying along some witness aside a functor value.
Instances
(Read (Sing w), Read (f a)) => Read (PTup f '(w, a)) Source # | |
(Show (Sing w), Show (f a)) => Show (PTup f '(w, a)) Source # | |
(Eq (Sing w), Eq (f a)) => Eq (PTup f '(w, a)) Source # | |
(Ord (Sing w), Ord (f a)) => Ord (PTup f '(w, a)) Source # | |
Defined in Data.Type.Functor.Product compare :: PTup f '(w, a) -> PTup f '(w, a) -> Ordering # (<) :: PTup f '(w, a) -> PTup f '(w, a) -> Bool # (<=) :: PTup f '(w, a) -> PTup f '(w, a) -> Bool # (>) :: PTup f '(w, a) -> PTup f '(w, a) -> Bool # (>=) :: PTup f '(w, a) -> PTup f '(w, a) -> Bool # |
data ISnd :: (j, k) -> k -> Type where Source #
Trivially witness an item in the second field of a type-level tuple.
Instances
Read (ISnd '(a, b) b) Source # | |
Show (ISnd as a) Source # | |
Eq (ISnd as a) Source # | |
Ord (ISnd as a) Source # | |
Defined in Data.Type.Functor.Product | |
SingKind (ISnd as a) Source # | |
SDecide (ISnd as a) Source # | |
SingI ('ISnd :: ISnd '(a, b) b) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (ISnd as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
data PIdentity :: (k -> Type) -> Identity k -> Type where Source #
A PIdentity
is a trivial functor product; it is simply the functor,
itself, alone.
is simply PIdentity
f (Identity
a)f a
. This
may be useful in conjunction with other combinators.
Instances
Read (f a2) => Read (PIdentity f ('Identity a2)) Source # | |
Show (f a2) => Show (PIdentity f ('Identity a2)) Source # | |
Eq (f a2) => Eq (PIdentity f ('Identity a2)) Source # | |
Ord (f a2) => Ord (PIdentity f ('Identity a2)) Source # | |
Defined in Data.Type.Functor.Product compare :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> Ordering # (<) :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> Bool # (<=) :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> Bool # (>) :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> Bool # (>=) :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> Bool # max :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) # min :: PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) -> PIdentity f ('Identity a2) # |
data IIdentity :: Identity k -> k -> Type where Source #
Trivially witness the item held in an Identity
.
Since: 0.1.3.0
Instances
Read (IIdentity ('Identity a) a) Source # | |
Show (IIdentity as a) Source # | |
Eq (IIdentity as a) Source # | |
Ord (IIdentity as a) Source # | |
Defined in Data.Type.Functor.Product compare :: IIdentity as a -> IIdentity as a -> Ordering # (<) :: IIdentity as a -> IIdentity as a -> Bool # (<=) :: IIdentity as a -> IIdentity as a -> Bool # (>) :: IIdentity as a -> IIdentity as a -> Bool # (>=) :: IIdentity as a -> IIdentity as a -> Bool # | |
SingKind (IIdentity as a) Source # | |
SDecide (IIdentity as a) Source # | |
SingI ('IId :: IIdentity ('Identity x) x) Source # | |
Defined in Data.Type.Functor.Product | |
type Demote (IIdentity as a) Source # | |
Defined in Data.Type.Functor.Product | |
type Sing Source # | |
Defined in Data.Type.Functor.Product |
sameNEIndexVal :: NEIndex as a -> NEIndex as b -> Maybe (a :~: b) Source #
Test if two indices point to the same item in a non-empty list.
We have to return a Maybe
here instead of a Decision
, because it
might be the case that the same item might be duplicated in a list.
Therefore, even if two indices are different, we cannot prove that the
values they point to are different.
Interfacing with vinyl
indexRElem :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as) => Index as a -> (RElem a as (RIndex a as) => r) -> r Source #
If we have
, we should also be able to create an item
that would require Index
as a
. Along with
RElem
a as (RIndex
as a)rElemIndex
, this essentially converts between the indexing system in
this library and the indexing system of vinyl.
toCoRec :: forall k (as :: [k]) a f. (RecApplicative as, FoldRec as as) => Index as a -> f a -> CoRec f as Source #
Singletons
data SIndex (as :: [k]) (a :: k) :: Index as a -> Type where Source #
Kind-indexed singleton for Index
.
data SIJust (as :: Maybe k) (a :: k) :: IJust as a -> Type where Source #
Kind-indexed singleton for IJust
.
data SIRight (as :: Either j k) (a :: k) :: IRight as a -> Type where Source #
Kind-indexed singleton for IRight
.
data SNEIndex (as :: NonEmpty k) (a :: k) :: NEIndex as a -> Type where Source #
Kind-indexed singleton for NEIndex
.
data SISnd (as :: (j, k)) (a :: k) :: ISnd as a -> Type where Source #
Kind-indexed singleton for ISnd
.
data SIIdentity (as :: Identity k) (a :: k) :: IIdentity as a -> Type where Source #
Kind-indexed singleton for IIdentity
.
Since: 0.1.5.0
SIId :: SIIdentity ('Identity a) a 'IId |
Instances
Show (SIIdentity as a i) Source # | |
Defined in Data.Type.Functor.Product showsPrec :: Int -> SIIdentity as a i -> ShowS # show :: SIIdentity as a i -> String # showList :: [SIIdentity as a i] -> ShowS # |