[Agda] `abstract' on Web keywords

[Nils Anders Danielsson]

On 2013-05-15 14:23, Serge D. Mechveliani wrote:
> On Wed, May 15, 2013 at 10:58:53AM +0200, Nils Anders Danielsson wrote:
>> 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" ?).

[...]

> 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.

If you use "careless-abstract", then the definitions are not unfolded,
just as if you had used abstract. The difference is that, when
careless-abstract is used, Agda can make use of the code of a body to
infer information about the corresponding definition's type signature.

If type-signatures "turn yellow" when you use abstract, then you can try
to give some implicit arguments (or underscores) explicitly. An example:

   data D : Set₁₃₇ where

   Works : Set _
   Works = D

   abstract

     Fails : Set _
     Fails = D

     Works′ : Set₁₃₇
     Works′ = D

> I currently think that  `abstract'  is a tool related to unfolding.
> And in Glasgow Haskell it is called `inlining'.
> Do I undertsand correct?

Abstract definitions are not unfolded when the type-checker decides
definitional equality (except in bodies in their own abstract block).
Compiler backends are free to inline abstract definitions.

-- 
/NAD