<div dir="ltr"><div>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.</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 9:41 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>That's the easier direction. I am not surprised, yet pleased,
that it is feasible.</p>
<p>So is this confirmation the Sigma -> record is indeed
currently not feasible?</p>
<p>Jacques<br>
</p>
<div>On 2020-04-14 2:12 p.m., Jesper Cockx
wrote:<br>
</div>
<blockquote type="cite">
<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" 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">
<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>
</blockquote>
</div>
</blockquote></div>