[Agda] Vezzosi's patch

[Sergei Meshveliani]

On Mon, 2017-04-10 at 08:58 -0400, Wolfram Kahl wrote:
> On Mon, Apr 10, 2017 at 03:17:51PM +0300, Sergei Meshveliani wrote:
> > Wolfram wrote recently
> > 
> > > Have you tried this with Andrea Vezzosi's patch from
> > > https://github.com/agda/agda/issues/1625#issuecomment-132196576
> > 
> > I have looked there. This patch is about 
> >   src/full/Agda/TypeChecking/Conversion.hs
> > 
> > I have  Development Agda of March 21, 2017  (ghc-7.10.2, Debian Linux)
> > And the patch is probably the difference file for some old Agda.
> > Is this all right?
> 
> For me, it is still working at least on 2.5.2.
> 
> > Well, I named the patch  V.diff  and commanded
> > 
> >   > mv V.diff  src/full/Agda/TypeChecking/
> > 
> >   > cd src/full/Agda/TypeChecking
> > 
> >   > patch Conversion.hs < V.diff
> > 
> > It reports that this point is found, and issues  Conversion.hs
> > with is about 500 byte longer.
> > 
> > Is this a correct way to use this patch?
> 
> Looks good.
> 
> > Then, I install the obtained Agda, and install the standard library.
> > Then I type-check my application. 
> 
> Did you remove all .agdai files? (Apparently you used a separate
> standard library installation --- good.)  With the patch, some .agdai
> files are different; I haven't tried to analyse this.
> 
> > But its error report is different. The original Agda succeeds, and the
> > patched Agda first type-checks several files and then reports something
> > like a wrong type in a certain .agda file.
> 
> I haven't had such a case yet --- if you can isolate this, it would
> probably be very useful if you could report that example under
> https://github.com/agda/agda/issues/1625 .
> 


Now I repeat this by new with  Development Agda of April 10, 2017
(call it Agda-main),

, and the standard library of the same date.

I apply the Vezzosi's patch, and then install Agda and standard library,
and this makes it  Agda-patched. 

1) Then I test Agda-patched on a relative small example that 
   profiles Serialization, Deserialization, Total  for a certain last
module (as I wrote about a week ago).
In this example the cost explosion is due to substituting for a module
parameter a certain large value expression, which expression occurs
copied many times in the obtained module instance. 

The patch does not help type check performance in this example, 
Agda-patched is a bit slower.
--sharing  makes it even more slow.
 
2) Type-checking the DoCon-A-2.00 library reports an error somewhere
before the middle,
while Agda-main type-checks it.
I do not know, which one is more correct, because it is difficult to see
what is the matter there
("Agda-main accepts it, so one can program things further").

The report is 
---------------------------------------------------------------
/home/mechvel/doconA/2.00/source/List/Multiset0.agda:1122,62-74
Set != (Set (α= ⊔ α))
when checking that the expression m>mults-tail has type
_x_2041 A C-Show decInhabited mS mSets .Relation.Unary.∈
All(All (λ z →
    suc (_i_2040 A C-Show decInhabited mS mSets) ≤
    proj₁ (upperMultiplicity mSets)))
---------------------------------------------------------------

If people ask, I can provide a reference to the code -- 
"a report of a certain unclear-so-far effect in Agda-patched".

This is about 1/5 of the DoCon-A-2.00 library, and it is large. 


Digression
----------
Currently, my main question to Agda is:

what to do with the internal data explosion produced by substituting a
value for a parameter into a module? into a type?

For example,  
a module M1 has a parameter  C : Set,  and C occurs 20 times in M1;
a module M2 has 
  C' = <a large expression made of taking parts of certain records>.

And M2 includes has declaration
 
    open M1 C' using ...

The representation of C' is copied 20 times in memory, and so on.
Probably, the type checker needs to internally represent the needed
module instance as 

  let  C' = <...>  in  M1-inst,

and a similar approach to be applied to representing a type.
May be this will lead to problems with pattern matching, unification, 
I cannot tell now, I expect that the Agda developers know better.  

Regards,

------
Sergei