[Agda] private fields in records?

[Andreas Abel]

This is a bug, I filed it as issue 580.

Each record declaration creates a module, with the corresponding privacy 
annotations.

If privacy was take seriously, you should also never be able to 
construct record r (where you set the private field to 42).

Cheers,
Andreas

On 25.02.12 8:24 PM, jleivent at comcast.net wrote:
> The Agda documentation doesn't actually say that a record field can
> be private, but it allows the syntax.  And, as one would expect,
> declaring a field private prevents the field's associated projector
> function from being defined (or, at least it is not in scope outside
> the record).  However, there still are ways to get at the "private"
> field from outside the record, as the attached code shows.
>
> One would think this is a bug, if only based on analogy between
> modules (where privacy is more fully documented) and records.
>
> -- Jonathan Leivent
>
>
>
> _______________________________________________ Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

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