[Agda] Question about the meaning of 'abstract'

Dan Licata drl at cs.cmu.edu
Fri Nov 16 04:20:12 CET 2012


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


More information about the Agda mailing list