Safe Haskell	None
Language	Haskell2010

Data.Vinyl.Core

Synopsis

data Rec :: (u -> *) -> [u] -> * where
- RNil :: Rec f '[]
- (:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs)
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
- Dict :: c a => a -> Dict c a
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 :: *.

Constructors

RNil :: Rec f '[]
(:&) :: !(f r) -> !(Rec f rs) -> Rec f (r ': rs) infixr 7

Instances

RecElem (Rec :: (a -> ) -> [a] -> ) (r :: a) (r ': rs :: [a]) Z Source #
Instance details Defined in Data.Vinyl.Lens Methods rlens :: Functor g => sing r -> (f r -> g (f r)) -> Rec f (r ': rs) -> g (Rec f (r ': rs)) Source # rget :: sing r -> Rec f (r ': rs) -> f r Source # rput :: f r -> Rec f (r ': rs) -> Rec f (r ': rs) Source #
(RIndex r (s ': rs) ~ S i, RElem r rs i) => RecElem (Rec :: (a -> ) -> [a] -> ) (r :: a) (s ': rs :: [a]) (S i) Source #
Instance details Defined in Data.Vinyl.Lens Methods rlens :: Functor g => sing r -> (f r -> g (f r)) -> Rec f (s ': rs) -> g (Rec f (s ': rs)) Source # rget :: sing r -> Rec f (s ': rs) -> f r Source # rput :: f r -> Rec f (s ': rs) -> Rec f (s ': rs) Source #
TestCoercion f => TestCoercion (Rec f :: [u] -> *) Source #
Instance details Defined in Data.Vinyl.Core Methods testCoercion :: Rec f a -> Rec f b -> Maybe (Coercion a b) #
TestEquality f => TestEquality (Rec f :: [u] -> *) Source #
Instance details Defined in Data.Vinyl.Core Methods testEquality :: Rec f a -> Rec f b -> Maybe (a :~: b) #
RecSubset (Rec :: (k -> ) -> [k] -> ) ([] :: [k]) (ss :: [k]) ([] :: [Nat]) Source #
Instance details Defined in Data.Vinyl.Lens Methods rsubset :: Functor g => (Rec f [] -> g (Rec f [])) -> Rec f ss -> g (Rec f ss) Source # rcast :: Rec f ss -> Rec f [] Source # rreplace :: Rec f [] -> Rec f ss -> Rec f ss Source #
(RElem r ss i, RSubset rs ss is) => RecSubset (Rec :: (k -> ) -> [k] -> ) (r ': rs :: [k]) (ss :: [k]) (i ': is) Source #
Instance details Defined in Data.Vinyl.Lens Methods rsubset :: Functor g => (Rec f (r ': rs) -> g (Rec f (r ': rs))) -> Rec f ss -> g (Rec f ss) Source # rcast :: Rec f ss -> Rec f (r ': rs) Source # rreplace :: Rec f (r ': rs) -> Rec f ss -> Rec f ss Source #
(Eq (f r), Eq (Rec f rs)) => Eq (Rec f (r ': rs)) Source #
Instance details Defined in Data.Vinyl.Core Methods (==) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool # (/=) :: Rec f (r ': rs) -> Rec f (r ': rs) -> Bool #
Eq (Rec f ([] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods (==) :: Rec f [] -> Rec f [] -> Bool # (/=) :: Rec f [] -> Rec f [] -> Bool #
(Ord (f r), Ord (Rec f rs)) => Ord (Rec f (r ': rs)) Source #
Instance details 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) #
Ord (Rec f ([] :: [u])) Source #
Instance details 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 [] #
RecAll f rs Show => Show (Rec f rs) Source #	Records may be shown insofar as their points may be shown. `reifyConstraint` is used to great effect here.
Instance details Defined in Data.Vinyl.Core Methods showsPrec :: Int -> Rec f rs -> ShowS # show :: Rec f rs -> String # showList :: [Rec f rs] -> ShowS #
(Monoid (f r), Monoid (Rec f rs)) => Semigroup (Rec f (r ': rs)) Source #
Instance details 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) #
Semigroup (Rec f ([] :: [u])) Source #
Instance details 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 [] #
(Monoid (f r), Monoid (Rec f rs)) => Monoid (Rec f (r ': rs)) Source #
Instance details 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) #
Monoid (Rec f ([] :: [u])) Source #
Instance details Defined in Data.Vinyl.Core Methods mempty :: Rec f [] # mappend :: Rec f [] -> Rec f [] -> Rec f [] # mconcat :: [Rec f []] -> Rec f [] #
(Storable (f r), Storable (Rec f rs)) => Storable (Rec f (r ': rs)) Source #
Instance details 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 () #
Storable (Rec f ([] :: [u])) Source #
Instance details 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 () #

rappend :: Rec f as -> Rec f bs -> Rec f (as ++ bs) Source #

Two records may be pasted together.

(<+>) :: Rec f as -> Rec f bs -> Rec f (as ++ bs) infixr 5 Source #

A shorthand for rappend.

rmap :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs Source #

Rec _ rs with labels in kind u gives rise to a functor Hask^u -> Hask; that is, a natural transformation between two interpretation functors f,g may be used to transport a value from Rec f rs to Rec g rs.

(<<$>>) :: (forall x. f x -> g x) -> Rec f rs -> Rec g rs infixl 8 Source #

A shorthand for rmap.

(<<&>>) :: Rec f rs -> (forall x. f x -> g x) -> Rec g rs Source #

An inverted shorthand for rmap.

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.

(<<*>>) :: Rec (Lift (->) f g) rs -> Rec f rs -> Rec g rs infixl 8 Source #

A shorthand for rapply.

class RecApplicative rs where Source #

Given a section of some functor, records in that functor of any size are inhabited.

Minimal complete definition

rpure

Methods

rpure :: (forall x. f x) -> Rec f rs Source #

Instances

RecApplicative ([] :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpure :: (forall (x :: u0). f x) -> Rec f [] Source #
RecApplicative rs => RecApplicative (r ': rs :: [u]) Source #
Instance details Defined in Data.Vinyl.Core Methods rpure :: (forall (x :: u0). f x) -> Rec f (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.

rzipWith :: (forall x. f x -> g x -> h x) -> forall xs. Rec f xs -> Rec g xs -> Rec h xs Source #

Given a natural transformation from the product of f and g to h, we have a natural transformation from the product of Rec f and Rec g to Rec h. You can also think about this operation as zipping two records with the same element types but different interpretations.

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.

data Dict c a where Source #

Wrap up a value with a capability given by its type

Constructors

Dict :: c a => a -> Dict c a

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.