Data.Record

Record core support.

Record basics

A record is a list of name-value pairs. Such pairs are called fields and are constructed using the data constructor (:=). Records are built from fields using the data constructors X (for the empty record) and (:&) (for non-empty records that consist of an initial record and a last field each). For example, the following expression denotes a record that contains some information about the author of these lines:

X :& Surname := "Jeltsch" :& Age := 33 :& Room := "HG/2.39"

The type of a record has the form r s where r is a record scheme and s is a representation of a type-level function, called the record style. A record scheme is a list of name-sort pairs, which correspond to the name-value pairs of the record. The type constructors X and (:&) are used to form record schemes. Name-sort pairs are constructed using the type constructor (:::).

The name of a name-sort pair equals the name of the corresponding record field. Applying the style to the sort yields the type of the corresponding field value. For example, the above record has the following type:

(X :& Surname ::: String :& Age ::: Int :& Room ::: String) (Id KindStar)

If we replace the type Id KindStar by Id KindStar :-> Id KindStar, we get a type that covers all records with a Surname, an Age, and a Room field that contain values of type String -> String, Int -> Int, and String -> String, respectively. So by varying the style, we can generate a family of related record types from a single record scheme.

data X style

The empty record scheme.

Constructors

X

The empty record.

Instances

Convertible rec X

Kind kind => Record kind X

Show (X style)

data (rec :& field) style

Non-empty record schemes.

Constructors

!(rec style) :& !(field style)

Non-empty records.

Instances

(Separation rec remain name' sort', Convertible remain rec') => Convertible rec (:& rec' (::: name' sort'))

(Record kind rec, Name name, Inhabitant kind sort) => Record kind (:& rec (::: name sort))

(:& remain (::: name sort) ~ extRemain, Separation rec remain sepName sepSort) => Separation (:& rec (::: name sort)) extRemain sepName sepSort

(sort ~ sepSort, Name name) => Separation (:& rec (::: name sort)) rec name sepSort

(Show (rec style), Show name, Show (App style sort)) => Show (:& rec (::: name sort) style)

data (name ::: sort) style

The type of record fields.

Constructors

!name := (App style sort)

Constructs a record field from a name and a value.

Instances

(Separation rec remain name' sort', Convertible remain rec') => Convertible rec (:& rec' (::: name' sort'))

(Record kind rec, Name name, Inhabitant kind sort) => Record kind (:& rec (::: name sort))

(:& remain (::: name sort) ~ extRemain, Separation rec remain sepName sepSort) => Separation (:& rec (::: name sort)) extRemain sepName sepSort

(sort ~ sepSort, Name name) => Separation (:& rec (::: name sort)) rec name sepSort

(Show name, Show (App style sort)) => Show (::: name sort style)

(Show (rec style), Show name, Show (App style sort)) => Show (:& rec (::: name sort) style)

class Name name where

The class of name types. For each field name N, there should be a declaration of the following form:

data N = N deriving (Show)

That way, the name can be represented in types by the type constructor N, and in expressions and patterns by the data constructor N. Furthermore, the following instance declaration should be added:

instance Name N where
 
    name = N

Such instance declarations allow record combinators to construct value-level representations of names from type-level representations.

Methods

name :: name

The sole inhabitant of the name type.

class Kind kind => Record kind rec where

An instance Record k r exists if and only if r is a record scheme whose sorts are of the subkind represented by k.

Methods

fold

Arguments

:: thing X

the definition of the combinator for the empty record scheme

-> (forall rec name. (Record kind rec, Name name) => All kind (Expander thing rec name))

turns the definition of the combinator for a record scheme r into the definition for any record scheme r :& n ::: s

-> thing rec

the resulting combinator that works for all record schemes

Folding of record schemes. This function can be used to define combinators whose types have the form (Record rec) => t rec by induction on the rec parameter.

Instances

Kind kind => Record kind X

(Record kind rec, Name name, Inhabitant kind sort) => Record kind (:& rec (::: name sort))

newtype Expander thing rec name sort

Transformations from the definition of a record combinator for some record scheme into its definition for an expanded record scheme.

Constructors

Expander (thing rec -> thing (rec :& (name ::: sort)))

Record conversion

Records are lists, so their fields are totally ordered. This order can be used to distinguish fields that have the same name. For each name, we index the fields of this name from right to left. We identify a field by its name and its index. However, the order of fields with different names is superfluous. Therefore, it is worthwhile that it can be modified. Furthermore, it is often beneficial if unnecessary fields can be ignored. That way, record operations can be made more general since they can also work with records that contain more than the expected fields.

Record conversion reorders and drops fields in such a way that all remaining fields keep their identification. So record conversion keeps the order of fields that share a common name, and it drops a field only if all preceding fields of the same name are also dropped. The scheme of the destination record is generated from the scheme of the source record by applying the same reorderings and droppings that are used to transform the source record into the destination record. The style is not changed.

class Convertible rec rec' where

An instance Convertible r r' exists if and only if r and r' are record schemes, and records of a type r s can be converted into records of the type r' s.

Methods

convert :: rec style -> rec' style

Converts a record into another record.

Instances

Convertible rec X

(Separation rec remain name' sort', Convertible remain rec') => Convertible rec (:& rec' (::: name' sort'))

Field separation

class Name sepName => Separation rec remain sepName sepSort | rec sepName -> remain sepSort where

An instance Separation r r' n s exists if and only if the following conditions are met:

• r is a record scheme that contains the name n.
• The last name-sort pair with the name n contains the sort s.
• Removing that name-sort pair from r yields r'.

Methods

separate :: rec style -> (remain style, (sepName ::: sepSort) style)

Extracts the last field of the respective name and returns the remaining record and the extracted field.

Instances

(:& remain (::: name sort) ~ extRemain, Separation rec remain sepName sepSort) => Separation (:& rec (::: name sort)) extRemain sepName sepSort

(sort ~ sepSort, Name name) => Separation (:& rec (::: name sort)) rec name sepSort