[Agda] `abstract' on Web keywords
Nils Anders Danielsson
nad at cse.gu.se
Mon May 27 18:44:57 CEST 2013
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
> 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
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.
More information about the Agda