protected attribute

Stream: general

[Reid Barton]

I just noticed that both protected def ... and @[protected] def ... seem to be valid. Is there any difference?

[Reid Barton]

To partially answer my question, there definitely is some difference

[Simon Hudon]

What difference do you see?

[Reid Barton]

In the same section, it looks like @[protected] has no effect. It's also possible it has no effect whatsoever.

[Simon Hudon]

Here is a comparison:

namespace my_ns

protected def foo := 3

#check my_ns.foo
#check foo -- error

@[protected] def bar := 3

#check my_ns.bar
#check bar -- not an error

end my_ns


#check my_ns.foo
#check foo -- error

#check my_ns.bar
#check bar -- error

open my_ns

#check my_ns.foo
#check foo -- error

#check my_ns.bar
#check bar -- error

[Simon Hudon]

You're right, in the same namespace, it does not take effect yet

[Simon Hudon]

But if you close and open the namespace again:

namespace my_ns

#check my_ns.foo
#check foo -- error

#check my_ns.bar
#check bar -- error

end my_ns

[Reid Barton]

Thanks, this confirms what I thought I was seeing. Now the question is--is this intentional? It does seem sort of useful...

[Simon Hudon]

It's not intentional, I didn't even know there was a difference. I'm not sure why it's there

[Simon Hudon]

How do you make use of it?

[Reid Barton]

Accidentally

[Simon Hudon]

That's an interesting technique :)

[Reid Barton]

I'm returning to nat.pow and I marked a lemma @[protected] in the original nat.pow changes--but I'm sure I didn't intentionally choose it over protected.

[Reid Barton]

Now I am marking more lemmas as protected and in the process of doing so I noticed this difference because the lemmas are used later on in the same section.

[Reid Barton]

In the end I intend to delete all the lemmas anyways so it doesn't matter.

[Simon Hudon]

That's interesting. The curious thing is that, if protected and @[protected] were to behave the same, you could achieve the same effect by adding attribute [protected] foo_bar when you're ready to protect it

[Kyle Miller]

I think this is an implementation detail of protected. When you enter a namespace or open a namespace, it seems to go through all the symbols that don't have the protected attribute and adds the prefix-free version to the list of currently accessible symbols. When you do def normally, it seems to both create the symbol and add it to the list of currently accessible symbols, but if it's protected def it adds the protected attribute but does not do the step where it adds it to the list of currently accessible symbols. If you do @[protected] def, then it's def but then adds the protected attribute afterwards.

Something I found surprising about open is how it is an action and not a declaration:

namespace foo
def x := 2
end foo

open foo

namespace foo
def y := 2
end foo

#check x -- ok
#check y -- error

[Kyle Miller]

It seems namespace management was inspired by some Scheme's symbol namespace management, at least to some degree. (Common Lisp has symbol packages that can refer to other symbol packages to permanently "open" them.)

[Reid Barton]

I think this behavior of open is changing in Lean 4

[Simon Hudon]

How so?

[Reid Barton]

my understanding is that open will apply also to definitions which didn't exist at the time of the open, like y in the above example

[Simon Hudon]

Yes, that's true, I heard that too. That's certainly an improvement