[Agda] Record "Setters"?

[Andreas Abel]

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.

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

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/