Data.Type.Functor.Product

Generalized functor products based on lifted Foldables.

For example, Rec f '[a,b,c] from vinyl contains an f a, f b, and f c.

PMaybe f ('Just a) contains an f a and PMaybe f 'Nothing contains nothing.

Also provide data types for "indexing" into each foldable.

Classes

class (PFunctor f, SFunctor f, PFoldable f, SFoldable f) => FProd (f :: Type -> Type) where

Unify different functor products over a Foldable f.

Minimal complete definition

singProd, prodSing, withIndices, htraverse, ixProd, toRec, withPureProd

Associated Types

type Elem f = (i :: f k -> k -> Type) | i -> f

type Prod f = (p :: (k -> Type) -> f k -> Type) | p -> f

Methods

singProd :: Sing as -> Prod f Sing as

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

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

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)

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

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))

Traverse a foldable functor product with a type-changing function.

ixProd :: Elem f as a -> Lens' (Prod f g as) (g a)

A Lens into an item in a foldable functor product, given its index.

This roughly generalizes rlens.

toRec :: Prod f g as -> Rec g (ToList as)

Fold a functor product into a Rec.

withPureProd :: Prod f g as -> (PureProd f as => r) -> r

Get a PureProd instance from a foldable functor product providing its shape.

Instances

FProd []

Defined in Data.Type.Functor.Product

Associated Types

type Elem [] = (i :: f k -> k -> Type)

type Prod [] = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod [] Sing as

prodSing :: Prod [] Sing as -> Sing as

withIndices :: Prod [] g as -> Prod [] (Elem [] as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod [] g as -> m (Prod [] h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j a) -> Prod [] g as -> Prod [] h as -> Prod [] j as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod [] g as -> m (Prod [] h (Fmap ff as))

ixProd :: Elem [] as a -> Lens' (Prod [] g as) (g a)

toRec :: Prod [] g as -> Rec g (ToList as)

withPureProd :: Prod [] g as -> (PureProd [] as -> r) -> r

FProd Maybe

Defined in Data.Type.Functor.Product

Associated Types

type Elem Maybe = (i :: f k -> k -> Type)

type Prod Maybe = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod Maybe Sing as

prodSing :: Prod Maybe Sing as -> Sing as

withIndices :: Prod Maybe g as -> Prod Maybe (Elem Maybe as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod Maybe g as -> m (Prod Maybe h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j a) -> Prod Maybe g as -> Prod Maybe h as -> Prod Maybe j as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod Maybe g as -> m (Prod Maybe h (Fmap ff as))

ixProd :: Elem Maybe as a -> Lens' (Prod Maybe g as) (g a)

toRec :: Prod Maybe g as -> Rec g (ToList as)

withPureProd :: Prod Maybe g as -> (PureProd Maybe as -> r) -> r

FProd Identity

Defined in Data.Type.Functor.Product

Associated Types

type Elem Identity = (i :: f k -> k -> Type)

type Prod Identity = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod Identity Sing as

prodSing :: Prod Identity Sing as -> Sing as

withIndices :: Prod Identity g as -> Prod Identity (Elem Identity as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod Identity g as -> m (Prod Identity h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j a) -> Prod Identity g as -> Prod Identity h as -> Prod Identity j as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod Identity g as -> m (Prod Identity h (Fmap ff as))

ixProd :: Elem Identity as a -> Lens' (Prod Identity g as) (g a)

toRec :: Prod Identity g as -> Rec g (ToList as)

withPureProd :: Prod Identity g as -> (PureProd Identity as -> r) -> r

FProd NonEmpty

Defined in Data.Type.Functor.Product

Associated Types

type Elem NonEmpty = (i :: f k -> k -> Type)

type Prod NonEmpty = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod NonEmpty Sing as

prodSing :: Prod NonEmpty Sing as -> Sing as

withIndices :: Prod NonEmpty g as -> Prod NonEmpty (Elem NonEmpty as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod NonEmpty g as -> m (Prod NonEmpty h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j a) -> Prod NonEmpty g as -> Prod NonEmpty h as -> Prod NonEmpty j as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod NonEmpty g as -> m (Prod NonEmpty h (Fmap ff as))

ixProd :: Elem NonEmpty as a -> Lens' (Prod NonEmpty g as) (g a)

toRec :: Prod NonEmpty g as -> Rec g (ToList as)

withPureProd :: Prod NonEmpty g as -> (PureProd NonEmpty as -> r) -> r

FProd (Either j)

Defined in Data.Type.Functor.Product

Associated Types

type Elem (Either j) = (i :: f k -> k -> Type)

type Prod (Either j) = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod (Either j) Sing as

prodSing :: Prod (Either j) Sing as -> Sing as

withIndices :: Prod (Either j) g as -> Prod (Either j) (Elem (Either j) as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod (Either j) g as -> m (Prod (Either j) h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j0 a) -> Prod (Either j) g as -> Prod (Either j) h as -> Prod (Either j) j0 as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod (Either j) g as -> m (Prod (Either j) h (Fmap ff as))

ixProd :: Elem (Either j) as a -> Lens' (Prod (Either j) g as) (g a)

toRec :: Prod (Either j) g as -> Rec g (ToList as)

withPureProd :: Prod (Either j) g as -> (PureProd (Either j) as -> r) -> r

FProd ((,) j)

Defined in Data.Type.Functor.Product

Associated Types

type Elem ((,) j) = (i :: f k -> k -> Type)

type Prod ((,) j) = (p :: (k -> Type) -> f k -> Type)

Methods

singProd :: Sing as -> Prod ((,) j) Sing as

prodSing :: Prod ((,) j) Sing as -> Sing as

withIndices :: Prod ((,) j) g as -> Prod ((,) j) (Elem ((,) j) as :*: g) as

traverseProd :: Applicative m => (forall (a :: k). g a -> m (h a)) -> Prod ((,) j) g as -> m (Prod ((,) j) h as)

zipWithProd :: (forall (a :: k). g a -> h a -> j0 a) -> Prod ((,) j) g as -> Prod ((,) j) h as -> Prod ((,) j) j0 as

htraverse :: Applicative m => Sing ff -> (forall (a :: a). g a -> m (h (ff @@ a))) -> Prod ((,) j) g as -> m (Prod ((,) j) h (Fmap ff as))

ixProd :: Elem ((,) j) as a -> Lens' (Prod ((,) j) g as) (g a)

toRec :: Prod ((,) j) g as -> Rec g (ToList as)

withPureProd :: Prod ((,) j) g as -> (PureProd ((,) j) as -> r) -> r

type Shape f = (Prod f Proxy :: f k -> Type)

Simply witness the shape of an argument (ie, Shape [] as witnesses the length of as, and Shape Maybe as witnesses whether or not as is Just or Nothing).

class PureProd (f :: Type -> Type) (as :: f k) where

Create Prod f if you can give a g a for every slot.

Methods

pureProd :: (forall a. g a) -> Prod f g as

Instances

RecApplicative as => PureProd [] (as :: [k])

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a :: k0). g a) -> Prod [] g as

PureProd Maybe (Nothing :: Maybe k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a :: k0). g a) -> Prod Maybe g Nothing

PureProd Maybe (Just a :: Maybe k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a0 :: k0). g a0) -> Prod Maybe g (Just a)

PureProd Identity (Identity a :: Identity k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a0 :: k0). g a0) -> Prod Identity g (Identity0 a)

RecApplicative as => PureProd NonEmpty (a :| as :: NonEmpty k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a0 :: k0). g a0) -> Prod NonEmpty g (a :| as)

PureProd (Either j) (Right a :: Either j k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a0 :: k0). g a0) -> Prod (Either j) g (Right a)

SingI e => PureProd (Either j) (Left e :: Either j k)

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a :: k0). g a) -> Prod (Either j) g (Left e)

SingI w => PureProd ((,) j) ((,) w a :: (j, k))

Defined in Data.Type.Functor.Product

Methods

pureProd :: (forall (a0 :: k0). g a0) -> Prod ((,)0 j) g (w, a)

pureShape :: PureProd f as => Shape f as

Create a Shape given an instance of PureProd.

class PureProdC (f :: Type -> Type) c (as :: f k) where

Create Prod f if you can give a g a for every slot, given some constraint.

Methods

pureProdC :: (forall a. c a => g a) -> Prod f g as

Instances

RPureConstrained c as => PureProdC [] (c :: k -> Constraint) (as :: [k])

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k0). c a => g a) -> Prod [] g as

PureProdC Maybe (c :: k -> Constraint) (Nothing :: Maybe k)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k0). c a => g a) -> Prod Maybe g Nothing

c a2 => PureProdC Maybe (c :: a1 -> Constraint) (Just a2 :: Maybe a1)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k). c a => g a) -> Prod Maybe g (Just a2)

c a2 => PureProdC Identity (c :: a1 -> Constraint) (Identity a2 :: Identity a1)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k). c a => g a) -> Prod Identity g (Identity0 a2)

(c a2, RPureConstrained c as) => PureProdC NonEmpty (c :: a1 -> Constraint) (a2 :| as :: NonEmpty a1)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k). c a => g a) -> Prod NonEmpty g (a2 :| as)

c a => PureProdC (Either j) (c :: b -> Constraint) (Right a :: Either j b)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a0 :: k). c a0 => g a0) -> Prod (Either j) g (Right a)

SingI e => PureProdC (Either j) (c :: k -> Constraint) (Left e :: Either j k)

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a :: k0). c a => g a) -> Prod (Either j) g (Left e)

(SingI w, c a) => PureProdC ((,) j) (c :: k -> Constraint) ((,) w a :: (j, k))

Defined in Data.Type.Functor.Product

Methods

pureProdC :: (forall (a0 :: k0). c a0 => g a0) -> Prod ((,)0 j) g (w, a)

class ReifyConstraintProd (f :: Type -> Type) c (g :: k -> Type) (as :: f k) where

Pair up each item in a Prod f with a witness that f a satisfies some constraint.

Methods

reifyConstraintProd :: Prod f g as -> Prod f (Dict c :. g) as

Instances

ReifyConstraint c f as => ReifyConstraintProd [] c (f :: k -> Type) (as :: [k])

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod [] f as -> Prod [] (Dict c :. f) as

ReifyConstraintProd Maybe c (g :: k -> Type) (Nothing :: Maybe k)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod Maybe g Nothing -> Prod Maybe (Dict c :. g) Nothing

c (g a2) => ReifyConstraintProd Maybe c (g :: a1 -> Type) (Just a2 :: Maybe a1)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod Maybe g (Just a2) -> Prod Maybe (Dict c :. g) (Just a2)

c (g a2) => ReifyConstraintProd Identity c (g :: a1 -> Type) (Identity a2 :: Identity a1)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod Identity g (Identity0 a2) -> Prod Identity (Dict c :. g) (Identity0 a2)

(c (g a2), ReifyConstraint c g as) => ReifyConstraintProd NonEmpty c (g :: a1 -> Type) (a2 :| as :: NonEmpty a1)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod NonEmpty g (a2 :| as) -> Prod NonEmpty (Dict c :. g) (a2 :| as)

c (g a) => ReifyConstraintProd (Either j) c (g :: b -> Type) (Right a :: Either j b)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod (Either j) g (Right a) -> Prod (Either j) (Dict c :. g) (Right a)

ReifyConstraintProd (Either j) c (g :: k -> Type) (Left e :: Either j k)

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod (Either j) g (Left e) -> Prod (Either j) (Dict c :. g) (Left e)

c (g a) => ReifyConstraintProd ((,) j) c (g :: k -> Type) ((,) w a :: (j, k))

Defined in Data.Type.Functor.Product

Methods

reifyConstraintProd :: Prod ((,)0 j) g (w, a) -> Prod ((,)0 j) (Dict c :. g) (w, a)

type AllConstrainedProd c as = AllConstrained c (ToList as)

A convenient wrapper over AllConstrained that works for any Foldable f.

Functions

indexProd :: FProd f => Elem f as a -> Prod f g as -> g a

Use an Elem to index a value out of a Prod.

mapProd :: FProd f => (forall a. g a -> h a) -> Prod f g as -> Prod f h as

Map a RankN function over a Prod. The generalization of rmap.

foldMapProd :: (FProd f, Monoid m) => (forall a. g a -> m) -> Prod f g as -> m

Map a RankN function over a Prod and collect the results as a Monoid.

hmap :: FProd f => Sing ff -> (forall a. g a -> h (ff @@ a)) -> Prod f g as -> Prod f h (Fmap ff as)

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

Zip together the values in two Prods.

imapProd :: FProd f => (forall a. Elem f as a -> g a -> h a) -> Prod f g as -> Prod f h as

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)

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

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

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)

Construct a Prod in an Applicative context by providing a generating function for each index.

selectProd :: FProd f => Prod f (Elem f as) bs -> Prod f g as -> Prod f g bs

Rearrange or permute the items in a Prod based on a Prod of indices.

selectProd (IS IZ :& IZ :& RNil) ("hi" :& "bye" :& "ok" :& RNil)
     == "bye" :& "hi" :& RNil

indices :: (FProd f, PureProd f as) => Prod f (Elem f as) as

Generate a Prod of indices for an as.

eqProd :: (FProd f, ReifyConstraintProd f Eq g as) => Prod f g as -> Prod f g as -> Bool

An implementation of equality testing for all FProd instances, as long as each of the items are instances of Eq.

compareProd :: (FProd f, ReifyConstraintProd f Ord g as) => Prod f g as -> Prod f g as -> Ordering

An implementation of order comparison for all FProd instances, as long as each of the items are instances of Ord.

Over singletons

indexSing

Arguments

:: FProd f

=> Elem f as a

Witness

-> Sing as

Collection

-> Sing a

Extract the item from the container witnessed by the Elem

singShape :: FProd f => Sing as -> Shape f as

Convert a Sing as into a Shape f as, witnessing the shape of of as but dropping all of its values.

foldMapSing :: forall f k (as :: f k) m. (FProd f, Monoid m) => (forall (a :: k). Sing a -> m) -> Sing as -> m

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

foldMapSing but with access to the index.

Instances

data Rec (a :: u -> Type) (b :: [u]) :: forall u. (u -> Type) -> [u] -> Type 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 :: *.

Constructors

RNil :: forall u (a :: u -> Type) (b :: [u]). Rec a ([] :: [u])

(:&) :: forall u (a :: u -> Type) (b :: [u]) (r :: u) (rs :: [u]). !(a r) -> !(Rec a rs) -> Rec a (r ': rs) infixr 7

Instances

RecElem (Rec :: (a -> Type) -> [a] -> Type) (r :: a) (r' :: a) (r ': rs :: [a]) (r' ': rs :: [a]) Z

Defined in Data.Vinyl.Lens

Associated Types

type RecElemFCtx Rec f :: Constraint

Methods

rlensC :: (Functor g, RecElemFCtx Rec f) => (f r -> g (f r')) -> Rec f (r ': rs) -> g (Rec f (r' ': rs))

rgetC :: (RecElemFCtx Rec f, r ~ r') => Rec f (r ': rs) -> f r

rputC :: RecElemFCtx Rec f => f r' -> Rec f (r ': rs) -> Rec f (r' ': rs)

(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

Associated Types

type RecElemFCtx Rec f :: Constraint

Methods

rlensC :: (Functor g, RecElemFCtx Rec f) => (f r -> g (f r')) -> Rec f (s ': rs) -> g (Rec f (s ': rs'))

rgetC :: (RecElemFCtx Rec f, r ~ r') => Rec f (s ': rs) -> f r

rputC :: RecElemFCtx Rec f => f r' -> Rec f (s ': rs) -> Rec f (s ': rs')

RecSubset (Rec :: (k -> Type) -> [k] -> Type) ([] :: [k]) (ss :: [k]) ([] :: [Nat])

Defined in Data.Vinyl.Lens

Associated Types

type RecSubsetFCtx Rec f :: Constraint

Methods

rsubsetC :: (Functor g, RecSubsetFCtx Rec f) => (Rec f [] -> g (Rec f [])) -> Rec f ss -> g (Rec f ss)

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f []

rreplaceC :: 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

Associated Types

type RecSubsetFCtx Rec f :: Constraint

Methods

rsubsetC :: (Functor g, RecSubsetFCtx Rec f) => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss)

rcastC :: RecSubsetFCtx Rec f => Rec f ss -> Rec f (r ': rs)

rreplaceC :: RecSubsetFCtx Rec f => Rec f (r ': rs) -> Rec f ss -> Rec f ss

TestCoercion f => TestCoercion (Rec f :: [u] -> Type)

Defined in Data.Vinyl.Core

Methods

testCoercion :: Rec f a -> Rec f b -> Maybe (Coercion a b)

TestEquality f => TestEquality (Rec f :: [u] -> Type)

Defined in Data.Vinyl.Core

Methods

testEquality :: Rec f a -> Rec f b -> Maybe (a :~: b)

Eq (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Methods

(==) :: Rec f [] -> Rec f [] -> Bool

(/=) :: Rec f [] -> Rec f [] -> Bool

(Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Methods

(==) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool

(/=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool

Ord (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Methods

compare :: Rec f [] -> Rec f [] -> Ordering

(<) :: Rec f [] -> Rec f [] -> Bool

(<=) :: Rec f [] -> Rec f [] -> Bool

(>) :: Rec f [] -> Rec f [] -> Bool

(>=) :: Rec f [] -> Rec f [] -> Bool

max :: Rec f [] -> Rec f [] -> Rec f []

min :: Rec f [] -> Rec f [] -> Rec f []

(Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Methods

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)

(RMap rs, ReifyConstraint Show f rs, RecordToList rs) => Show (Rec f rs)

Records may be shown insofar as their points may be shown. reifyConstraint is used to great effect here.

Defined in Data.Vinyl.Core

Methods

showsPrec :: Int -> Rec f rs -> ShowS

show :: Rec f rs -> String

showList :: [Rec f rs] -> ShowS

Generic (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Associated Types

type Rep (Rec f []) :: Type -> Type

Methods

from :: Rec f [] -> Rep (Rec f []) x

to :: Rep (Rec f []) x -> Rec f []

Generic (Rec f rs) => Generic (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Associated Types

type Rep (Rec f (r ': rs)) :: Type -> Type

Methods

from :: Rec f (r ': rs) -> Rep (Rec f (r ': rs)) x

to :: Rep (Rec f (r ': rs)) x -> Rec f (r ': rs)

Semigroup (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Methods

(<>) :: Rec f [] -> Rec f [] -> Rec f []

sconcat :: NonEmpty (Rec f []) -> Rec f []

stimes :: Integral b => b -> Rec f [] -> Rec f []

(Semigroup (f r), Semigroup (Rec f rs)) => Semigroup (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Methods

(<>) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs)

sconcat :: NonEmpty (Rec f (r ': rs)) -> Rec f (r ': rs)

stimes :: Integral b => b -> Rec f (r ': rs) -> Rec f (r ': rs)

Monoid (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Methods

mempty :: Rec f []

mappend :: Rec f [] -> Rec f [] -> Rec f []

mconcat :: [Rec f []] -> Rec f []

(Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Methods

mempty :: Rec f (r ': rs)

mappend :: Rec f (r ': rs) -> Rec f (r ': rs) -> Rec f (r ': rs)

mconcat :: [Rec f (r ': rs)] -> Rec f (r ': rs)

Storable (Rec f ([] :: [u]))

Defined in Data.Vinyl.Core

Methods

sizeOf :: Rec f [] -> Int

alignment :: Rec f [] -> Int

peekElemOff :: Ptr (Rec f []) -> Int -> IO (Rec f [])

pokeElemOff :: Ptr (Rec f []) -> Int -> Rec f [] -> IO ()

peekByteOff :: Ptr b -> Int -> IO (Rec f [])

pokeByteOff :: Ptr b -> Int -> Rec f [] -> IO ()

peek :: Ptr (Rec f []) -> IO (Rec f [])

poke :: Ptr (Rec f []) -> Rec f [] -> IO ()

(Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs))

Defined in Data.Vinyl.Core

Methods

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 ()

peek :: Ptr (Rec f (r ': rs)) -> IO (Rec f (r ': rs))

poke :: Ptr (Rec f (r ': rs)) -> Rec f (r ': rs) -> IO ()

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) = ()

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) = ()

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) = ()

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) = ()

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

type Rep (Rec f ([] :: [u])) = C1 (MetaCons "RNil" PrefixI False) (S1 (MetaSel (Nothing :: Maybe Symbol) NoSourceUnpackedness NoSourceStrictness DecidedLazy) (U1 :: Type -> Type))

data Index :: [k] -> k -> Type where

Witness an item in a type-level list by providing its index.

The number of ISs correspond to the item's position in the list.

IZ         :: Index '[5,10,2] 5
IS IZ      :: Index '[5,10,2] 10
IS (IS IZ) :: Index '[5,10,2] 2

Constructors

IZ :: Index (a ': as) a

IS :: Index bs a -> Index (b ': bs) a

Instances

Eq (Index as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: Index as a -> Index as a -> Bool

(/=) :: Index as a -> Index as a -> Bool

Ord (Index as a)

Defined in Data.Type.Functor.Product

Methods

compare :: Index as a -> Index as a -> Ordering

(<) :: Index as a -> Index as a -> Bool

(<=) :: Index as a -> Index as a -> Bool

(>) :: Index as a -> Index as a -> Bool

(>=) :: Index as a -> Index as a -> Bool

max :: Index as a -> Index as a -> Index as a

min :: Index as a -> Index as a -> Index as a

Show (Index as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> Index as a -> ShowS

show :: Index as a -> String

showList :: [Index as a] -> ShowS

SDecide (Index as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (Index as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (Index as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (Index as a)

toSing :: Demote (Index as a) -> SomeSing (Index as a)

SingI (IZ :: Index (a ': as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing IZ

SingI i => SingI (IS i :: Index (b ': bs) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing (IS i)

data Sing (i :: Index as a)

Defined in Data.Type.Functor.Product

data Sing (i :: Index as a) = SIndex' (SIndex as a i)

type Demote (Index as a)

Defined in Data.Type.Functor.Product

type Demote (Index as a) = Index as a

withPureProdList :: Rec f as -> ((RecApplicative as, PureProd [] as) => r) -> r

A stronger version of withPureProd for Rec, providing a RecApplicative instance as well.

data PMaybe :: (k -> Type) -> Maybe k -> Type where

A PMaybe f 'Nothing contains nothing, and a PMaybe f ('Just a) contains an 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.

Constructors

PNothing :: PMaybe f Nothing

PJust :: f a -> PMaybe f (Just a)

Instances

ReifyConstraintProd Maybe Eq f as => Eq (PMaybe f as)

Defined in Data.Type.Functor.Product

Methods

(==) :: PMaybe f as -> PMaybe f as -> Bool

(/=) :: PMaybe f as -> PMaybe f as -> Bool

(ReifyConstraintProd Maybe Eq f as, ReifyConstraintProd Maybe Ord f as) => Ord (PMaybe f as)

Defined in Data.Type.Functor.Product

Methods

compare :: PMaybe f as -> PMaybe f as -> Ordering

(<) :: PMaybe f as -> PMaybe f as -> Bool

(<=) :: PMaybe f as -> PMaybe f as -> Bool

(>) :: PMaybe f as -> PMaybe f as -> Bool

(>=) :: PMaybe f as -> PMaybe f as -> Bool

max :: PMaybe f as -> PMaybe f as -> PMaybe f as

min :: PMaybe f as -> PMaybe f as -> PMaybe f as

ReifyConstraintProd Maybe Show f as => Show (PMaybe f as)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> PMaybe f as -> ShowS

show :: PMaybe f as -> String

showList :: [PMaybe f as] -> ShowS

data IJust :: Maybe k -> k -> Type where

Witness an item in a type-level Maybe by proving the Maybe is Just.

Constructors

IJust :: IJust (Just a) a

Instances

Eq (IJust as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IJust as a -> IJust as a -> Bool

(/=) :: IJust as a -> IJust as a -> Bool

Ord (IJust as a)

Defined in Data.Type.Functor.Product

Methods

compare :: IJust as a -> IJust as a -> Ordering

(<) :: IJust as a -> IJust as a -> Bool

(<=) :: IJust as a -> IJust as a -> Bool

(>) :: IJust as a -> IJust as a -> Bool

(>=) :: IJust as a -> IJust as a -> Bool

max :: IJust as a -> IJust as a -> IJust as a

min :: IJust as a -> IJust as a -> IJust as a

Read (IJust (Just a) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IJust (Just a) a)

readList :: ReadS [IJust (Just a) a]

readPrec :: ReadPrec (IJust (Just a) a)

readListPrec :: ReadPrec [IJust (Just a) a]

Show (IJust as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> IJust as a -> ShowS

show :: IJust as a -> String

showList :: [IJust as a] -> ShowS

SDecide (IJust as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IJust as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IJust as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (IJust as a)

toSing :: Demote (IJust as a) -> SomeSing (IJust as a)

SingI (IJust :: IJust (Just a) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing IJust

data Sing (i :: IJust as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IJust as a) = SIJust' (SIJust as a i)

type Demote (IJust as a)

Defined in Data.Type.Functor.Product

type Demote (IJust as a) = IJust as a

data PEither :: (k -> Type) -> Either j k -> Type where

A PEither f ('Left e) contains Sing e, and a PMaybe f ('Right a) contains an f a.

In practice this can be useful in the same situatinos that PMaybe can, but with an extra value in the case where value f is "turned off" with Left.

Constructors

PLeft :: Sing e -> PEither f (Left e)

PRight :: f a -> PEither f (Right a)

Instances

(SShow j, ReifyConstraintProd (Either j) Show f as) => Show (PEither f as)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> PEither f as -> ShowS

show :: PEither f as -> String

showList :: [PEither f as] -> ShowS

data IRight :: Either j k -> k -> Type where

Witness an item in a type-level Either j by proving the Either is Right.

Constructors

IRight :: IRight (Right a) a

Instances

Eq (IRight as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IRight as a -> IRight as a -> Bool

(/=) :: IRight as a -> IRight as a -> Bool

Ord (IRight as a)

Defined in Data.Type.Functor.Product

Methods

compare :: IRight as a -> IRight as a -> Ordering

(<) :: IRight as a -> IRight as a -> Bool

(<=) :: IRight as a -> IRight as a -> Bool

(>) :: IRight as a -> IRight as a -> Bool

(>=) :: IRight as a -> IRight as a -> Bool

max :: IRight as a -> IRight as a -> IRight as a

min :: IRight as a -> IRight as a -> IRight as a

Read (IRight (Right a :: Either j k) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IRight (Right a) a)

readList :: ReadS [IRight (Right a) a]

readPrec :: ReadPrec (IRight (Right a) a)

readListPrec :: ReadPrec [IRight (Right a) a]

Show (IRight as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> IRight as a -> ShowS

show :: IRight as a -> String

showList :: [IRight as a] -> ShowS

SDecide (IRight as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IRight as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IRight as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (IRight as a)

toSing :: Demote (IRight as a) -> SomeSing (IRight as a)

SingI (IRight :: IRight (Right a :: Either j k) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing IRight

data Sing (i :: IRight as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IRight as a) = SIRight' (SIRight as a i)

type Demote (IRight as a)

Defined in Data.Type.Functor.Product

type Demote (IRight as a) = IRight as a

data NERec :: (k -> Type) -> NonEmpty k -> Type where

A non-empty version of Rec.

Constructors

(:&|) :: f a -> Rec f as -> NERec f (a :| as) infixr 5

Instances

(Eq (f a2), Eq (Rec f as)) => Eq (NERec f (a2 :| as))

Defined in Data.Type.Functor.Product

Methods

(==) :: NERec f (a2 :| as) -> NERec f (a2 :| as) -> Bool

(/=) :: NERec f (a2 :| as) -> NERec f (a2 :| as) -> Bool

(Ord (f a2), Ord (Rec f as)) => Ord (NERec f (a2 :| as))

Defined in Data.Type.Functor.Product

Methods

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)

(Show (f a2), RMap as, ReifyConstraint Show f as, RecordToList as) => Show (NERec f (a2 :| as))

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> NERec f (a2 :| as) -> ShowS

show :: NERec f (a2 :| as) -> String

showList :: [NERec f (a2 :| as)] -> ShowS

data NEIndex :: NonEmpty k -> k -> Type where

Witness an item in a type-level NonEmpty by either indicating that it is the "head", or by providing an index in the "tail".

Constructors

NEHead :: NEIndex (a :| as) a

NETail :: Index as a -> NEIndex (b :| as) a

Instances

Eq (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: NEIndex as a -> NEIndex as a -> Bool

(/=) :: NEIndex as a -> NEIndex as a -> Bool

Ord (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

compare :: NEIndex as a -> NEIndex as a -> Ordering

(<) :: NEIndex as a -> NEIndex as a -> Bool

(<=) :: NEIndex as a -> NEIndex as a -> Bool

(>) :: NEIndex as a -> NEIndex as a -> Bool

(>=) :: NEIndex as a -> NEIndex as a -> Bool

max :: NEIndex as a -> NEIndex as a -> NEIndex as a

min :: NEIndex as a -> NEIndex as a -> NEIndex as a

Show (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> NEIndex as a -> ShowS

show :: NEIndex as a -> String

showList :: [NEIndex as a] -> ShowS

SDecide (NEIndex as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (NEIndex as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (NEIndex as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (NEIndex as a)

toSing :: Demote (NEIndex as a) -> SomeSing (NEIndex as a)

SingI (NEHead :: NEIndex (a :| as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing NEHead

SingI i => SingI (NETail i :: NEIndex (b :| as) a)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing (NETail i)

data Sing (i :: NEIndex as a)

Defined in Data.Type.Functor.Product

data Sing (i :: NEIndex as a) = SNEIndex' (SNEIndex as a i)

type Demote (NEIndex as a)

Defined in Data.Type.Functor.Product

type Demote (NEIndex as a) = NEIndex as a

withPureProdNE :: f a -> Rec f as -> ((RecApplicative as, PureProd NonEmpty (a :| as)) => r) -> r

A stronger version of withPureProd for NERec, providing a RecApplicative instance as well.

data PTup :: (k -> Type) -> (j, k) -> Type where

A PTup tuples up some singleton with some value; a PTup f '(w, a) contains a Sing w and an f a.

This can be useful for carrying along some witness aside a functor value.

Constructors

PTup :: Sing w -> f a -> PTup f '(w, a)

Instances

(Eq (Sing w), Eq (f a)) => Eq (PTup f ((,) w a))

Defined in Data.Type.Functor.Product

Methods

(==) :: PTup f (w, a) -> PTup f (w, a) -> Bool

(/=) :: PTup f (w, a) -> PTup f (w, a) -> Bool

(Ord (Sing w), Ord (f a)) => Ord (PTup f ((,) w a))

Defined in Data.Type.Functor.Product

Methods

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

max :: PTup f (w, a) -> PTup f (w, a) -> PTup f (w, a)

min :: PTup f (w, a) -> PTup f (w, a) -> PTup f (w, a)

(Read (Sing w), Read (f a)) => Read (PTup f ((,) w a))

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (PTup f (w, a))

readList :: ReadS [PTup f (w, a)]

readPrec :: ReadPrec (PTup f (w, a))

readListPrec :: ReadPrec [PTup f (w, a)]

(Show (Sing w), Show (f a)) => Show (PTup f ((,) w a))

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> PTup f (w, a) -> ShowS

show :: PTup f (w, a) -> String

showList :: [PTup f (w, a)] -> ShowS

data ISnd :: (j, k) -> k -> Type where

Trivially witness an item in the second field of a type-level tuple.

Constructors

ISnd :: ISnd '(a, b) b

Instances

Eq (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: ISnd as a -> ISnd as a -> Bool

(/=) :: ISnd as a -> ISnd as a -> Bool

Ord (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

compare :: ISnd as a -> ISnd as a -> Ordering

(<) :: ISnd as a -> ISnd as a -> Bool

(<=) :: ISnd as a -> ISnd as a -> Bool

(>) :: ISnd as a -> ISnd as a -> Bool

(>=) :: ISnd as a -> ISnd as a -> Bool

max :: ISnd as a -> ISnd as a -> ISnd as a

min :: ISnd as a -> ISnd as a -> ISnd as a

Read (ISnd ((,) a b) b)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (ISnd (a, b) b)

readList :: ReadS [ISnd (a, b) b]

readPrec :: ReadPrec (ISnd (a, b) b)

readListPrec :: ReadPrec [ISnd (a, b) b]

Show (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> ISnd as a -> ShowS

show :: ISnd as a -> String

showList :: [ISnd as a] -> ShowS

SDecide (ISnd as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (ISnd as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (ISnd as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (ISnd as a)

toSing :: Demote (ISnd as a) -> SomeSing (ISnd as a)

SingI (ISnd :: ISnd ((,) a b) b)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing ISnd

data Sing (i :: ISnd as a)

Defined in Data.Type.Functor.Product

data Sing (i :: ISnd as a) = SISnd' (SISnd as a i)

type Demote (ISnd as a)

Defined in Data.Type.Functor.Product

type Demote (ISnd as a) = ISnd as a

data PIdentity :: (k -> Type) -> Identity k -> Type where

A PIdentity is a trivial functor product; it is simply the functor, itself, alone. PIdentity f (Identity a) is simply f a. This may be useful in conjunction with other combinators.

Constructors

PIdentity :: f a -> PIdentity f (Identity a)

Instances

Eq (f a2) => Eq (PIdentity f (Identity a2))

Defined in Data.Type.Functor.Product

Methods

(==) :: PIdentity f (Identity a2) -> PIdentity f (Identity a2) -> Bool

(/=) :: PIdentity f (Identity a2) -> PIdentity f (Identity a2) -> Bool

Ord (f a2) => Ord (PIdentity f (Identity a2))

Defined in Data.Type.Functor.Product

Methods

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)

Read (f a2) => Read (PIdentity f (Identity a2))

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (PIdentity f (Identity a2))

readList :: ReadS [PIdentity f (Identity a2)]

readPrec :: ReadPrec (PIdentity f (Identity a2))

readListPrec :: ReadPrec [PIdentity f (Identity a2)]

Show (f a2) => Show (PIdentity f (Identity a2))

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> PIdentity f (Identity a2) -> ShowS

show :: PIdentity f (Identity a2) -> String

showList :: [PIdentity f (Identity a2)] -> ShowS

data IIdentity :: Identity k -> k -> Type where

Trivially witness the item held in an Identity.

Since: 0.1.3.0

Constructors

IId :: IIdentity (Identity x) x

Instances

Eq (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

(==) :: IIdentity as a -> IIdentity as a -> Bool

(/=) :: IIdentity as a -> IIdentity as a -> Bool

Ord (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

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

max :: IIdentity as a -> IIdentity as a -> IIdentity as a

min :: IIdentity as a -> IIdentity as a -> IIdentity as a

Read (IIdentity (Identity a) a)

Defined in Data.Type.Functor.Product

Methods

readsPrec :: Int -> ReadS (IIdentity (Identity a) a)

readList :: ReadS [IIdentity (Identity a) a]

readPrec :: ReadPrec (IIdentity (Identity a) a)

readListPrec :: ReadPrec [IIdentity (Identity a) a]

Show (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> IIdentity as a -> ShowS

show :: IIdentity as a -> String

showList :: [IIdentity as a] -> ShowS

SDecide (IIdentity as a)

Defined in Data.Type.Functor.Product

Methods

(%~) :: Sing a0 -> Sing b -> Decision (a0 :~: b)

SingKind (IIdentity as a)

Defined in Data.Type.Functor.Product

Associated Types

type Demote (IIdentity as a) = (r :: Type)

Methods

fromSing :: Sing a0 -> Demote (IIdentity as a)

toSing :: Demote (IIdentity as a) -> SomeSing (IIdentity as a)

SingI (IId :: IIdentity (Identity x) x)

Defined in Data.Type.Functor.Product

Methods

sing :: Sing IId

data Sing (i :: IIdentity as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IIdentity as a) = SIIdentity' (SIIdentity as a i)

type Demote (IIdentity as a)

Defined in Data.Type.Functor.Product

type Demote (IIdentity as a) = IIdentity as a

sameIndexVal :: Index as a -> Index as b -> Maybe (a :~: b)

Test if two indices point to the same item in a 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.

sameNEIndexVal :: NEIndex as a -> NEIndex as b -> Maybe (a :~: b)

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

rElemIndex :: forall r rs i. (RElem r rs i, PureProd [] rs) => Index rs r

Produce an Index from an RElem constraint.

indexRElem :: (SDecide k, SingI (a :: k), RecApplicative as, FoldRec as as) => Index as a -> (RElem a as (RIndex a as) => r) -> r

If we have Index as a, we should also be able to create an item that would require RElem a as (RIndex as a). Along with rElemIndex, this essentially converts between the indexing system in this library and the indexing system of vinyl.

toCoRec :: forall as a f. (RecApplicative as, FoldRec as as) => Index as a -> f a -> CoRec f as

Use an Index to inject an f a into a CoRec.

Singletons

data SIndex as a :: Index as a -> Type where

Kind-indexed singleton for Index. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SIndex', which has an actual proper Sing instance.

Constructors

SIZ :: SIndex (a ': as) a IZ

SIS :: SIndex bs a i -> SIndex (b ': bs) a (IS i)

Instances

Show (SIndex as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SIndex as a i -> ShowS

show :: SIndex as a i -> String

showList :: [SIndex as a i] -> ShowS

data SIJust as a :: IJust as a -> Type where

Kind-indexed singleton for IJust. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SIJust', which has an actual proper Sing instance.

This distinction will be unnecessary once Sing is a type family.

Constructors

SIJust :: SIJust (Just a) a IJust

Instances

Show (SIJust as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SIJust as a i -> ShowS

show :: SIJust as a i -> String

showList :: [SIJust as a i] -> ShowS

data SIRight as a :: IRight as a -> Type where

Kind-indexed singleton for IRight. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SIRight', which has an actual proper Sing instance.

Constructors

SIRight :: SIRight (Right a) a IRight

Instances

Show (SIRight as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SIRight as a i -> ShowS

show :: SIRight as a i -> String

showList :: [SIRight as a i] -> ShowS

data SNEIndex as a :: NEIndex as a -> Type where

Kind-indexed singleton for NEIndex. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SNEIndex', which has an actual proper Sing instance.

Constructors

SNEHead :: SNEIndex (a :| as) a NEHead

SNETail :: SIndex as a i -> SNEIndex (b :| as) a (NETail i)

Instances

Show (SNEIndex as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SNEIndex as a i -> ShowS

show :: SNEIndex as a i -> String

showList :: [SNEIndex as a i] -> ShowS

data SISnd as a :: ISnd as a -> Type where

Kind-indexed singleton for ISnd. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SISnd', which has an actual proper Sing instance.

Constructors

SISnd :: SISnd '(a, b) b ISnd

Instances

Show (SISnd as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SISnd as a i -> ShowS

show :: SISnd as a i -> String

showList :: [SISnd as a i] -> ShowS

data SIIdentity as a :: IIdentity as a -> Type where

Kind-indexed singleton for IIdentity. Provided as a separate data declaration to allow you to use these at the type level. However, the main interface is still provided through the newtype wrapper SIIdentity', which has an actual proper Sing instance.

Since: 0.1.5.0

Constructors

SIId :: SIIdentity (Identity a) a IId

Instances

Show (SIIdentity as a i)

Defined in Data.Type.Functor.Product

Methods

showsPrec :: Int -> SIIdentity as a i -> ShowS

show :: SIIdentity as a i -> String

showList :: [SIIdentity as a i] -> ShowS

data family Sing (a :: k) :: Type

The singleton kind-indexed data family.

Instances

data Sing (a :: Bool)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Bool) where

• SFalse :: forall (a :: Bool). Sing False
• STrue :: forall (a :: Bool). Sing True

data Sing (a :: Ordering)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Ordering) where

• SLT :: forall (a :: Ordering). Sing LT
• SEQ :: forall (a :: Ordering). Sing EQ
• SGT :: forall (a :: Ordering). Sing GT

data Sing (n :: Nat)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Nat) where

• SNat :: forall (n :: Nat). KnownNat n => Sing n

data Sing (n :: Symbol)

Defined in Data.Singletons.TypeLits.Internal

data Sing (n :: Symbol) where

• SSym :: forall (n :: Symbol). KnownSymbol n => Sing n

data Sing (a :: ())

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: ()) where

• STuple0 :: forall (a :: ()). Sing ()

data Sing (a :: Void)

Defined in Data.Singletons.Prelude.Instances

data Sing (a :: Void)

data Sing (a :: All)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: All) where

• SAll :: forall (a :: All) (n :: Bool). {..} -> Sing (All n)

data Sing (a :: Any)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: Any) where

• SAny :: forall (a :: Any) (n :: Bool). {..} -> Sing (Any n)

data Sing (b :: [a])

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: [a]) where

• SNil :: forall a (b :: [a]). Sing ([] :: [a])
• SCons :: forall a (b :: [a]) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 ': n2)

data Sing (b :: Maybe a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Maybe a) where

• SNothing :: forall a (b :: Maybe a). Sing (Nothing :: Maybe a)
• SJust :: forall a (b :: Maybe a) (n :: a). Sing n -> Sing (Just n)

data Sing (b :: Min a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Min a) where

• SMin :: forall a (b :: Min a) (n :: a). {..} -> Sing (Min n)

data Sing (b :: Max a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Max a) where

• SMax :: forall a (b :: Max a) (n :: a). {..} -> Sing (Max n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: a). {..} -> Sing (Last n)

data Sing (a :: WrappedMonoid m)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (a :: WrappedMonoid m) where

• SWrapMonoid :: forall m (a :: WrappedMonoid m) (n :: m). {..} -> Sing (WrapMonoid n)

data Sing (b :: Option a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Option a) where

• SOption :: forall a (b :: Option a) (n :: Maybe a). {..} -> Sing (Option n)

data Sing (b :: Identity a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: Identity a) where

• SIdentity :: forall a (b :: Identity a) (n :: a). {..} -> Sing (Identity n)

data Sing (b :: First a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: First a) where

• SFirst :: forall a (b :: First a) (n :: Maybe a). {..} -> Sing (First n)

data Sing (b :: Last a)

Defined in Data.Singletons.Prelude.Monoid

data Sing (b :: Last a) where

• SLast :: forall a (b :: Last a) (n :: Maybe a). {..} -> Sing (Last n)

data Sing (b :: Dual a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Dual a) where

• SDual :: forall a (b :: Dual a) (n :: a). {..} -> Sing (Dual n)

data Sing (b :: Sum a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Sum a) where

• SSum :: forall a (b :: Sum a) (n :: a). {..} -> Sing (Sum n)

data Sing (b :: Product a)

Defined in Data.Singletons.Prelude.Semigroup.Internal

data Sing (b :: Product a) where

• SProduct :: forall a (b :: Product a) (n :: a). {..} -> Sing (Product n)

data Sing (b :: Down a)

Defined in Data.Singletons.Prelude.Ord

data Sing (b :: Down a) where

• SDown :: forall a (b :: Down a) (n :: a). Sing n -> Sing (Down n)

data Sing (b :: NonEmpty a)

Defined in Data.Singletons.Prelude.Instances

data Sing (b :: NonEmpty a) where

• (:%|) :: forall a (b :: NonEmpty a) (n1 :: a) (n2 :: [a]). Sing n1 -> Sing n2 -> Sing (n1 :| n2)

data Sing (b :: Endo a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: Endo a) where

• SEndo :: forall a (b :: Endo a) (x :: a ~> a). Sing x -> Sing (Endo x)

data Sing (b :: MaxInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MaxInternal a) where

• SMaxInternal :: forall a (b :: MaxInternal a) (x :: Maybe a). Sing x -> Sing (MaxInternal x)

data Sing (b :: MinInternal a)

Defined in Data.Singletons.Prelude.Foldable

data Sing (b :: MinInternal a) where

• SMinInternal :: forall a (b :: MinInternal a) (x :: Maybe a). Sing x -> Sing (MinInternal x)

data Sing (c :: Either a b)

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: Either a b) where

• SLeft :: forall a b (c :: Either a b) (n :: a). Sing n -> Sing (Left n :: Either a b)
• SRight :: forall a b (c :: Either a b) (n :: b). Sing n -> Sing (Right n :: Either a b)

data Sing (c :: (a, b))

Defined in Data.Singletons.Prelude.Instances

data Sing (c :: (a, b)) where

• STuple2 :: forall a b (c :: (a, b)) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing ((,) n1 n2)

data Sing (c :: Arg a b)

Defined in Data.Singletons.Prelude.Semigroup

data Sing (c :: Arg a b) where

• SArg :: forall a b (c :: Arg a b) (n1 :: a) (n2 :: b). Sing n1 -> Sing n2 -> Sing (Arg n1 n2)

data Sing (f :: k1 ~> k2)

Defined in Data.Singletons.Internal

data Sing (f :: k1 ~> k2) = SLambda {

• applySing :: forall (t :: k1). Sing t -> Sing (f @@ t)

}

data Sing (b :: StateL s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateL s a) where

• SStateL :: forall s a (b :: StateL s a) (x :: s ~> (s, a)). Sing x -> Sing (StateL x)

data Sing (b :: StateR s a)

Defined in Data.Singletons.Prelude.Traversable

data Sing (b :: StateR s a) where

• SStateR :: forall s a (b :: StateR s a) (x :: s ~> (s, a)). Sing x -> Sing (StateR x)

data Sing (d :: (a, b, c))

Defined in Data.Singletons.Prelude.Instances

data Sing (d :: (a, b, c)) where

• STuple3 :: forall a b c (d :: (a, b, c)) (n1 :: a) (n2 :: b) (n3 :: c). Sing n1 -> Sing n2 -> Sing n3 -> Sing ((,,) n1 n2 n3)

data Sing (c :: Const a b)

Defined in Data.Singletons.Prelude.Const

data Sing (c :: Const a b) where

• SConst :: forall k a (b :: k) (c :: Const a b) (a1 :: a). {..} -> Sing (Const a1 :: Const a b)

data Sing (i :: IIdentity as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IIdentity as a) = SIIdentity' (SIIdentity as a i)

data Sing (i :: NEIndex as a)

Defined in Data.Type.Functor.Product

data Sing (i :: NEIndex as a) = SNEIndex' (SNEIndex as a i)

data Sing (i :: IJust as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IJust as a) = SIJust' (SIJust as a i)

data Sing (i :: Index as a)

Defined in Data.Type.Functor.Product

data Sing (i :: Index as a) = SIndex' (SIndex as a i)

data Sing (e :: (a, b, c, d))

Defined in Data.Singletons.Prelude.Instances

data Sing (e :: (a, b, c, d)) where

• STuple4 :: forall a b c d (e :: (a, b, c, d)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing ((,,,) n1 n2 n3 n4)

data Sing (i :: ISnd as a)

Defined in Data.Type.Functor.Product

data Sing (i :: ISnd as a) = SISnd' (SISnd as a i)

data Sing (i :: IRight as a)

Defined in Data.Type.Functor.Product

data Sing (i :: IRight as a) = SIRight' (SIRight as a i)

data Sing (f :: (a, b, c, d, e))

Defined in Data.Singletons.Prelude.Instances

data Sing (f :: (a, b, c, d, e)) where

• STuple5 :: forall a b c d e (f :: (a, b, c, d, e)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing ((,,,,) n1 n2 n3 n4 n5)

data Sing (g :: (a, b, c, d, e, f))

Defined in Data.Singletons.Prelude.Instances

data Sing (g :: (a, b, c, d, e, f)) where

• STuple6 :: forall a b c d e f (g :: (a, b, c, d, e, f)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing ((,,,,,) n1 n2 n3 n4 n5 n6)

data Sing (h :: (a, b, c, d, e, f, g))

Defined in Data.Singletons.Prelude.Instances

data Sing (h :: (a, b, c, d, e, f, g)) where

• STuple7 :: forall a b c d e f g (h :: (a, b, c, d, e, f, g)) (n1 :: a) (n2 :: b) (n3 :: c) (n4 :: d) (n5 :: e) (n6 :: f) (n7 :: g). Sing n1 -> Sing n2 -> Sing n3 -> Sing n4 -> Sing n5 -> Sing n6 -> Sing n7 -> Sing ((,,,,,,) n1 n2 n3 n4 n5 n6 n7)

Defunctionalization symbols

data ElemSym0 (f :: Type -> Type) :: f k ~> (k ~> Type)

Instances

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> Type) (as :: f k)

Defined in Data.Type.Functor.Product

type Apply (ElemSym0 f :: TyFun (f k) (k ~> Type) -> Type) (as :: f k) = ElemSym1 f as

data ElemSym1 (f :: Type -> Type) :: f k -> k ~> Type

Instances

type Apply (ElemSym1 f as :: TyFun k Type -> Type) (a :: k)

Defined in Data.Type.Functor.Product

type Apply (ElemSym1 f as :: TyFun k Type -> Type) (a :: k) = Elem f as a

type ElemSym2 (f :: Type -> Type) (as :: f k) (a :: k) = Elem f as a

data ProdSym0 (f :: Type -> Type) :: (k -> Type) ~> (f k ~> Type)

Instances

type Apply (ProdSym0 f :: TyFun (k -> Type) (f k ~> Type) -> Type) (g :: k -> Type)

Defined in Data.Type.Functor.Product

type Apply (ProdSym0 f :: TyFun (k -> Type) (f k ~> Type) -> Type) (g :: k -> Type) = ProdSym1 f g

data ProdSym1 (f :: Type -> Type) :: (k -> Type) -> f k ~> Type

Instances

type Apply (ProdSym1 f g :: TyFun (f k) Type -> Type) (as :: f k)

Defined in Data.Type.Functor.Product

type Apply (ProdSym1 f g :: TyFun (f k) Type -> Type) (as :: f k) = Prod f g as

type ProdSym2 (f :: Type -> Type) (g :: k -> Type) (as :: f k) = Prod f g as