[Agda] Record "Setters"?

[Liam O'Connor]

Hi All,

In Haskell, if I make a record:

data Foo = Foo { x :: Bar, y :: Baz }

Then I'm automatically able to "set" values on those records:

blerp = Foo { x = 12, y = 13 }

blarp = blerp { x = 13} -- y is also 13.

Does agda have equivalent functionality? Writing these setters manually
means my code size grows quadratically in the amount of fields in the
record, as I have to write:

record Blah : Set where
   field
      foo : FooT
      bar : BarT
      baz : BazT

   setFoo : FooT -> Blah
   setFoo x = record { foo = x ; bar = bar ; baz = baz }

   setBar : BarT -> Blah
   setBar x = record { foo = foo ; bar = x ; baz = baz }

   setBaz : BazT -> Blah
   setBaz x = record { foo = foo ; bar = bar ; baz = x }

Is there any better way to do this? Any ideas?

If there is no easy way to do this, how hard would it be to add such
functionality to Agda? All you'd have to do is (perhaps at option) generate
setX functions as I have above. I might even write the patch if Agda's code
is easy enough for me to figure out (I have some experience with PLs work).

Cheers.
~Liam
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110510/ad011f82/attachment.html