[Agda] no-eta-equality

[Sergei Meshveliani]

On Wed, 2016-09-28 at 15:07 +0200, Andrea Vezzosi wrote:
> 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
> 

Sorry, I am somewhat confused.
Consider the example below in which the record  UpDSet   uses
no-eta-equality,  and  eUpDSet  builds a certain instance of UpDSet.

What do I need to change there concretely in order to make  eUpDSet  to
use copatterns?

My library for algebra is a small and a toy library from the point of
view of CA practice. But it cannot type-check within  6 G byte  of
memory (with Agda of September 16, 2016). 

So far I need only to understand: what is the main source of the
expense, to find out the `bottleneck' in the current Agda with respect
to my program.
The first suspect is the record tower for algebraic structures:
    DSet -- UpDSet -- Magma -- UpMagma -- Semigroup -- UpSemigroup,
    CommutativeSemigroup -- UpCommutativeSemigroup, ...,
    and so on, up to EuclideanRing and Field
    (about 26 levels),
    with higher levels having fields and also arguments of lower levels.

The first experiment is only to implement the instance construction of
Up-domains above via copatterns and `no-eta-equality', and to see the
memory expense in type checking.
(This does not mean that I am going to complicate the final program,
this is only for finding the inefficiency source).

Thank you in advance for explanation,

------
Sergei



***************************************************************************
{-# OPTIONS --copatterns #-} 
module M where
open import Level    using (Level; _⊔_; suc)
open import Function using (id)
open import Algebra.FunctionProperties as FuncProp using (Op₂)
open import Relation.Binary   using (Rel; DecSetoid; _Preserves₂_⟶_⟶_)
open import Data.Maybe as Mb  using (Maybe; just; nothing)
open import Data.Nat   as Nat using (ℕ)

--------------------------------------------------------------           
setoidLevel : Level → Level → Level
setoidLevel l l' =  suc (l ⊔ l')

record DSet {c l} (decS : DecSetoid c l) : Set (c ⊔ l)
  where
  constructor dSet′

  open DecSetoid decS using (Carrier)

  field  dSet1 : Carrier → Carrier        -- contrived
         dset2 : Carrier → ℕ


record UpDSet c l : Set (setoidLevel c l)
       where
       no-eta-equality         -- (1) 
       constructor upDSet′

       field  decSetoid : DecSetoid c l
              dSet      : DSet decSetoid

       open DSet dSet public

---------------------------------------------------------------          
module OfMaybe-DSet (c l : Level) (upDS : UpDSet c l)
  where
  decSetoid = UpDSet.decSetoid upDS
  dSet      = UpDSet.dSet upDS

  eDecSetoid : DecSetoid _ _
  eDecSetoid = Mb.decSetoid decSetoid

  open DecSetoid eDecSetoid using () renaming (Carrier to eC)

  eDSet : DSet eDecSetoid
  eDSet = dSet′ f g       -- contrived
          where
          f : eC → eC
          f = id

          g : eC → ℕ
          g _ = 0

  eUpDSet : UpDSet _ _
  eUpDSet = upDSet′ eDecSetoid eDSet   	-- (2) 
*****************************************************************************