[Agda] Instance fields

[Ulf Norell]

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>
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.h
> tml#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
> https://lists.chalmers.se/mailman/listinfo/agda
>
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170801/f2c1a40c/attachment.html>