[Agda] Record "Setters"?

[Andreas Abel]

On 5/10/11 1:58 PM, Liam O'Connor wrote:
>
> 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.

Well, I did not complain that "my code size grows quadratically"... ;-)

-- Andreas

> On 10 May 2011 18:15, Andreas Abel <andreas.abel at ifi.lmu.de
> <mailto: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/