Private record fields do not work like expected

[GoogleCodeExporter]

record R : Set where
  private
    field
      i : ℕ

r : R
r = record { i = 42 }

get-i : R → ℕ
get-i r = F r refl
  where
    F : {n : ℕ} (r : R) → (r ≡ record { i = n }) → ℕ
    F {n} .(record { i = n }) refl = n

k : ℕ
k = get-i r

k-is-42 : k ≡ 42
k-is-42 = refl

Jonathan Leivent complains one can get the content of a private record field, I suspect this is due to constraint solving not respecting the scope.

However, I wonder why one can set a private field in the first place. In my opinion, the definition of r should fail as well.

Original issue reported on code.google.com by andreas....@gmail.com on 26 Feb 2012 at 11:26

[GoogleCodeExporter]

If we changed Agda so that unification respected the scope, then lots of code would stop working (consider implicit arguments).

I think we should solve this issue by requiring that all fields are public (and non-abstract).

Original comment by nils.anders.danielsson on 27 Feb 2012 at 3:22

[GoogleCodeExporter]

I do not see the connection to implicit arguments.

If you declare a field to be private, you do not want it accessed other than by the methods of that record/object, which in Agda's case would be the functions defined in the record module.

Record construction with

  record { i = ...}

should be forbidden if i is private.

Original comment by andreas....@gmail.com on 27 Feb 2012 at 4:22

[GoogleCodeExporter]

I do not see the connection to implicit arguments.

You wrote "I suspect this is due to constraint solving not respecting the scope". I don't think constraint solving should respect the scope: it should be possible to instantiate meta-variables to things which are not in scope, including names which are declared privately in another module (and including implicitly bound variables).

Original comment by nils.anders.danielsson on 27 Feb 2012 at 6:17

[GoogleCodeExporter]

With scope I did not mean that what the user sees or can enter, but things which are legal in an expression internally. An implicit argument can always be brought into scope by giving it a name.

Private and public is not about naive scoping, but about things I can access. If I can access another modules private stuff, what is the use of private?
(Except to avoid name conflicts, maybe.)

The component "i" or record "R" is private so record { i = ... } should give an error. I think scope checking has not been properly implemented for record values.

Consequently, a record with private fields cannot have a constructor which is not private itself. Only a public user-defined constructor is then possible.

Original comment by andreas....@gmail.com on 27 Feb 2012 at 7:20

[GoogleCodeExporter]

If I can access another modules private stuff, what is the use of private? (Except to avoid name conflicts, maybe.)

To avoid polluting the name space. Private things still compute. If you really want to hide something, use abstract.

As I wrote above: I think we should solve this issue by requiring that all fields are public (and non-abstract).

Original comment by nils.anders.danielsson on 28 Feb 2012 at 4:37

[GoogleCodeExporter]

Fixed by disallowing private fields. You already get an error for trying to make fields abstract.

Original comment by ulf.nor...@gmail.com on 4 Apr 2012 at 2:20

• Changed state: Fixed

[GoogleCodeExporter]

Original comment by andreas....@gmail.com on 14 Nov 2012 at 10:25

• Added labels: Abstract

[andreasabel]

We could also have decided to interpret private for a record field that the respective projection is not exported while the content of the field can still be obtained by matching. Maybe this can be diametral to the user expectations on the concept of a "private field", but it can help with the problem of irrelevant projections. In particular, we could make irrelevant projections private unless --irrelevant-projections is given.

• 6359