[Agda] Instance fields

[Andreas Nuyts]

Thanks. A little experiment shows that `bar2` works regardless of 
whether its argument is explicit, implicit or instance.

So I conclude that declaring a field `{{foo}}` of a record type R does 
two things:
* It makes the corresponding argument to the constructor, implicit;
* Whenever an argument of type R is in the context, its `foo` field 
becomes available for instance search upon eta-expansion.

Andreas

On 02-08-17 01:50, agda-request at lists.chalmers.se wrote:
> Date: Tue, 1 Aug 2017 11:18:11 -0700
> From: Martin Stone Davis<martin.stone.davis at gmail.com>
> To:agda at lists.chalmers.se
> Subject: Re: [Agda] Instance fields
> Message-ID:<5fb4917c-30a0-4e44-1dda-32984d88b633 at gmail.com>
> Content-Type: text/plain; charset=utf-8; format=flowed
>
> record R : Set where
>     field instance fooI : Foo
>     field {{fooF}} : Foo
>
> For code outside of R, both R.fooI and R.fooF are of type R -> Foo, but
> only R.fooI is subject to instance search. When you're writing code
> inside the record R, fooF is also subject to instance search because
> there it's an instance argument. I should mention that, in practice,
> there are some caveats having to do with eta-expansion, as the code
> below demonstrates.
>
>
> it : ? {a} {A : Set a} {{x : A}} ? A
> it {{x}} = x
>
> record Foo : Set where
>     no-eta-equality
>
> record RNEEI : Set where
>     no-eta-equality
>     field instance fooI : Foo -- if "instance" is removed, then bar1
> fails (because there are no instances)
>     field {{fooR}} : Foo
>
> record REEI : Set where
>     field fooI : Foo -- if "instance" is added, then bar2 fails (because
> there are too many instances)
>     field {{fooR}} : Foo
>
> bar1 : {{_ : RNEEI}} ? Foo
> bar1 = it -- works because RNEEI.fooI is subject to instance search
>
> bar2 : {{_ : REEI}} ? Foo
> bar2 = it -- works because REEI.fooR is an instance argument made
> available by eta-expansion

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