[Agda] type check performance

[Sergei Meshveliani]

On Fri, 2017-01-13 at 12:00 -0500, Jacques Carette wrote:
> Investigate what "open ... public" does.  This is useful to 'flatten' 
> hierarchies.


The code in my last letter does make use of  open-public.
Thus in the function

  f : ∀ {α α=} → (upR : UpCommutativeRing α α=) →
                 UpCommutativeRing.Carrier upR  →
                 UpCommutativeRing.Carrier upR

  f upR a =  let open UpCommutativeRing upR
             in  a + (a * a + 1#)


Carrier, +, *, 1#  are not operations in  UpCommutativeRing.

This structure definition is
 
 record UpCommutativeRing (α α= : Level) :  Set _
   where
   constructor upCommRing′

   field  upRingWithOne   : UpRingWithOne α α=
          commutativeRing : CommutativeRing upRingWithOne

   open CommutativeRing commutativeRing public hiding (upRingWithOne)


CommutativeRing  also does not have them, instead it (besides having
operations of its own) declares open-public for certain lower level
structures, and so on.
So that
1# appears only at the level of RingWithOne, and comes as 
   (Monoid._∙_ *monoid).
_+_ appears only from Ringoid, and is substituted as  
    (Magma._∙_ +magma).
 
and Carrier appears only at the lowest level of  (Dec)Setoid.

Each of these operations is declared only once in one place in the
hierarchy.
So, I have an impression that open-public does not help to have a type
expression printing size comparable to the one of Standard library.

One of the differences to Standard library is that  Standard library
re-declares some operations.
For example, Setoid declares Carrier and _≈_.  
And DecSetoid re-declares these two, and also adds  isDecEquivalence.
And Semigroup re-declares these two, and also adds  _∙_ and isSemigroup.
And Monoid  re-declares Carrier, _≈_, _∙_,  
            and adds  ε  and  isMonoid.
And so on.
This re-declaring looks strange to me. I suspected that this was set
according some subtle considerations about type expressions size.

I always thought that I need another approach. Because DoCon-A has more
levels and more operations at each level, and such a re-declaring will
probably lead to exponentially grown code, the program will hardly be
possible to read even to myself.

Now, the type sizes, and the type check cost are this way ...

I do not know of whether it is due to different architecture or due to
other features (there are a lot of proofs, some additional
operations).  

I also do not understand of whether this can, in principle, be
essentially improved by fixing the type checker. 
Or may be, a machine checking of some full formal constructive proof of
a small size may require exponentially large cost as minimum.
I just suspect that this particular DoCon-A-0.04.1 can be type-checked
in  500 Mb * 10 minutes  on a 3 GHz computer,  if only Agda is somehow
optimized.

The current simplest question is:  

why the above  type(f) related to CommutativeRing  is printed about 10
times shorter for Standard library,
and whether this size difference has a real relation to the type check
cost.

Regards,

------
Sergei

 
 




> 
> 
> On 2017-01-13 11:47 AM, Sergei Meshveliani wrote:
> > Am I missing something?
> > Why does not it mention the intermediate structure names, like
> > Semigroup, Group, AbelianGroup ... ?
> >
> >
> 
>