[Agda] Question about the meaning of 'abstract'

[Andreas Abel]

Thanks for your answers, which helped me understand 'abstract' better.

Here is another one:  Agda does not know about abstract record fields.

record R : Set₁ where
   constructor c
   abstract
     field
       f : Set
     g : Set
     g = f
open R

-- fields are never abstract
test : {A : Set} → f (c A) ≡ A
test = refl

The abstract is only applied to g, not to f.

Of course, one could make the whole record abstract, which boils down to 
removing the constructor from scope.  Fields are still not abstract, but 
this cannot be exploited in the absence of a means to construct a record.

My question:  Do you think it is ok that data constructors can be 
abstract but record fields not?

Cheers,
Andreas


On 16.11.12 4:20 AM, Dan Licata wrote:\
> 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).

-- 
Andreas Abel  <><      Du bist der geliebte Mensch.

Theoretical Computer Science, University of Munich
Oettingenstr. 67, D-80538 Munich, GERMANY

andreas.abel at ifi.lmu.de
http://www2.tcs.ifi.lmu.de/~abel/