<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>