<html>
  <head>
    <meta http-equiv="Content-Type" content="text/html; charset=utf-8">
  </head>
  <body text="#000000" bgcolor="#FFFFFF">
    <p>
      <blockquote type="cite">... That's almost never what you want. ...<br>
      </blockquote>
      Is it *ever* what you want? I haven't yet found a use case where I
      didn't instead prefer `{{...}}`.<br>
    </p>
    <br>
    <div class="moz-cite-prefix">On 08/01/2017 11:23 AM, Ulf Norell
      wrote:<br>
    </div>
    <blockquote type="cite"
cite="mid:CAJjNqYHMwXHeJgBLRHUvMmLmi+g9RVewiDyfq+uhPN5BhVusng@mail.gmail.com">
      <div dir="ltr">Using the `instance` keyword declares the
        projection function an instance. That's almost never what you
        want. You can use it to model super classes, but it's much less
        efficient than using `{{...}}`. Suppose you have
        <div><br>
        </div>
        <div>instance</div>
        <div>  EqA : Eq Bla</div>
        <div>  EqA = ...</div>
        <div><br>
        </div>
        <div>  OrdA : Ord Bla</div>
        <div>  OrdA = ...</div>
        <div><br>
        </div>
        <div>with a super class `instance` field `Ord.super : Ord A
          -> Eq A`. Now you have two possible instances for `Eq A`:
          `EqA` and `Ord.super OrdA`. They are definitionally equal but
          instance search still needs to go through the trouble of
          finding and comparing them. This leads to at least quadratic
          (possibly exponential?) slowdowns in the depth of the super
          class hierarchy.</div>
        <div><br>
        </div>
        <div>You get the same problem when you open a record with
          `instance` fields: the original projection and the specialised
          field are both (definitionally equal) instances.</div>
        <div><br>
        </div>
        <div>/ Ulf</div>
      </div>
      <div class="gmail_extra"><br>
        <div class="gmail_quote">On Tue, Aug 1, 2017 at 2:20 PM, Andreas
          Nuyts <span dir="ltr"><<a
              href="mailto:andreas.nuyts@cs.kuleuven.be" target="_blank"
              moz-do-not-send="true">andreas.nuyts@cs.kuleuven.be</a>></span>
          wrote:<br>
          <blockquote class="gmail_quote" style="margin:0 0 0
            .8ex;border-left:1px #ccc solid;padding-left:1ex">Hi,<br>
            <br>
            In a record type declaration, there are two ways in which we
            can make a field 'instance': either by using the `instance`
            keyword, or by wrapping the name in `{{...}}`.<br>
            I know that the latter makes the field an instance argument
            of the constructor, and the former does not. But are they
            otherwise different, and if so, how?<br>
            <br>
            The docs have an example about making a sub-typeclass: <a
href="http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields"
              rel="noreferrer" target="_blank" moz-do-not-send="true">http://agda.readthedocs.io/en/<wbr>v2.5.2/language/record-types.h<wbr>tml#instance-fields</a><br>
            but I would expect this to work equally well by using the
            `instance` keyword instead of `{{...}}`.<br>
            <br>
            Best,<br>
            Andreas<br>
            ______________________________<wbr>_________________<br>
            Agda mailing list<br>
            <a href="mailto:Agda@lists.chalmers.se" target="_blank"
              moz-do-not-send="true">Agda@lists.chalmers.se</a><br>
            <a href="https://lists.chalmers.se/mailman/listinfo/agda"
              rel="noreferrer" target="_blank" moz-do-not-send="true">https://lists.chalmers.se/mail<wbr>man/listinfo/agda</a><br>
          </blockquote>
        </div>
        <br>
      </div>
      <br>
      <fieldset class="mimeAttachmentHeader"></fieldset>
      <br>
      <pre wrap="">_______________________________________________
Agda mailing list
<a class="moz-txt-link-abbreviated" href="mailto:Agda@lists.chalmers.se">Agda@lists.chalmers.se</a>
<a class="moz-txt-link-freetext" href="https://lists.chalmers.se/mailman/listinfo/agda">https://lists.chalmers.se/mailman/listinfo/agda</a>
</pre>
    </blockquote>
    <br>
  </body>
</html>