[Agda] Record "Setters"?

[Liam O'Connor]

I can't use the labels trick (already tried that), because I'm doing a
dependent record.

> Using the manual setter implementation as below, to prevent quadratic
blowup you could structure the record into subrecords.

What do you mean by that? I'm not opposed to writing setters if they'll be
short.

Cheers.
~Liam


On 10 May 2011 18:15, Andreas Abel <andreas.abel at ifi.lmu.de> wrote:

> Hi Liam,
>
> you can model non-dependent records, as those below, as functions from
> labels, e.g.
>
> data BlahLabels : Set where Foo Bar Baz : BlahLabels
>
> BlahTypes : BlahLabels -> Set
> BlahTypes Foo = FooT
> BlahTypes Bar = BarT
> BlahTypes Baz = BazT
>
> -- the record type
> Blah : Set
> Blah = (l : BlahLabels) -> BlahTypes l
>
> -- the constructor
> blah : FooT -> BarT -> BazT -> Blah
> blah foo bar baz Foo = foo
> blah foo bar baz Bar = bar
> blah foo bar baz Baz = baz
>
> -- individual field update
> set : Blah -> (l : BlahLabels) -> BlahTypes l -> Blah
> set r Foo x Foo = x
> set r Bar x Bar = x
> set r Baz x Baz = x
> set r _   x l   = r l
>
> For dependent records, this does not work, since one would need very
> dependent function types.
>
> You could do something with the new meta-programming facility, though.
> Nicolas Pouillard might be able to help you with that.
>
>
> 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.
>
> Cheers,
> Andreas
>
>
> On 10.05.11 8:05 AM, Liam O'Connor wrote:
>
>> 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).
>>
>
>
> --
> Andreas Abel  <><      Du bist der geliebte Mensch.
>
> Theoretical Computer Science, University of Munich
> Oettingenstr. 67, D-80538 Munich, GERMANY
>
> andreas.abel at ifi.lmu.de
> http://www2.tcs.ifi.lmu.de/~abel/
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110510/77a44dea/attachment.html