Safe Haskell  None 

Language  Haskell2010 
 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 :: *
.
RecElem a (Rec a) r ((:) a r rs) Z Source #  
((~) Nat (RIndex a r ((:) a s rs)) (S i), RElem a r rs i) => RecElem a (Rec a) r ((:) a s rs) (S i) Source #  
TestCoercion u f => TestCoercion [u] (Rec u f) Source #  
TestEquality u f => TestEquality [u] (Rec u f) Source #  
RecSubset (k > *) k (Rec k) ([] k) ss ([] Nat) Source #  
(RElem k r ss i, RSubset k rs ss is) => RecSubset (k > *) k (Rec k) ((:) k r rs) ss ((:) Nat i is) Source #  
(Eq (f r), Eq (Rec a f rs)) => Eq (Rec a f ((:) a r rs)) Source #  
Eq (Rec u f ([] u)) Source #  
(Ord (f r), Ord (Rec a f rs)) => Ord (Rec a f ((:) a r rs)) Source #  
Ord (Rec u f ([] u)) Source #  
RecAll u f rs Show => Show (Rec u f rs) Source #  Records may be shown insofar as their points may be shown.

(Monoid (f r), Monoid (Rec a f rs)) => Semigroup (Rec a f ((:) a r rs)) Source #  
Semigroup (Rec u f ([] u)) Source #  
(Monoid (f r), Monoid (Rec a f rs)) => Monoid (Rec a f ((:) a r rs)) Source #  
Monoid (Rec u f ([] u)) Source #  
(Storable (f r), Storable (Rec a f rs)) => Storable (Rec a f ((:) a r rs)) Source #  
Storable (Rec u f ([] u)) Source #  
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.
RecApplicative u ([] u) Source #  
RecApplicative u rs => RecApplicative u ((:) u r rs) Source #  
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.