[Agda] `abstract' on Web keywords

[Serge D. Mechveliani]

On Wed, May 15, 2013 at 10:58:53AM +0200, Nils Anders Danielsson wrote:
> On 2013-05-14 12:38, Sergei Meshveliani wrote:
> >Now, the obstacle is that all these lemmata are not at the top level,
> >they are each inside its parametrized module, and usually, somewhere at
> >the second level of `where'. And abstracting them out most often leads
> >to "unsolved metas" at the type check.
> 
> If you use abstract, then the type signature is "frozen" before the body
> is checked. This can be annoying, but ensures that implementation
> details do not leak out. In your case I guess you do not care about such
> leakage, because you use abstract for performance reasons, not to hide
> implementation details. One possibility is to have two kinds of
> abstract, one that is aimed at performance and one that is aimed at
> information hiding. However, abstract is already a bit of a hack.
> 

I am trying to understand your consideration.
Probably, you talk of introducing some  careless-abstract  to the 
Language.
careless-abstract  will be possible to set in such places where I 
tried to set `abstract' and failed 
(by "freesing signature", and hence, by "unsolved metas" ?).

Do I understand correct?

> you use abstract for performance reasons not to hide
> implementation details. 

1. In this particular case I aimed at the    type-check performance,
   namely -- at reducing its memory eagerness.

2. I do not uderstand how can one win in the  type-check performance
   by abstracting something and in the same time not hiding 
   implementation details.
When a function body of  f  is  not unfold  in the outer place where 
it is called, then I think, the implementation details of  f  
"are hidden" (?). 
If it is unfold there, then the type-check is space-eager, and 
performance is down.

Is `abstract' similar to  inline-not  in Glasgow Haskell?

I currently think that  `abstract'  is a tool related to unfolding. 
And in Glasgow Haskell it is called `inlining'.
Do I undertsand correct?
If a function is inlined, then GHC can optimize the code deeper.

In GHC, there is set the default depth (or size -- I do not recall) of 
inlining. All things that have greater size/depth are not inlined.
This parameter can be changed by the programmer in a GHC option,
also there is the INLINE pragma.
If GHC inlines everything, then there is likely to occur an explosion 
at the compile-time.
I rely on the default depth/sise -- and just have forgotten of the 
whole point, and I am sure that I do not need to rewise this approach.
Because the complication cost and the code quality are all right.

The question is: is it practically possible to arrange a similar
solution in Agda (I aim at efficient complex algebraic algorithms +
verification). 
I have forgotten that Agda is very different at this point.
It has reasons to unfold functions much more eagerly than GHC. 
Because with restricting unfolding, one, probably, restricts type 
normalization (?), and this makes writing proofs more difficult.
Right?

The situation is as follows.

I tried to set `abstract' in order to make the  type check
practically workable
(3 times speed up, 7 times win in space).
And it is set _only_ for the functions  f  which implementation 
details are surely not necessary to inspect in any outside place 
where  f  is called (this will not help the checker any).

And in 90% of cases I failed to set this `abstract', probably, due 
to the feature of "frosen signature", and hence, to "unsolved metas".
By occasion (I do not understand why and how), this was successful 
for two functions 
(inside a parameterized module, at the 2-3 level of `where'),
and by occasion, these two were unfold in many places, so that the 
space win has occured 7 times. 

I tried to move another similar function for `abstract' to the top 
level, but this needs far too much prelude things. 

If I fail with `abstract', then I shall be forced to write unnaturally
many small modules. This is not nice, for the two reasons.
1) Modules are concept units, like chapters in a book.
2) Many records and functions usually live in the same parameterized 
   module, and use its common prelude.
Splitting a file, leads to introducing an extra parameterized module 
in a different file, and copying the prelude file, usually, a half-page 
code.

On the other hand, Standard library sets `abstract' almost nowhere,
and has many large files and modules, it is considerably larger than 
my currect program. And it is type-checked in  1 Gb
-- while my program needs 9 Gb. 
And there appeared two other users (more experienced) who also need 
about 12 Gb to type-check their applications.
The thing is very unclear, so far. We need to see further. 

Regards,

------
Sergei