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