Data.Vinyl.Notation

Documentation

type (:~:) r1 r2 = (r1 <: r2, r2 <: r1)

If two records types are subtypes of each other, that means that they differ only in order of fields.

(<-:) :: sing r -> f (el $ r) -> Rec el f `[r]` infixr 6

Shorthand for a record with a single field. This is useful for Applicative or Monadic intialization of records as in the idiom:

dist $ myField <-: someIO <+> yourField <-: otherIO

class xs <: ys

One record is a subtype of another if the fields of the latter are a subset of the fields of the former.

Minimal complete definition

cast

Instances

(<:) k xs ([] k)

((∈) k y xs, (<:) k xs ys) => (<:) k xs ((:) k y ys)

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

Append for records.

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

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

(=:) :: Applicative f => sing k -> (el $ k) -> Rec el f `[k]`

Shorthand for a record with a single field. Lifts the field's value into the chosen functor automatically.

(~=) :: (Eq (Rec el f xs), xs :~: ys) => Rec el f xs -> Rec el f ys -> Bool

Term-level record congruence.

data Rec el f rrs where

A record is parameterized by a universe u, list of rows rs, a large elimination el, and a type constructor f to be applied to the interpretation el r of each of those r.

Constructors

(:&) :: !(f (el $ r)) -> !(Rec el f rs) -> Rec el f (r : rs) infixr 9

Instances

(Eq (f (($) * k el r)), Eq (Rec k el f rs)) => Eq (Rec k el f ((:) k r rs))

Eq (Rec k el f ([] k))

(Storable (($) * k el r), Storable (Rec k el Identity rs)) => Storable (Rec k el Identity ((:) k r rs))

Storable (Rec k el Identity ([] k))

(Monoid (($) * k el r), Monoid (Rec k el f rs), Applicative f) => Monoid (Rec k el f ((:) k r rs))

Monoid (Rec k el f ([] k))

FoldRec (Rec k el f ([] k)) a

((~) * t (($) * k el r), FoldRec (Rec k el f rs) (f t)) => FoldRec (Rec k el f ((:) k r rs)) (f t)

data Semantics

Constructors

forall s t . (TyRep t, TyRep s) => t :~> s