[Agda] about serialization

[Sergei Meshveliani]

On Fri, 2017-03-31 at 22:38 -0400, Wolfram Kahl wrote:
> On Fri, Mar 31, 2017 at 11:41:37PM +0300, Sergei Meshveliani wrote:
> > My real example is of the scheme
> > 
> > [...]
> > So that  M2  does almost nothing.
> > 
> > Only in the real example  M11  has certain complex definitions inside
> > it, with  p : CommutativeMonoid  (represented by a dependent record).
> > But real  M2  has nothing besides importing  p  from a certain
> > parametric module and declaring  
> >            module M11-p = M11 p.
> > 
> > In the above example I replace this with the line
> > 
> >    module M11-2 = M11 2. 
> > 
> > And type-checking of the real  M2.agda  takes 75 sec on a 3 GHz machine,
> > and needs more than 3 Gb heap.
> 
> Have you tried this with Andrea Vezzosi's patch from
> https://github.com/agda/agda/issues/1625#issuecomment-132196576
> ?


Thank you. I am going to try it.

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?

The concrete code is below.

Can, please, the Agda developers comment?


--------------------------------- M1.agda ------------------------
module M1 where
open import Relation.Binary using (Setoid)
open import Algebra         using (Semigroup)
open import Relation.Binary.Product.Pointwise using (_×-setoid_)

module OfSemigroup {α α=} (H : Semigroup α α=)
  where
  open Semigroup H using (setoid)

  setoid-2 : Setoid _ _
  setoid-2 = setoid ×-setoid setoid


----------------------------------- M2.agda -----------------------
module M2 where
open import Relation.Binary    using (Rel)
open import Algebra            using (Semigroup; Ring)
open import Algebra.Structures using (IsSemigroup)
open import Algebra.FunctionProperties using (Op₂)
open import Data.Product               using (_×_; _,_)
open import Data.Nat                   using (ℕ)

_×-semigroup_ :  ∀ {α α= β β=} → Semigroup α α= → Semigroup β β= →
                                                  Semigroup _ _
H₁ ×-semigroup H₂ = record{ Carrier     = C₁ × C₂
		          ; _≈_         = eq
		          ; _∙_         = _∙∙_
		          ; isSemigroup = isSmg }
    where
    open Semigroup H₁ using () renaming (Carrier to C₁; _≈_ to _≈₁_;
                                                        _∙_ to _∙₁_)
    open Semigroup H₂ using () renaming (Carrier to C₂; _≈_ to _≈₂_;
                                                        _∙_ to _∙₂_)
    eq : Rel (C₁ × C₂) _
    eq (x , y) (x' , y') =  x ≈₁ x' × y ≈₂ y'

    _∙∙_ : Op₂ (C₁ × C₂)
    (x , y) ∙∙ (x' , y') =  (x ∙₁ x' , y ∙₂ y')

    postulate  isSmg : IsSemigroup eq _∙∙_

module OfRing {α α=} (R : Ring α α=)
  where
  open Ring R using (*-semigroup)

  *-semigroup-2 :  Semigroup _ _
  *-semigroup-2 =  *-semigroup ×-semigroup *-semigroup

  record Foo : Set α where
                     field fromNat : ℕ → Ring.Carrier R


---------------------------------- M.agda ----------------------
open import Algebra using (Ring)
open import M1 using (module OfSemigroup)
open import M2 using (module OfRing)

module M {α α=} (R : Ring α α=)
  where
  open OfRing R using (*-semigroup-2)

  module OfMulSemigroup = OfSemigroup *-semigroup-2
----------------------------------------------------------------


In the real example 
a) Semigroup and Ring are defined as certain nested records, 
b) the module OfRing does with *-semigroup something more complex than
   _×-semigroup_.


Thanks,

------
Sergei