[Agda] Instance fields

[Martin Stone Davis]

> ... That's almost never what you want. ...
Is it *ever* what you want? I haven't yet found a use case where I 
didn't instead prefer `{{...}}`.


On 08/01/2017 11:23 AM, Ulf Norell wrote:
> 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
>
> instance
>   EqA : Eq Bla
>   EqA = ...
>
>   OrdA : Ord Bla
>   OrdA = ...
>
> 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.
>
> 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.
>
> / Ulf
>
> On Tue, Aug 1, 2017 at 2:20 PM, Andreas Nuyts 
> <andreas.nuyts at cs.kuleuven.be <mailto:andreas.nuyts at cs.kuleuven.be>> 
> wrote:
>
>     Hi,
>
>     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 `{{...}}`.
>     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?
>
>     The docs have an example about making a sub-typeclass:
>     http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields
>     <http://agda.readthedocs.io/en/v2.5.2/language/record-types.html#instance-fields>
>     but I would expect this to work equally well by using the
>     `instance` keyword instead of `{{...}}`.
>
>     Best,
>     Andreas
>     _______________________________________________
>     Agda mailing list
>     Agda at lists.chalmers.se <mailto:Agda at lists.chalmers.se>
>     https://lists.chalmers.se/mailman/listinfo/agda
>     <https://lists.chalmers.se/mailman/listinfo/agda>
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170801/eb63da0b/attachment.html>