[Agda] Question about the meaning of 'abstract'

[Dan Licata]

I

In-Reply-To: <50A57BE1.5040107 at ifi.lmu.de>

On Nov16, Andreas Abel wrote:
> If you have an abstract definition
>
>   abstract
>     lhs = rhs
>
> is it ok with the meaning of `abstract' that
>
>
>   lhs == rhs
> holds propositionally outside the abstract block.  

when phrased this way, I would say no!

> Agda currently says yes, 
> but would you agree with Agda?
>
>   abstract
>
>     T : Set -> Set
>     T A = A
>
>     see-through : ∀ {A} → T A ≡ A
>     see-through = refl
>
>   opaque : ∀ {A} → T A ≡ A
>   opaque = see-through



But when phrased this way, I would say yes.  

My strongest basis for intuition about abstract is module sealing in ML:
I shouldn't know anything that's not in the signature.  I should be
allowed to explicitly export a propositional equality like see-though
(essentially, putting the equation in the signature), if I want to
advertize a certain equation.  But if I don't export it, then clients
shouldn't know it (which is how I read the original example).  

BTW, Agda is already a little leaky when it comes to abstract, which
came up in relation to faking higher inductive types a few months ago.
As I recall, the problem is that there is no way to stop Agda from
exporting the fact that 

chalk == cheese -> void

when chalk and cheese are abstract but defined to be datatype
constructors inside the abstraction, because they still reduce during
type checking and you can use an absurd pattern to match on the
equality.

-Dan