<div dir="ltr"><div class="gmail_extra"><div class="gmail_quote">On Sat, Apr 1, 2017 at 2:45 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"><br>
But anyway I need to understand: what generally the type 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 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 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></blockquote><div><br></div><div>Nothing is normalised and the only type checking that happens is</div><div>to check that the given module arguments match the types expected</div><div>by the module. The arguments are substituted into the types of the</div><div>module definitions, but not the bodies. Nevertheless, this may create</div><div>very big types that take a long time to serialise. What does the profile</div><div>information tell you about where the time is spent? My money would</div><div>be on serialisation.</div><div><br></div><div>/ Ulf</div></div></div></div>