[Agda] Automatic conversion between records and iterated Sigma types

[Jesper Cockx]

Indeed, automatically converting from an iterated sigma type into a record
type would require generating fresh top-level names for the fields of the
record, which is currently not possible.

-- Jesper

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

> 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>
> 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/c3139624/attachment.html>