[Agda] type check performance

[Sergei Meshveliani]

On Wed, 2017-01-11 at 21:27 +0100, Nils Anders Danielsson wrote:
> On 2017-01-11 19:46, Sergei Meshveliani wrote:
> > Here the size of the type expression grows 2 times with each adding of
> > `id'.
> >
> > Probably this expense in unavoidable.
> 
> No, it can be avoided. See the first page of the paper from which I took
> the example: "Implementing Typed Intermediate Languages" by Shao, League
> and Monnier (https://doi.org/10.1145/289423.289460). The basic idea is
> to store the terms more compactly.
> 


Well, of course, the type checker can process a type expression as

  (T (f x y) -> T (f x y)) -> (T (f x y) -> T (f x y))

with keeping it as   let  U = T (f x y);  V = U -> U  in  V -> V

Is this the idea? I am sorry if I am missing the point.

In many examples this will prevent the data explosion.
In others it may lead to wasting time ...,
also I do not know, what difficulties will this bring to modifying the
unification method, modifying normalization procedure etc.

I have an impression that GHC compiler or interpreter deal with this
kind of evaluation strategy, when concerning operating with _values_
(?).

I have the following question to Agda developers.

Suppose a programmer needs to find out whether his Agda program involves
enormous internal type expression growth when type-checking, which can
be canceled by bringing to the the above `let' form. 
Suppose that a certain  debug-type-check  version 
1) performs type checking as usual,
2) notes each particularly large type expression E (its internal 
   form), and brings it to the `let' form and compares the two sizes,
3) returns the statistics in the end.

Will this statistics really show the inefficiency caused by unlucky
internal representation of a type? 
Is such a `profiling' easy to implement? 

(can this be tested by somehow modifying the application source
program?). 

This does not require any essential change in the type checker.
This is only to test whether this particular effect takes place when
type-checking any chosen application.
Suppose that all reasonable applications on practice do not reveal such
an effect. Then the problem can be delayed, and one will search for
other source of inefficiency.

What people think of this?

Thanks,

------
Sergei