[Agda] type check performance

[Sergei Meshveliani]

On Thu, 2017-01-12 at 14:55 -0500, Wolfram Kahl wrote:
> On Thu, Jan 12, 2017 at 09:35:26PM +0300, Sergei Meshveliani wrote:
> > On Wed, 2017-01-11 at 14:21 -0500, Wolfram Kahl wrote:
> > > Can you go to the top-level of the file module in which this is defined,
> > > and ask for the type  (C-c C-d) of the qualified name of remByDivisor,
> > > qualified as necessary to be able to refer to it from the top-level
> > > of the file module?
> > > 
> > > And also do that for each of  ∣  ,  eucRem ,  ≈ , and  0# ?
> > > 
> > > If my understanding is correct, then at least in some circumstances
> > > and to a certain degree, these are the types that Agda is really dealing with.
> > > 
> > 
> > I have there
> > 
> > --------------------------------------------
> > open import Level using (_⊔_)
> > ...
> > ...
> > module OfEuclideanRing {α α=} (upIR∣? : UpIntegralRing-with∣? α α=)
> >                  (open OverIntegralRing-0 upIR∣? using (EuclideanRing))
> >                  E : EuclideanRing)  
> >   where
> >
> > [...]
> > 
> >   remByDivisor : (a b : C) → b ∣ a → eucRem a b ≈ 0#
> >   ...
> > --------------------------------------------               
> > 
> > I go to the beginning of this file and command
> > 
> >   C-c C-d  
> >   remByDivisor
> > 
> > And it prints its type.
> 
> I just tried something like that myself, and apparently my instructions
> were no good --- sorry! Better create a test file:
> 
> Test1.agda:
> 
>  | module Test1 where
>  | import OfEuclideanRing
> 
> and then do
> 
>   C-c C-d OfEuclideanRing.remByDivisor
> 
> there.


Thank you for help.
I program:

--******************************************************
module Test where
open import Structures3 using (UpCommutativeRing)

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

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

------------------------------------------------------
module Test1 where
open import Test

--****************************************************

(this does not use the Standard library algebraic hierarchy).  

Then, load  Test1  and command

   C-c C-d
   f

It prints

{α α= : .Agda.Primitive.Level}
(upR : .Structures3.UpCommutativeRing α α=) →
.Relation.Binary.DecSetoid.Carrier
(.Structures0.UpDSet.decSetoid
 (.Structures0.UpMagma.upDSet
  (.Structures0a.UpSemigroup.upMagma
   (.Structures1.UpMonoid.upSemigroup
    (.Structures1.UpGroup.upMonoid
     (.Structures1.UpCommutativeGroup.upGroup
      (.Structures2.UpRingoid.+upCommGroup
       (.Structures2.UpRing.upRingoid
        (.Structures3.UpRingWithOne.upRing
         (.Structures3.UpCommutativeRing.upRingWithOne upR)))))))))) →
.Relation.Binary.DecSetoid.Carrier
(.Structures0.UpDSet.decSetoid
 (.Structures0.UpMagma.upDSet
  (.Structures0a.UpSemigroup.upMagma
   (.Structures1.UpMonoid.upSemigroup
    (.Structures1.UpGroup.upMonoid
     (.Structures1.UpCommutativeGroup.upGroup
      (.Structures2.UpRingoid.+upCommGroup
       (.Structures2.UpRing.upRingoid
        (.Structures3.UpRingWithOne.upRing
         (.Structures3.UpCommutativeRing.upRingWithOne upR))))))))))


Naturally, It mentions the levels from UpcommutativeRing down to
DecSetoid -- somewhat  11  levels, as it is set in the user program.

How does the type checker keep this in memory? 
With what expressions this expression is being unified 
(by which variables -- upR, a  ?) 
in the process of type checking the whole project?
What is happening with the generic code (for proofs, for additional
`ordinary' functions) contained in some records inside this
expression?  
(may be some substitutions are made in this code along the process of
unification) ?  
Does this print-out explain that the cost of  7 Gb * 60 minutes
is natural for this project?
 
-- I wonder about all this, only may have suspicions.


Now, let us compare this to using  CommutativeRing  of Standard library.
There CommutativeRing has level  7  in the hierarchy.

--*****************************************************
module Test where                                               
open import Algebra using (CommutativeRing)

f : ∀ {α α=} → (rR : CommutativeRing α α=) → 
               CommutativeRing.Carrier rR → CommutativeRing.Carrier rR

f rR a =  let open CommutativeRing rR in  a + (a * a + 1#)

-----------------------------
module Test1 where
open import Test

--*****************************************************


Load Test1 and command  
               C-c C-d
               f  
It prints

{α α= : .Agda.Primitive.Level}
(rR : .Algebra.CommutativeRing α α=) →
.Algebra.CommutativeRing.Carrier rR →
.Algebra.CommutativeRing.Carrier rR

Am I missing something?
Why does not it mention the intermediate structure names, like
Semigroup, Group, AbelianGroup ... ?

I know that Standard library builds the hierarchy in a different way.
Really, does this imply that this way has somewhat 10-20 smaller type
expressions for domains than mine when type-checking?

Regards,

------
Sergei