[Agda] about serialization

[Ulf Norell]

On Sat, Apr 1, 2017 at 2:45 PM, Sergei Meshveliani <mechvel at botik.ru> wrote:

>
> But anyway I need to understand: what generally the type checker does in
> the examples of this kind.
> Here is a simplified example.
>
> module OfSemigroup  is given an arbitrary semigroup H as a parameter,
> and it defines certain items using H.
>
> module OfRing  is given an arbitrary ring R as a parameter.
> It defines  *-semigroup-2  -- a direct product of the multiplcative
> semigroup of R with itself.
>
> module M is given an arbitrary ring R as a parameter.
> And its only implementation is
>     where
>     open OfRing R using (*-semigroup-2)
>     module OfMulSemigroup = OfSemigroup *-semigroup-2
>
> Suppose that M1 and M2 have been type-checked earlier.
> When type-checking M,
> * what is substituted to where?
> * what is being normalized?
> * what part can be expensive?
>

Nothing is normalised and the only type checking that happens is
to check that the given module arguments match the types expected
by the module. The arguments are substituted into the types of the
module definitions, but not the bodies. Nevertheless, this may create
very big types that take a long time to serialise. What does the profile
information tell you about where the time is spent? My money would
be on serialisation.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: <http://lists.chalmers.se/pipermail/agda/attachments/20170404/ffba62a3/attachment.html>