[Agda] Automatic conversion between records and iterated Sigma types

[Jesper Cockx]

Hi Jacques,

No, I was thinking of the other direction: if you define a record type in
Agda, then a macro could automatically turn it into its representation as
an iterated sigma type, and automatically generate the conversion functions
back and forth.

-- Jesper

On Tue, Apr 14, 2020 at 7:38 PM Jacques Carette <carette at mcmaster.ca> wrote:

> Thanks Jesper.
>
> I don't think I fully follow though.  Is it possible to use reflection to
> take in a (nested) Sigma type (say the one for Monoid) and return the
> declaration of the associated record type?  Could I take the name of the
> bound variables in that Sigma type as the labels of the resulting record
> type?  That would be perfect.  I did not think that was possible. I would
> love to be wrong here!
>
> Jacques
> On 2020-04-14 4:07 a.m., Jesper Cockx wrote:
>
> Hi Jacques,
>
> Note that it *is* possible to generate fresh names from Agda's reflection
> machinery, it is just not possible to access those generated names from
> outside of the macro call. But if you're willing to give just one name
> manually to the top-level definition (e.g. a value of a record type
> containing fields for the iterated sigma type itself, functions converting
> back and forth, and proofs about them) then the current reflection
> machinery should work just fine. In particular, there should be no need to
> generate new datatypes, which is the main bottleneck in #3699.
>
> -- Jesper
>
> On Mon, Apr 13, 2020 at 9:20 PM Jacques Carette <carette at mcmaster.ca>
> wrote:
>
>> Very hard, I believe.  Lines 1113 and 1114
>>
>>    let u := fresh "u" in
>>    let v := fresh "v" in
>>
>> in particular.  See the comment by @jespercockx on
>> https://github.com/agda/agda/issues/3699.
>>
>> Jacques
>>
>> On 2020-04-13 3:11 p.m., Bas Spitters wrote:
>> > This is what the issig tactic does in the HoTT library. I don't know
>> > how difficult it is to convert it to agda.
>> > https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v
>> >
>> > On Mon, Apr 13, 2020 at 8:47 PM Martin Escardo <m.escardo at cs.bham.ac.uk>
>> wrote:
>> >> Is it possible to write a tactic to convert between records and
>> >> equivalent iterated Sigma types? And, if so, to also produce code to
>> >> establish their equivalence?
>> >>
>> >> Thanks,
>> >> Martin
>> >> _______________________________________________
>> >> Agda mailing list
>> >> Agda at lists.chalmers.se
>> >> https://lists.chalmers.se/mailman/listinfo/agda
>> > _______________________________________________
>> > Agda mailing list
>> > Agda at lists.chalmers.se
>> > https://lists.chalmers.se/mailman/listinfo/agda
>> _______________________________________________
>> Agda mailing list
>> Agda at lists.chalmers.se
>> https://lists.chalmers.se/mailman/listinfo/agda
>>
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20200414/f25a06f5/attachment.html>