[Agda] about serialization

[Sergei Meshveliani]

On Wed, 2017-04-05 at 16:16 +0200, Ulf Norell wrote:
> 
> 
> On Wed, Apr 5, 2017 at 3:35 PM, Sergei Meshveliani <mechvel at botik.ru>
> wrote:
>         
>         This type can be defined as
>         
>         --------------------------------------------------------
>         (let C =
>              .Relation.Binary.DecSetoid.Carrier
>         (.Structures0.UpDSet.decSetoid
>                 (.Structures0.UpMagma.upDSet
>                 (.Structures0a.UpSemigroup.upMagma
>                 (.Structures1.UpMonoid.upSemigroup
>                 (.Structures1.UpCommutativeMonoid.upMonoid
>                 (OverIntegralRing-0.*upCMon-NZ {α} {α=} upIR∣?)))))
>               )
>          in
>          {α α= : .Agda.Primitive.Level}
>          (upIR∣? : UpIntegralRing-with∣? α α=) →
>          Data.Product._×_ {α .Agda.Primitive.⊔ α=}
>         {.Agda.Primitive.lzero}
>          C
>          .Agda.Builtin.Nat.Nat
>          →
>          C
>         )
>         -------------------------------------------------------
>         
>         But in the report the expression of C is printed twice.
>         How the checker stores it internally?
> 


> It is stored twice. Some sharing is recovered during serialisation,
> but it's not
> represented explicitly so it will be destroyed by substitution.
> 


The module OfCCMonoid-1 to which the parameter type substitution is
applied has about 30 signatures of kind  (foo : Foo).  And each of them
after substitution is printed by C-c C-o on about 30 lines  on average
-- in the format of  C-c C-o.
So, all the substituted types (with many copies) in this module take
about  900 lines to print.  This is about 16 screen pages. 

I wonder of whether this is large enough to take 33 sec of serialization
for the head module (on a 3 GHz machine).

1) It has sense to make available the sharing output format for C-c C-o 
-- which somehow uses `let' and avoids copies. 
With this it will be easier to see what happens with types.

2) In principle, how usable/difficult can be the sharing representation
of types in the checker? It is easy to agree with substitution.
And I wonder about pattern matching, unification, normalization.

What the Agda developers think of this?

Thanks,

------
Sergei