Record projection

[Bowuigi]

Projecting field names and accessing them even with unknown records would be a nice change. At the very least, functions that could lead to a definition of:

recordToList :: Record r -> List {key : Text, value : a}

Where all the values in r have the type a. This would be specially useful when writing config files, since it would quickly automate the creation of subsections with something like:

-- We render to a INI-like format
let Color = Text -- (bad practice because proper practice requires either a lot of boilerplate and more advanced types)
let Path = Text
textStyling : {color : Color, font : Path} -> Text
textStyling = r -> listFold (x y -> x ++ y) (listMap ({key, value} -> key ++ "=" ++ value ++ "\n") (recordToList r))

Note that the type annotation of textStyling could be removed, getting a Record r -> Text function that renders text records into a INI-ish format.

[Bowuigi]

For something more general, more complex types are needed, particularly, treating labels as "type level strings" and quantifying over them, for example:

recordMap : forall k v. Label k => {k : a} -> (a -> b) -> {k : b}

Some semantics:

Label k => {k : a} a closed record only filled with values of type a, but with arbitrary labels

Label k => {k : a | r} a record having at least one value of type a, with r being the rest of the record, that is, the key-value pairs that don't have a value of type a. (Note that r could be empty)

Label k => {thing : a, k : b} a closed record with a label thing whose value has type a and at least one entry with type b.

The last two can be combined.

With what appears to be dependent typeclass constraints, you can do cooler stuff like converting every Show-able value into Text inside the record, to then use recordToList and get a rendered config file, for example:

mapConstrained : forall v. (c : Constraint) -> (c v => v -> fv) -> (forall k. Label k => c v => {k : v} -> {k : fv})

The types get really complex here, but the benefits are pretty neat.

If this project is unmaintained, some pointers on how to get to label quantifiers or at least recordToList would be heavily appreciated

[willtim]

Hi, unfortunately this project is no longer being actively developed, although I still accept small patches. The feature you describe is of course a very big change, it's often called "first-class labels" in the literature. Daan Leijen has a very readable paper proposing a system for first-class labels here: https://www.microsoft.com/en-us/research/publication/first-class-labels-for-extensible-rows/ I am sure this project could be forked and the row types system updated, but it would be a complete reworking of how records and variants worked.

[Bowuigi]

Thanks! I will check that out