[Agda] Automatic conversion between records and iterated Sigma types

[Jacques Carette]

That's the easier direction. I am not surprised, yet pleased, that it is 
feasible.

So is this confirmation the Sigma -> record is indeed currently not 
feasible?

Jacques

On 2020-04-14 2:12 p.m., Jesper Cockx wrote:
> 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 
> <mailto: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 <mailto: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 <mailto: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 <mailto:Agda at lists.chalmers.se>
>>         >> https://lists.chalmers.se/mailman/listinfo/agda
>>         > _______________________________________________
>>         > Agda mailing list
>>         > Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>>         > https://lists.chalmers.se/mailman/listinfo/agda
>>         _______________________________________________
>>         Agda mailing list
>>         Agda at lists.chalmers.se <mailto: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/7c0237c9/attachment.html>