[Agda] about `abstract'

[Ulf Norell]

On Mon, Feb 29, 2016 at 2:27 PM, Sergei Meshveliani <mechvel at botik.ru>
wrote:

>
> 2. The given proof for  two+0  is constructed only from the signature of
>    +0.  Hence  +0  can be placed under `abstract' (for this example).
>
> Also I expect that the implementation part for  +0  will not be used
> anywhere in type-checking any future client function, the type checker
> will be satisfied with the signature of  +0.
>
> Can you imagine the necessity of using the implementation rules for 0+
> in type checking something?
>

There are certainly cases where you need equality proofs to reduce. In this
case you might be writing a function on vectors and needing to product a
Vec A n from a Vec A (n + 0). That's easy to do given +0, but if it is
abstract
your function won't evaluate (at compile time, at run-time there's no
problem).

For equality proofs, an alternative is to use
Relation.Binary.PropositionalEquality.TrustMe.erase. This has the effect of
getting rid of the expensive implementation of a proof and replacing it with
a cheaper proof, that still reduces.

/ Ulf
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20160229/d7298b76/attachment.html