<div dir="ltr"><div>Hi Jacques,</div><div><br></div><div>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.</div><div><br></div><div>-- Jesper<br></div></div><br><div class="gmail_quote"><div dir="ltr" class="gmail_attr">On Tue, Apr 14, 2020 at 7:38 PM Jacques Carette <<a href="mailto:carette@mcmaster.ca">carette@mcmaster.ca</a>> wrote:<br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">
<div>
<p>Thanks Jesper.</p>
<p>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!</p>
<p>Jacques<br>
</p>
<div>On 2020-04-14 4:07 a.m., Jesper Cockx
wrote:<br>
</div>
<blockquote type="cite">
<div dir="ltr">
<div>Hi Jacques,</div>
<div><br>
</div>
<div>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.</div>
<div><br>
</div>
<div>-- Jesper<br>
</div>
</div>
<br>
<div class="gmail_quote">
<div dir="ltr" class="gmail_attr">On Mon, Apr 13, 2020 at 9:20
PM Jacques Carette <<a href="mailto:carette@mcmaster.ca" target="_blank">carette@mcmaster.ca</a>> wrote:<br>
</div>
<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left:1px solid rgb(204,204,204);padding-left:1ex">Very
hard, I believe. Lines 1113 and 1114<br>
<br>
let u := fresh "u" in<br>
let v := fresh "v" in<br>
<br>
in particular. See the comment by @jespercockx on <br>
<a href="https://github.com/agda/agda/issues/3699" rel="noreferrer" target="_blank">https://github.com/agda/agda/issues/3699</a>.<br>
<br>
Jacques<br>
<br>
On 2020-04-13 3:11 p.m., Bas Spitters wrote:<br>
> This is what the issig tactic does in the HoTT library. I
don't know<br>
> how difficult it is to convert it to agda.<br>
> <a href="https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v" rel="noreferrer" target="_blank">https://github.com/HoTT/HoTT/blob/master/theories/Basics/Overture.v</a><br>
><br>
> On Mon, Apr 13, 2020 at 8:47 PM Martin Escardo <<a href="mailto:m.escardo@cs.bham.ac.uk" target="_blank">m.escardo@cs.bham.ac.uk</a>>
wrote:<br>
>> Is it possible to write a tactic to convert between
records and<br>
>> equivalent iterated Sigma types? And, if so, to also
produce code to<br>
>> establish their equivalence?<br>
>><br>
>> Thanks,<br>
>> Martin<br>
>> _______________________________________________<br>
>> Agda mailing list<br>
>> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
>> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
> _______________________________________________<br>
> Agda mailing list<br>
> <a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
> <a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
_______________________________________________<br>
Agda mailing list<br>
<a href="mailto:Agda@lists.chalmers.se" target="_blank">Agda@lists.chalmers.se</a><br>
<a href="https://lists.chalmers.se/mailman/listinfo/agda" rel="noreferrer" target="_blank">https://lists.chalmers.se/mailman/listinfo/agda</a><br>
</blockquote>
</div>
</blockquote>
</div>
</blockquote></div>