Hi All,<div><br></div><div>In Haskell, if I make a record:</div><div><br></div><div>data Foo = Foo { x :: Bar, y :: Baz }</div><div><br></div><div>Then I'm automatically able to "set" values on those records:</div>
<div><br></div><div>blerp = Foo { x = 12, y = 13 }</div><div><br></div><div>blarp = blerp { x = 13} -- y is also 13.</div><div><br></div><div>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:</div>
<div><br></div><div>record Blah : Set where</div><div> field</div><div> foo : FooT</div><div> bar : BarT</div><div> baz : BazT</div><div><br></div><div> setFoo : FooT -> Blah</div><div> setFoo x = record { foo = x ; bar = bar ; baz = baz }</div>
<div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div> setBar : BarT -> Blah</div><div> setBar x = record { foo = foo ; bar = x ; baz = baz }</div></div><div><br></div><div><meta http-equiv="content-type" content="text/html; charset=utf-8"><div>
setBaz : BazT -> Blah</div><div> setBaz x = record { foo = foo ; bar = bar ; baz = x }</div></div><div><br></div><div>Is there any better way to do this? Any ideas?</div><div><br></div><div>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).</div>
<div><br></div><div>Cheers.<br>~Liam<br>
</div>