[Agda] about `abstract'

[Sergei Meshveliani]

On Mon, 2016-02-29 at 19:40 +0100, Ulf Norell wrote:
> 
> 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).


Please, what precisely is the example?
Is it to program, say

  f : Vec Bool (2 + 0) → Vec Bool 2
and
  bi-f : Bijective f
?
I thought that (Vec A m) and (Vec A n) are considered as different
domains, but it it possible to program a provable bijection

  g :  ∀ {m n} → m ≡ n → Bijection (Vec A m) (Vec A n)

(and isomorphism for any structure on A and (Vec A _)).
And  (2 + 0 ≡ 2)  is provided here by the call  (+0 2).  This does not
need analyzing the body of +0 when type checking.

I do not know, may be you mean making Adga to take (Vec A m) and 
(Vec A n) as the same domain?
(generally, I do not know how to arrange this).

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

Thank you. I shall keep this possibility in mind.

Also I can place both  +0  and  +0-abstract in M0,  and apply
+0-abstract in M1,  and in other suitable places one is free to apply
+0
-- ?

Regards,

------
Sergei