<meta http-equiv="content-type" content="text/html; charset=utf-8"><div><br></div><div>I can't use the labels trick (already tried that), because I'm doing a dependent record.</div><br>> Using the manual setter implementation as below, to prevent quadratic blowup you could structure the record into subrecords.<div>
<br></div><div>What do you mean by that? I'm not opposed to writing setters if they'll be short. </div><div><br clear="all">Cheers.<br>~Liam<br>
<br><br><div class="gmail_quote">On 10 May 2011 18:15, Andreas Abel <span dir="ltr"><<a href="mailto:andreas.abel@ifi.lmu.de">andreas.abel@ifi.lmu.de</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex;">
Hi Liam,<br>
<br>
you can model non-dependent records, as those below, as functions from labels, e.g.<br>
<br>
data BlahLabels : Set where Foo Bar Baz : BlahLabels<br>
<br>
BlahTypes : BlahLabels -> Set<br>
BlahTypes Foo = FooT<br>
BlahTypes Bar = BarT<br>
BlahTypes Baz = BazT<br>
<br>
-- the record type<br>
Blah : Set<br>
Blah = (l : BlahLabels) -> BlahTypes l<br>
<br>
-- the constructor<br>
blah : FooT -> BarT -> BazT -> Blah<br>
blah foo bar baz Foo = foo<br>
blah foo bar baz Bar = bar<br>
blah foo bar baz Baz = baz<br>
<br>
-- individual field update<br>
set : Blah -> (l : BlahLabels) -> BlahTypes l -> Blah<br>
set r Foo x Foo = x<br>
set r Bar x Bar = x<br>
set r Baz x Baz = x<br>
set r _ x l = r l<br>
<br>
For dependent records, this does not work, since one would need very dependent function types.<br>
<br>
You could do something with the new meta-programming facility, though. Nicolas Pouillard might be able to help you with that.<br><br>
<br>
Finally, we could think about adding a native syntax for record update as in Haskell. One thing to keep in mind is that with dependent records, one might not be able to update individual fields without making the record ill-typed. Simultaneous update would be possible, of course.<br>
<br>
Cheers,<br>
Andreas<div><div></div><div class="h5"><br>
<br>
On 10.05.11 8:05 AM, Liam O'Connor wrote:<br>
<blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex">
In Haskell, if I make a record:<br>
<br>
data Foo = Foo { x :: Bar, y :: Baz }<br>
<br>
Then I'm automatically able to "set" values on those records:<br>
<br>
blerp = Foo { x = 12, y = 13 }<br>
<br>
blarp = blerp { x = 13} -- y is also 13.<br>
<br>
Does agda have equivalent functionality? Writing these setters manually<br>
means my code size grows quadratically in the amount of fields in the<br>
record, as I have to write:<br>
<br>
record Blah : Set where<br>
field<br>
foo : FooT<br>
bar : BarT<br>
baz : BazT<br>
<br>
setFoo : FooT -> Blah<br>
setFoo x = record { foo = x ; bar = bar ; baz = baz }<br>
<br>
setBar : BarT -> Blah<br>
setBar x = record { foo = foo ; bar = x ; baz = baz }<br>
<br>
setBaz : BazT -> Blah<br>
setBaz x = record { foo = foo ; bar = bar ; baz = x }<br>
<br>
Is there any better way to do this? Any ideas?<br>
<br>
If there is no easy way to do this, how hard would it be to add such<br>
functionality to Agda? All you'd have to do is (perhaps at option)<br>
generate setX functions as I have above. I might even write the patch if<br>
Agda's code is easy enough for me to figure out (I have some experience<br>
with PLs work).<br>
</blockquote>
<br>
<br></div></div><font color="#888888">
-- <br>
Andreas Abel <>< Du bist der geliebte Mensch.<br>
<br>
Theoretical Computer Science, University of Munich<br>
Oettingenstr. 67, D-80538 Munich, GERMANY<br>
<br>
<a href="mailto:andreas.abel@ifi.lmu.de" target="_blank">andreas.abel@ifi.lmu.de</a><br>
<a href="http://www2.tcs.ifi.lmu.de/~abel/" target="_blank">http://www2.tcs.ifi.lmu.de/~abel/</a><br>
</font></blockquote></div><br></div>