Safe Haskell  None 

Language  Haskell2010 
Synopsis
 data Rec :: (u > *) > [u] > * where
 rappend :: Rec f as > Rec f bs > Rec f (as ++ bs)
 (<+>) :: Rec f as > Rec f bs > Rec f (as ++ bs)
 rmap :: (forall x. f x > g x) > Rec f rs > Rec g rs
 (<<$>>) :: (forall x. f x > g x) > Rec f rs > Rec g rs
 (<<&>>) :: Rec f rs > (forall x. f x > g x) > Rec g rs
 rapply :: Rec (Lift (>) f g) rs > Rec f rs > Rec g rs
 (<<*>>) :: Rec (Lift (>) f g) rs > Rec f rs > Rec g rs
 class RecApplicative rs where
 rtraverse :: Applicative h => (forall x. f x > h (g x)) > Rec f rs > h (Rec g rs)
 rzipWith :: (forall x. f x > g x > h x) > forall xs. Rec f xs > Rec g xs > Rec h xs
 rfoldMap :: forall f m rs. Monoid m => (forall x. f x > m) > Rec f rs > m
 recordToList :: Rec (Const a) rs > [a]
 data Dict c a where
 reifyConstraint :: RecAll f rs c => proxy c > Rec f rs > Rec (Dict c :. f) rs
 rpureConstrained :: forall c (f :: u > *) proxy ts. (AllConstrained c ts, RecApplicative ts) => proxy c > (forall a. c a => f a) > Rec f ts
 rpureConstraints :: forall cs (f :: * > *) proxy ts. (AllAllSat cs ts, RecApplicative ts) => proxy cs > (forall a. AllSatisfied cs a => f a) > Rec f ts
Documentation
data Rec :: (u > *) > [u] > * where Source #
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 :: *
.
Instances
RecElem (Rec :: (a > *) > [a] > *) (r :: a) (r ': rs :: [a]) Z Source #  
(RIndex r (s ': rs) ~ S i, RElem r rs i) => RecElem (Rec :: (a > *) > [a] > *) (r :: a) (s ': rs :: [a]) (S i) Source #  
TestCoercion f => TestCoercion (Rec f :: [u] > *) Source #  
Defined in Data.Vinyl.Core  
TestEquality f => TestEquality (Rec f :: [u] > *) Source #  
Defined in Data.Vinyl.Core  
RecSubset (Rec :: (k > *) > [k] > *) ([] :: [k]) (ss :: [k]) ([] :: [Nat]) Source #  
(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k > *) > [k] > *) (r ': rs :: [k]) (ss :: [k]) (i ': is) Source #  
(Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) Source #  
Eq (Rec f ([] :: [u])) Source #  
(Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) Source #  
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])) Source #  
Defined in Data.Vinyl.Core  
RecAll f rs Show => Show (Rec f rs) Source #  Records may be shown insofar as their points may be shown.

(Monoid (f r), Monoid (Rec f rs)) => Semigroup (Rec f (r ': rs)) Source #  
Semigroup (Rec f ([] :: [u])) Source #  
(Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) Source #  
Monoid (Rec f ([] :: [u])) Source #  
(Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) Source #  
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])) Source #  
Defined in Data.Vinyl.Core 
rapply :: Rec (Lift (>) f g) rs > Rec f rs > Rec g rs Source #
A record of components f r > g r
may be applied to a record of f
to
get a record of g
.
class RecApplicative rs where Source #
Given a section of some functor, records in that functor of any size are inhabited.
Instances
RecApplicative ([] :: [u]) Source #  
Defined in Data.Vinyl.Core  
RecApplicative rs => RecApplicative (r ': rs :: [u]) Source #  
Defined in Data.Vinyl.Core 
rtraverse :: Applicative h => (forall x. f x > h (g x)) > Rec f rs > h (Rec g rs) Source #
A record may be traversed with respect to its interpretation functor. This can be used to yank (some or all) effects from the fields of the record to the outside of the record.
rfoldMap :: forall f m rs. Monoid m => (forall x. f x > m) > Rec f rs > m Source #
Map each element of a record to a monoid and combine the results.
recordToList :: Rec (Const a) rs > [a] Source #
A record with uniform fields may be turned into a list.
Wrap up a value with a capability given by its type
reifyConstraint :: RecAll f rs c => proxy c > Rec f rs > Rec (Dict c :. f) rs Source #
Sometimes we may know something for all fields of a record, but when
you expect to be able to each of the fields, you are then out of luck.
Surely given ∀x:u.φ(x)
we should be able to recover x:u ⊢ φ(x)
! Sadly,
the constraint solver is not quite smart enough to realize this and we must
make it patently obvious by reifying the constraint pointwise with proof.
rpureConstrained :: forall c (f :: u > *) proxy ts. (AllConstrained c ts, RecApplicative ts) => proxy c > (forall a. c a => f a) > Rec f ts Source #
Build a record whose elements are derived solely from a constraint satisfied by each.
rpureConstraints :: forall cs (f :: * > *) proxy ts. (AllAllSat cs ts, RecApplicative ts) => proxy cs > (forall a. AllSatisfied cs a => f a) > Rec f ts Source #
Build a record whose elements are derived solely from a list of constraint constructors satisfied by each.