Definition dependencies public

Stream: general

[Martin Dvořák]

What is the easiest way to check that a specific important (public) definition doesn't depend on any private definition? I mean both def and abbrev by "definition" in the previous sentence.

[Eric Wieser]

Why do you care?

[Martin Dvořák]

API consistency?

[Ruben Van de Velde]

I think you'll need to expand on that

[Eric Wieser]

Maybe I should ask what you mean by "depend on"?

[Eric Wieser]

Indeed def foo : Bar := _ where private structure Bar is probably problematic, but def foo : Nat := bar where private def bar is not

[Martin Dvořák]

I would like to detect both (anti)patterns:

private def Foo : Type := Fin 37
def zeroFoo : Foo := ⟨0, by decide⟩

private def bar : Char := 'b'
def baz : Char := bar

The latter is less problematic, but I'd like to avoid both of them.

[Kenny Lau]

the latter is fine as long as there is API

[Martin Dvořák]

Speaking of the former problem, is the following catch known?

private def Foo : Type := Fin 37
private theorem Foo.eq_self (x : Foo) : x = x := rfl
theorem break_me (x : Foo) : x = x := x.eq_self

Removing private from Foo.eq_self breaks the proof of the subsequent theorem.

[Aaron Liu]

It because of macro scopes but I can see why it would be confusing if you didn't know the reason

[Robin Arnez]

It's not macro scopes but the fact that private is a name prefix, similar to namespaces

[Robin Arnez]

private Foo is actually _private.My.Module.Path.0.Foo and then it obviously expected _private.My.Module.Path.0.Foo.eq_self for dot notation

[Aaron Liu]

Robin Arnez said:

private Foo is actually _private.My.Module.Path.0.Foo and then it obviously expected _private.My.Module.Path.0.Foo.eq_self for dot notation

Oh I thought those were macro scopes but I guess not (they seemed really similar)

[Robin Arnez]

It's similar but _private is a deterministic prefix (only based on module name) and macro scopes are suffixes with random (technically deterministic but ever-changing) numbers

[Robin Arnez]

or well, _hyg vs _private

[Martin Dvořák]

Robin Arnez said:

It's not macro scopes but the fact that private is a name prefix, similar to namespaces

Would it be reasonable to open a RFC about changing this behavior?

[Joachim Breitner]

Martin Dvořák schrieb:

I would like to detect both (anti)patterns:

private def Foo : Type := Fin 37
def zeroFoo : Foo := ⟨0, by decide⟩

private def bar : Char := 'b'
def baz : Char := bar

The latter is less problematic, but I'd like to avoid both of them.

I think the upcoming module system will prevent the former, and also the latter if the definition is exposed. So maybe just wait for that?

[Martin Dvořák]

Martin Dvořák said:

Speaking of the former problem, is the following catch known?

private def Foo : Type := Fin 37
private theorem Foo.eq_self (x : Foo) : x = x := rfl
theorem break_me (x : Foo) : x = x := x.eq_self

Removing private from Foo.eq_self breaks the proof of the subsequent theorem.

The suggested potential RFC was about this behavior.