-
Notifications
You must be signed in to change notification settings - Fork 58
New issue
Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.
By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.
Already on GitHub? Sign in to your account
"record {elem_name} record_name" to access elements in a record #288
Comments
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 infixr 0 >>>
(>>>) : (a -> b) -> (b -> c) -> (a -> c)
f >>> g = \ x => g (f x)
getNestedSubElement : MyRecord -> Nat
getNestedSubElement myRec = nested >>> subElement $ myRec |
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. |
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. |
I guess one way to do it would be to unify records and namespaces to some extent? |
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? |
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:The text was updated successfully, but these errors were encountered: