Extensible records/row polymorphism are features not implemented in Haskell. Some other functional languages do it, like Purescript. GHC extensions allowing type level-programming allow us to encode them in Haskell.

Let us define records as a (partial) mapping from names (fields, wich are static) to values.

There are many implementations out there. This is yet another one, inspired in the HList library. It arose when programming the AspectAG library. Before, we depended on HList. Then we choose to implement a record library from scratch for two reasons:

• HList is experimental, it does not maintain a stable interface.
• We prefer a solution that fits better in our use case.

AspectAG is a library to encode type safe attribute grammars. Statically checked extensible records are used everywhere, knowing at compile time the structure of the grammar, and checking if it is well-formed.

Some example structures in AspectAG library are:

• Records: that's it, plane extensible records: Mappings from names to values.
• Attributions: mappings from attribute names to values. This is the same idea that the one for records, but we wanted to have different types for each structure, and for each label. This means that our labels must be polyinded.
• Children Records: That is a map from children to attibutions. It is a record of records.

One common way to implement a record is by using a GADT. For instance indexed by the list of pairs (label, value). We want labels polykinded, and values are usually of kind Type, what makes sense since Type is the kind of inhabited types, and records store values. However, in cases such as our children records, where we store attributions that are also represented by an indexed GADT, we would like to be able to reflect some of this structural information at the indexes of the record. This can be achieved if we are polymorphic in the kind of the types corresponding to the record fields.