Composite.Record

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 :: *.

The type of regular plain records where each field has a value, equal to Rec Identity.

Bidirectional pattern matching the first field of a record using :-> values and the Identity functor.

This pattern is bidirectional meaning you can use it either as a pattern or a constructor, e.g.

  let rec = 123 :*: Just "foo" :*: RNil
      foo :*: bar :*: RNil = rec

Mnemonic: * for products.

Bidirectional pattern matching the first field of a record using :-> values and any functor.

This pattern is bidirectional meaning you can use it either as a pattern or a constructor, e.g.

  let rec = Just 123 :^: Just "foo" :^: RNil
      Just foo :^: Just bar :^: RNil = rec

Mnemonic: ^ for products (record) of products (functor).

Some value of type a tagged with a symbol indicating its field name or label. Used as the usual type of elements in a Rec or Record.

Recommended pronunciation: record val.

Convenience function to make an Identity (s :-> a) with a particular symbol, used for named field construction.

For example:

  type FFoo = "foo" :-> Int
  type FBar = "bar" :-> String
  type FBaz = "baz" :-> Double
  type MyRecord = [FFoo, FBar, FBaz]

  myRecord1 :: Record MyRecord
  myRecord1
    =  val @"foo" 123
    :& val @"bar" "foobar"
    :& val @"baz" 3.21
    :& RNil

  myRecord2 :: Record MyRecord
  myRecord2 = rcast
    $  val @"baz" 3.21
    :& val @"foo" 123
    :& val @"bar" "foobar"
    :& RNil

In this example, both myRecord1 and myRecord2 have the same value, since rcast can reorder records.

Reflect the type level name of a named value s :-> a to a Text. For example, given "foo" :-> Int, yields "foo" :: Text

Extract the value and reflect the name of a named value.

Constraint expressing that r is in rs and providing the index of r in rs. Equal to RElem rs (RIndex r rs).

Lens to a particular field of a record using the Identity functor.

For example, given:

  type FFoo = "foo" :-> Int
  type FBar = "bar" :-> String
  fBar_ :: Proxy FBar
  fBar_ = Proxy

  rec :: Rec Identity '[FFoo, FBar]
  rec = 123 :*: "hello!" :*: Nil

Then:

  view (rlens fBar_)               rec == "hello!"
  set  (rlens fBar_) "goodbye!"    rec == 123 :*: "goodbye!" :*: Nil
  over (rlens fBar_) (map toUpper) rec == 123 :*: "HELLO!"   :*: Nil

Synonym for rlensCo

Lens to a particular field of a record using any functor.

For example, given:

  type FFoo = "foo" :-> Int
  type FBar = "bar" :-> String
  fBar_ :: Proxy FBar
  fBar_ = Proxy

  rec :: Rec Maybe '[FFoo, FBar]
  rec = Just 123 :^: Just "hello!" :^: Nil

Then:

  view (rlensCo fBar_)                      rec == Just "hello!"
  set  (rlensCo fBar_) Nothing              rec == Just 123 :^: Nothing       :^: Nil
  over (rlensCo fBar_) (fmap (map toUpper)) rec == Just 123 :^: Just "HELLO!" :^: Nil

Lens to a particular field of a record using a contravariant functor.

For example, given:

  type FFoo = "foo" :-> Int
  type FBar = "bar" :-> String
  fBar_ :: Proxy FBar
  fBar_ = Proxy

  rec :: Rec Predicate '[FFoo, FBar]
  rec = Predicate even :!: Predicate (even . length) :!: Nil

Then:

  view (rlensContra fBar_)                           rec == Predicate even
  set  (rlensContra fBar_) Predicate (odd . length)  rec == Predicate even :!: Predicate (odd . length) :!: Nil
  over (rlensContra fBar_) (contramap show)          rec == Predicate even :!: Predicate (odd . length . show) :!: Nil

Type function which produces the cross product of constraints cs and types as.

For example, AllHave '[Eq, Ord] '[Int, Text] is equivalent to (Eq Int, Ord Int, Eq Text, Ord Text)

Type function which produces a constraint on a for each constraint in cs.

For example, HasInstances Int '[Eq, Ord] is equivalent to (Eq Int, Ord Int).

Type function which produces the cross product of constraints cs and the values carried in a record rs.

For example, ValuesAllHave '[Eq, Ord] '["foo" :-> Int, "bar" :-> Text] is equivalent to (Eq Int, Ord Int, Eq Text, Ord Text)

zipWith for Rec's.

Given a list of constraints cs, apply some function for each r in the target record type rs with proof that those constraints hold for r, generating a record with the result of each application.

Reify the type of a val.

Convert a provably nonempty Rec (Const a) rs to a NonEmpty a.

Class which reifies the symbols of a record composed of :-> fields as Text.

Class with rmap but which gives the natural transformation evidence that the value its working over is contained within the overall record ss.

Type function which removes the first element r from a list rs, and doesn't expand if r is not present in rs.

Constraint which reflects that an element r can be removed from rs using rdelete.

Remove an element r from a Rec f rs. Note this is just a type constrained rcast.

Widen a record from Record rs to Rec Maybe ss. Note this is just a type constrainted rdowncast.

Iso which observes that a record with a single field s with value a is isomorphic to the value alone.