Records

Definitions

RecordSpec : Type -> Type

  Specification for a record, consisting of a list of key value pairs, where the value is the specification for that field.

Visibility: public export

data RecordField : String -> Type -> Type

  A field (label value pair) in the record, with the given label and
  type.  The label is erased at the value level, but included to
  make it easy to see which field is used in the code.

Totality: total
Visibility: public export
Constructor: 

(:->) : (0 s : String) -> t -> RecordField s t

data Field : String -> Type -> Type

  A field definition for a given label.

Totality: total
Visibility: public export
Constructor: 

(:->:) : (s : String) -> t -> Field s t

FieldSpec : Field s t -> t

  Get the specification for a single field.

Visibility: public export

FieldToType : Type -> Type

  The actual type of a field in the record.

Visibility: public export

data Record : RecordSpec k -> FieldToType k -> Type

  A strongly specified record.  The type contains the specification,
  and a function mapping that specification for each field to a
  concrete type.

Totality: total
Visibility: public export
Constructors:

Nil : {0 f : FieldToType k} -> Record [] (\{s:894} => f)

(::) : {0 f : FieldToType k} -> RecordField lbl (f (lbl :->: t)) -> Record xs (\{s:920} => f) -> Record ((lbl, t) :: xs) (\{s:928} => f)

SimpleRecord : RecordSpec Type -> Type

  Simple record with types as specification

Visibility: public export

AllConstraints : (a -> Type) -> List a -> Type

  Constraint that holds for all values in a list.

Visibility: public export

data HasField : String -> k -> RecordSpec k -> Type

  proof that the spec has some label with the given spec

Totality: total
Visibility: public export
Constructors:

FirstField : HasField s t ((s, t) :: {_:1009})

NextField : {auto 0 _ : t == s = False} -> HasField s v xs -> HasField s v ((t, w) :: xs)

Hint: 

Uninhabited (HasField s t [])

HasField' : RecordSpec k -> (String, k) -> Type

Visibility: public export

HasFields : RecordSpec k -> RecordSpec k -> Type

  Proof that a spec is a subset of another spec.

Visibility: public export

data LabelOf : RecordSpec k -> Type

  A label of a spec.  Contains a hidden (auto) proof that the label
  is actually in the RecordSpec, and a hidden reference to the field Spec.

Totality: total
Visibility: public export
Constructor: 

MkLabel : (lbl : String) -> HasField lbl t spec => LabelOf spec

labelString : LabelOf spec -> String

  Extract the string of the label

Visibility: export

labelSpec : LabelOf spec -> k

  Extract the spec from the label

Visibility: export

data IsNothing : Maybe a -> Type

Totality: total
Visibility: public export
Constructor: 

ItIsNothing : IsNothing Nothing

data HasOptionalField : String -> k -> RecordSpec k -> Type

  proof that an optional field with the given spec exists.  The spec
  must be either present with the right type, or be absent.  This is
  written in terms of HasField, so it is isomorphic to Maybe
  Natural, which has an efficient runtime representation.

Totality: total
Visibility: public export
Constructors:

NoSuchField : IsNothing (lookup s specs) => HasOptionalField s t specs

FieldExists : HasField s t specs => HasOptionalField s t specs

HasOptionalField' : RecordSpec k -> (String, k) -> Type

Visibility: public export

HasOptionalFields : RecordSpec k -> RecordSpec k -> Type

Visibility: public export

remField : RecordSpec k -> (String, k) -> RecordSpec k

Visibility: export

remFields : RecordSpec k -> RecordSpec k -> RecordSpec k

Visibility: export

data NubFields : RecordSpec k -> RecordSpec k -> RecordSpec k -> Type

Totality: total
Visibility: public export
Constructor: 

MkNubFields : NubFields spec fields (remFields spec fields)

data WithRecordFields : RecordSpec k -> RecordSpec k -> RecordSpec k -> RecordSpec k -> Type

  Proof that a record contains some mandatory fields, some optional
  fields, and some remaining fields.

Totality: total
Visibility: public export
Constructor: 

MkWithRecordFields : HasFields spec mandatory => NubFields spec (optional ++ mandatory) other => WithRecordFields spec mandatory optional other

hasFieldToIndex : HasField s t r -> Integer

  Create an integer index of the field from the HasField proof.

Visibility: export

get : (0 lbl : String) -> {0 f : FieldToType k} -> HasField lbl t r => Record r (\{s:1502} => f) -> f (lbl :->: t)

  Get a field value by label

Visibility: public export

SpecGet : (0 lbl : String) -> (r : RecordSpec k) -> HasField lbl t r => k

  Get a field specification from the RecordSpec by label

Visibility: public export

(!!) : {0 f : FieldToType k} -> Record r (\{s:1640} => f) -> (0 lbl : String) -> HasField lbl t r => f (lbl :->: t)

  Operator version of get with arguments flipped.

Visibility: export
Fixity Declaration: infixr operator, level 10

getMaybe : {0 f : FieldToType k} -> (0 s : String) -> HasOptionalField s t r => Record r (\{s:1698} => f) -> Maybe (f (s :->: t))

  Get an optional field from a spec, as Maybe value

Visibility: public export

getOpt : {0 f : FieldToType k} -> (0 s : String) -> HasOptionalField s t r => Lazy (f (s :->: t)) -> Record r (\{s:1783} => f) -> f (s :->: t)

  Get an optional field, return the given default if it is not found.

Visibility: public export

set : {0 f : FieldToType k} -> RecordField lbl (f (lbl :->: t)) -> HasField lbl t r => Record r (\{s:1839} => f) -> Record r (\{s:1846} => f)

  Set a field in a record.

Visibility: export

mapRecord : {0 f : FieldToType k} -> {0 g : FieldToType k} -> (f (lbl :->: spec) -> g (lbl :->: spec)) -> Record specs (\{s:1972} => f) -> Record specs (\{s:1979} => g)

  Map a function over all fields of a record.

Visibility: public export

sequenceRecord : Applicative m => {0 f : FieldToType k} -> Record spec (\{s:2068} => m . f) -> m (Record spec (\{s:2080} => f))

  Run all the effects for each field.

Visibility: public export

traverseRecord : Applicative m => {0 f : FieldToType k} -> {0 g : FieldToType k} -> (f (lbl :->: spec) -> m (g (lbl :->: spec))) -> Record specs (\{s:2204} => f) -> m (Record specs (\{s:2211} => g))

  Apply an effectful function over all fields of the record.

Visibility: public export

aseq : Applicative m => Record spec (\{s:2334} => m . FieldSpec) -> m (SimpleRecord spec)

  convenient specialization of sequenceRecord, to bind applicative
  values.  Useful as replacement of applicative do in haskell.

Visibility: public export

mapRecordSpec : {0 f : FieldToType k} -> (spec : RecordSpec k) -> ((label : String) -> (spec : k) -> f (label :->: spec)) -> Record spec (\{s:2384} => f)

  Create a record by applying a function over each field in the RecordSpec.

Visibility: public export

traverseRecordSpec : Applicative m => {0 f : FieldToType k} -> (spec : RecordSpec k) -> ((label : String) -> (spec : k) -> m (f (label :->: spec))) -> m (Record spec (\{s:2453} => f))

  Create a record by applying an effectful function over each field in the RecordSpec.

Visibility: public export

zipWithRecord : {0 f : FieldToType k} -> {0 g : FieldToType k} -> {0 h : FieldToType k} -> (f (s :->: a) -> g (s :->: a) -> h (s :->: a)) -> Record spec (\{s:2575} => f) -> Record spec (\{s:2584} => g) -> Record spec (\{s:2591} => h)

  Zip two records for each field in the record.

Visibility: public export

data HkdList : (k -> Type) -> List k -> Type

  Higher kinded heterogenous list

Totality: total
Visibility: public export
Constructors:

Nil : HkdList f []

(::) : f a -> HkdList f b -> HkdList f (a :: b)

mapHkd : (f a -> g a) -> HkdList f s -> HkdList g s

  map a Hkd List

Visibility: export

zipWithManyRecord : {g : FieldToType k} -> (HkdList (\{arg:0} => {arg:0} (s :->: a)) fs -> g (s :->: a)) -> HkdList (Record spec) fs -> Record spec (\{s:2997} => g)

  Zip a (heterogenous) list of records, by zipping each row over a
  function.  The function takes a list of all the values in that row
  for each of the records.

Visibility: export

foldMapRecord : Monoid m => {f : FieldToType k} -> (f (s :->: a) -> m) -> Record spec (\{s:3165} => f) -> m

  Maps each field to a value and combine them.

Visibility: export

foldrRecord : {f : FieldToType k} -> (f (s :->: a) -> acc -> acc) -> acc -> Record spec (\{s:3268} => f) -> acc

  Successively combine the fields using the provided function,
  starting with the element that is in the final position i.e. the
  right-most position.

Visibility: export

foldlRecord : {f : FieldToType k} -> (acc -> f (s :->: a) -> acc) -> acc -> Record spec (\{s:3361} => f) -> acc

  Successively combine the fields using the provided function,
  starting with the element that is in the first position i.e. the
  left-most position.

Visibility: export

recordLabels : Record spec (\{s:3427} => const String)

  create a record with all the labels of the spec.

Visibility: export

EntryDict : ((String, k) -> Type) -> FieldToType k

  Type of the interface implementation for a given field.

Visibility: public export

recordDicts : (0 c : ((String, k) -> Type)) -> (spec : RecordSpec k) -> AllConstraints c spec => Record spec (\{s:3498} => EntryDict c)

  Create a record with the interface implementations for each field of the spec.

Visibility: export

recordSpecs : (l : RecordSpec k) -> Record l (\{s:3550} => const k)

  Create a record with the specs for each field from the record spec.

Visibility: export

concatRecords : {f : FieldToType k} -> Record spec1 (\{s:3594} => f) -> Record spec2 (\{s:3603} => f) -> Record (spec1 ++ spec2) (\{s:3611} => f)

  Concatenate two records

Visibility: export

RecordSubset : List (LabelOf spec) -> RecordSpec k

  A subset of a RecordSpec, given a list of labels.

Visibility: public export

recordSubset : {f : FieldToType k} -> (labels : List (LabelOf spec)) -> Record spec (\{s:3709} => f) -> Record (RecordSubset labels) (\{s:3718} => f)

  Create a subset of a record, given a list of labels.

Visibility: export