[Agda] type check performance

[Robbert Krebbers]

This may be related: having large chains of coercions is also 
problematic in Coq, see [1]:

   There is also a severe efficiency issue: the complexity of Coq's
   term comparison algorithm is exponential in the length of the
   coercion chain. While this is clearly a problem specific to the
   current Coq implementation, it is hard and unlikely to be
   resolved soon, so it seems prudent to seek a design that does
   not run into it.

The paper [1] describes another way of organizing algebraic hierarchies 
in Coq so that these long chains of coercions can be avoided. It quite 
crucially relies on Coq's canonical structures mechanism, so I have no 
clue whether you can practically do something similar in Agda.

[1] François Garillot, Georges Gonthier, Assia Mahboubi, Laurence 
Rideau. Packaging Mathematical Structures. TPHOLs'09.
https://hal.inria.fr/inria-00368403v2

On 01/13/2017 05:47 PM, Sergei Meshveliani wrote:
> 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
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda
>