"record {elem_name} record_name" to access elements in a record

[vfrinken]

I would like to have an efficient way to access elements in records and nested sub-records, lust like in Idris 1. This works for updating elements { ... = ...}, resp. {... $= ...}, but simply extracting the wanted element doesn't work. In short, I would like this:

record NestedRecord where
    constructor MkNestedRecord
    subElement : Nat

record MyRecord where
    constructor MkMyRecord
    nested : NestedRecord

getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = record {nested->subElement} myRec

[gallais]

Is function composition not adequate in this situation?

getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = subElement . nested $ myRec

If you want to go left-to-right, you can use F#'s "pipe forward"

infixl 0 |>
(|>) : a -> (a -> b) -> b
x |> f = f x

getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = myRec |> nested |> subElement

Lastly you could use Haskell's flipped composition operator if you want left-to-right but insist on keeping the record at the end:

infixr 0 >>>
(>>>) : (a -> b) -> (b -> c) -> (a -> c)
f >>> g = \ x => g (f x)

getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = nested >>> subElement $ myRec

[vfrinken]

Yes, function composition is adequate, it's mostly a convenience issue to not change code written for Idris 1.

So if it is too much of a hassle to add it, then please don't bother.

[edwinb]

I wonder if we should also find a way to do record access by dots. I couldn't see how to fix the syntax to support it, but the Haskell people have worked out a way to do it so maybe we should look into it too... it's something that would be nice for interactive editing especially.

[clayrat]

I guess one way to do it would be to unify records and namespaces to some extent?

[alrunner4]

Maybe I'm an outlier, but I always enjoyed using RecordWildcards more than the other Haskell records solutions. Doesn't simplify the case of multiple same-typed records in a scope, though. Perhaps the distance between records and interfaces can be narrowed now that we can use the fat arrow for both interfaces and auto implicits?