Feature Question: Traversal for Record

[junjihashimoto]

lens of dex is iso like #foo .
https://google-research.github.io/dex-lang/prelude.html#s-42

When define RGB as follows, how do we describe the lens to get Fin 3 => Fin 8 => Float32 of #r axis from Fin 3 => Fin 8 => RGB Float32?

data RGB n:Type = MkRGB { r: n & g : n & b : n }

Is it possible to use overField to add +1 to the #r element?
Does dex have traversal of lens?

[junjihashimoto]

In this case, I may have to define Iso (in 3 => Fin 8 => RGB Float32) (RGB (Fin 3 => Fin 8 => Float32)).

[junjihashimoto]

Is it better to use map (map (getAt #r)) without considering the troublesome things such as the cost of loop?

[apaszke]

Well, you will not escape loops if you want to map an array, but the whole point of Dex is to allow you to write out the loops without having to worry that they're going to be inefficient! So if map (map (getAt #r)) type-checks, then it's likely what you want.

[junjihashimoto]

Thank you for your comments!
We can avoid difficult index operations by using lens for pytorch or matlab, but we don't even need it for dex.
Dex is excellent!

I'll explore the binding from haskell and see how to manage resources of dex.

[apaszke]

Thanks, I'm glad you're as excited as we are! Let me know if we can help in any way. Are you planning to make it a DSL, or to expose an interface that takes Dex programs as strings?

[junjihashimoto]

dex is implemented in haskell.
So I'm thinking of making a DSL, and the DSL will output the data-types of Syntax.hs.
https://github.com/google-research/dex-lang/blob/main/src/lib/Syntax.hs