[Agda] no-eta-equality

[Andrea Vezzosi]

Using rd' doesn't make things any better than using the constructor.

Your suc'Rd is already somewhat improved by no-eta because the match
on (rd a n) will be strict now.

However you should also consider the following version, so that
(suc'Rd (rd a n)) does not reduce by itself, but only when projections
are applied to it.

suc'Rd :  {A : Set} → Rd A → Rd A
fl1 (suc'Rd (rd a n)) =  a
fl2 (suc'Rd (rd a n)) = n



On Wed, Sep 28, 2016 at 1:48 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:
> On Tue, 2016-09-27 at 15:00 +0200, Andrea Vezzosi wrote:
>> No, doing that wouldn't be enough to see major improvements.
>>
>> You have to change definitions that build elements of Foo into ones
>> that do so by copatterns.
>
>
> Consider the example:
>
>   {-# OPTIONS --copatterns #-}
>   record Rd (A : Set) : Set where no-eta-equality
>                                   constructor rd
>                                   field fl1 : A
>                                         fl2 : ℕ
>   open Rd
>
>   sucRd :  {A : Set} → Rd A → Rd A
>   sucRd (rd a n) =  rd a (suc n)
>
> Suppose that I need to reduce the type check expense for a further
> program that contains many functions that build elements of the type
> family  Rd A.
>
> Then I need to add the function
>
>   rd' :  {A : Set} → A → ℕ → Rd A
>   fl1 (rd' a _) = a
>   fl2 (rd' _ n) = n
>
> (where rd' looks like another version of the constructor  rd)
>
> and to replace the function  sucRd  with
>
>   suc'Rd :  {A : Set} → Rd A → Rd A
>   suc'Rd (rd a n) =  rd' a (suc n)
>
> and to replace in a similar way other functions that build values of the
> type family  Rd A.
>
> Do I understand this correct?
> What things in this example will be compared "by name" rather than
> structurally?
>
> Thank you in advance for explanation,
>
> ------
> Sergei
>
>