Safe Haskell | None |
---|---|
Language | Haskell2010 |
- (<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs)
- (<<*>>) :: Rec (Lift (->) f g) rs -> 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
- data Rec :: (u -> *) -> [u] -> * where
- type (∈) r rs = RElem r rs (RIndex r rs)
- type (⊆) rs ss = RSubset rs ss (RImage rs ss)
- type (≅) rs ss = REquivalent rs ss (RImage rs ss) (RImage ss rs)
- type (<:) rs ss = rs ⊆ ss
- type (:~:) rs ss = rs ≅ ss
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 :: *
.
TestCoercion u f => TestCoercion [u] (Rec u f) Source # | |
TestEquality u f => TestEquality [u] (Rec u f) 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)) => 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 # | |
type (⊆) rs ss = RSubset rs ss (RImage rs ss) Source #
A shorthand for RSubset
which supplies its image.
type (≅) rs ss = REquivalent rs ss (RImage rs ss) (RImage ss rs) Source #
A shorthand for REquivalent
which supplies its images.