<div dir="ltr">As you noticed from the profiling information almost all time is spent on<div>serialisation and deserialisation. Given that you mostly have module</div><div>application this likely means that your types are very big. You can</div><div>inspect the types of everything in a module with the command C-c C-o.</div><div>If you first turn on showing implicit arguments (C-c C-x C-h) you should</div><div>be able to spot the problematic types.</div><div><br></div><div>Note that deserialisation also takes a lot of time, i.e. loading the already<br></div><div>checked modules is expensive, so your problems are not restricted to </div><div>M.agda.</div><div><br></div><div>/ Ulf</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Tue, Apr 4, 2017 at 4:29 PM, Sergei Meshveliani <span dir="ltr"><<a href="mailto:mechvel@botik.ru" target="_blank">mechvel@botik.ru</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div class="HOEnZb"><div class="h5">On Tue, 2017-04-04 at 12:02 +0200, Ulf Norell wrote:<br>
> On Sat, Apr 1, 2017 at 2:45 PM, Sergei Meshveliani <<a href="mailto:mechvel@botik.ru">mechvel@botik.ru</a>><br>
> wrote:<br>
><br>
> But anyway I need to understand: what generally the type<br>
> checker does in<br>
> the examples of this kind.<br>
> Here is a simplified example.<br>
><br>
> module OfSemigroup is given an arbitrary semigroup H as a<br>
> parameter,<br>
> and it defines certain items using H.<br>
><br>
> module OfRing is given an arbitrary ring R as a parameter.<br>
> It defines *-semigroup-2 -- a direct product of the<br>
> multiplcative<br>
> semigroup of R with itself.<br>
><br>
> module M is given an arbitrary ring R as a parameter.<br>
> And its only implementation is<br>
> where<br>
> open OfRing R using (*-semigroup-2)<br>
> module OfMulSemigroup = OfSemigroup *-semigroup-2<br>
><br>
> Suppose that M1 and M2 have been type-checked earlier.<br>
> When type-checking M,<br>
> * what is substituted to where?<br>
> * what is being normalized?<br>
> * what part can be expensive?<br>
><br>
><br>
> Nothing is normalised and the only type checking that happens is<br>
> to check that the given module arguments match the types expected<br>
> by the module. The arguments are substituted into the types of the<br>
> module definitions, but not the bodies. Nevertheless, this may create<br>
> very big types that take a long time to serialise. What does the<br>
> profile information tell you about where the time is spent? My money<br>
> would be on serialisation.<br>
><br>
<br>
</div></div>Thank you for explanation.<br>
<br>
In the real example, it reports for -M8G and 3 GHz machine:<br>
<br>
Total 122,391ms<br>
Miscellaneous 51,607ms<br>
UFtRing0 70,784ms<br>
<br>
Serialization 49,883ms (61,239ms)<br>
Deserialization 51,303ms,<br>
<br>
where M.agda = UFtRing0.agda,<br>
the first 3 lines are of profile.modules:10,<br>
the last 2 lines are of profile:7.<br>
<br>
I am trying to understand what is happening there so that takes a great<br>
cost.<br>
Let us, so far, consider only the cost of Serialization.<br>
<br>
For the above M.agda, I have in reality quite a small source:<br>
<br>
------------------------------<wbr>------------------------------<wbr>-------<br>
module UFtRing0 where<br>
open import Data.Product using (_,_)<br>
<br>
-- of application-----<br>
open import Structures3 using (UpIntegralRing; UpIntegralRing-with∣?)<br>
open import Structures4 using (module OverIntegralRing-0)<br>
open import Structures6 using (module OverIntegralRing-2)<br>
open import FtMonoid1 using (module OfCCMonoid-1)<br>
open import FtRing using (module OverIntegralRing-5)<br>
<br>
module UniqueFtRing-0 {α α=}<br>
(upIR∣? : UpIntegralRing-with∣? α α=)<br>
(open OverIntegralRing-2 upIR∣? using (Prime∣split))<br>
(open OverIntegralRing-5 upIR∣? using (FactorizationRing))<br>
(ftRing : FactorizationRing)<br>
(prime∣split : Prime∣split)<br>
where<br>
open OverIntegralRing-0 upIR∣? using (_∣'?_; *upCMon-NZ; *cancel-nz)<br>
<br>
module NZPack1 = OfCCMonoid-1 (*upCMon-NZ , _∣'?_) *cancel-nz<br>
------------------------------<wbr>------------------------------<wbr>----------<br>
<br>
The last line "module NZPack1 = ..."<br>
takes 93 % of the type check cost. This is visible when we comment out<br>
this line.<br>
<br>
It remains to see what happens when type checking this last line.<br>
<br>
OfCCMonoid-1 is defined in previous .agda file:<br>
<br>
module OfCCMonoid-1 {α α=}<br>
(upCMon∣? : UpCommutativeMonoid-with∣? α α=)<br>
(let upCMon = proj₁ upCMon∣?)<br>
(open UpCommutativeMonoid upCMon using (setoid; _∙_))<br>
(cancel : LCancellation setoid _∙_)<br>
where ...<br>
<br>
<br>
(1) So, the type checker checks that *upCMon-NZ : UpCommutativeMonoid.<br>
This has been checked earlier, in the module OverIntegralRing-0.agda,<br>
so its Serialization cost here is zero<br>
Right?<br>
<br>
(2) The type checker processes all the signatures in the module<br>
OfCCMonoid-1, with substituting there the parameter values.<br>
<br>
The main parameter value is *upCMon-NZ,<br>
(the parameters _∣'?_ and *cancel-nz give a smaller cost, also they<br>
are considered similarly).<br>
<br>
*upCMon-NZ is imported from OverIntegralRing-0 as ready.<br>
This (nested record structure) is the instance of a generic structure of<br>
CommutativeMonoid for the case of the monoid of nonzero elements in the<br>
given IR : IntegralRing, for multiplication in IR. It may be a large<br>
term.<br>
<br>
And *upCMon-NZ is substituted into all signatures in OfCCMonoid-1.<br>
C = Carrier is extracted from upCMon∣?; the latter is replaced<br>
according to *upCMon-NZ, so that C is being replaced in with<br>
Nonzero in OfCCMonoid-1.<br>
<br>
For example, in<br>
pairValue : C × ℕ → C<br>
pairValue = uncurry _^_<br>
<br>
the signature is replaced with<br>
pairValue : Nonzero × ℕ → Nonzero,<br>
<br>
and the second line is not touched.<br>
Right?<br>
<br>
The signature<br>
pairToAsd : C × ℕ → Associated × ℕ<br>
<br>
is replaced with<br>
pairToAsd : Nonzero × ℕ → Associated-NZ × ℕ<br>
<br>
Here a notion of Associated is imported by<br>
open OfAssociated upCMon∣? using (Associated; ...),<br>
<br>
upCMon∣? is replaced there (in a previous .agda module) with *upCMon-NZ,<br>
and Associated is replaced there with a certain Associated-NZ,<br>
and this has been done when type checking previous .agda modules.<br>
<br>
In the definition<br>
<br>
record Factorization (a : C) : Set (α ⊔ α=)<br>
where<br>
constructor factorization′<br>
<br>
field multiset : Multiset<br>
allPrime : All IsPrime $ msKeys multiset<br>
productEq : a ~ msValue multiset<br>
<br>
Multiset is replaced with certain Multiset-NZ,<br>
IsPrime with IsPrime-NZ,<br>
Both these values are checked and ready in previous .agda modules.<br>
<br>
OfCCMonoid-1 is so that (according to your explanation) only the above<br>
trivial substitutions are done for the values prepared and checked in<br>
previous .agda files.<br>
<br>
Only the size of terms being substituted may be large.<br>
For example, *upCMon-NZ is a structure which contains a proof for that<br>
nonzero elements Nonzero in upIR : IntegralRing form a commutative<br>
monoid for multiplication, and also implementation for several<br>
operations for Monomial.<br>
<br>
These construct and proof are simple conceptually, but take<br>
about 150 nonempty lines of the source in the module devoted to<br>
substructures (sub-semigroup, sub-monoid, etc).<br>
I do not know: how the term for this *upCMon-NZ instance is stored in<br>
the memory.<br>
In the .agdai file, it may take much size (agdai files are large).<br>
But this refers to Deserialization, right?<br>
And symbolic substitutions with this term refer to Serialization.<br>
Right?<br>
I do not know how to find:<br>
which substitution is the most expensive here.<br>
<br>
Intuitively, noone can (probably) be expensive for serialization.<br>
Because a thing there is unfolded once in the memory, and then many<br>
references are copied (?).<br>
But I do not know how Agda performs these substitutions.<br>
May be,<br>
profile.definitions:10<br>
will help?<br>
The declaration<br>
module NZPack1 = OfCCMonoid-1 (*upCMon-NZ , _∣'?_) *cancel-nz<br>
<br>
leads to substituting of the parts of *upCMon-NZ into the definitions in<br>
the module OfCCMonoid-1 which is type-checked in previous .agda files.<br>
How to measure the cost of any of these substitutions?<br>
<br>
Thanks,<br>
<br>
------<br>
Sergei<br>
<br>
<br>
<br>
</blockquote></div><br></div>