Partitioning mathlib

Stream: lean4

[Mario Carneiro]

@Scott Morrison What are the smallest strongly connected components? (i.e. pick a point, close under all forward edges)

[Mario Carneiro]

Regarding data, I think you should just treat the top level subfiles/folders in data as their own nodes in this graph. It's kind of a "misc" directory

[Scott Morrison]

In[76]:= ConnectedComponents[t]

Out[76]= {{"algebraic_topology"}, {"geometry"}, \
{"representation_theory"}, {"probability_theory"}, {"computability"}, \
{"algebra", "algebraic_geometry", "analysis", "category_theory",
  "combinatorics", "control", "data", "deprecated", "dynamics",
  "field_theory", "group_theory", "linear_algebra", "logic",
  "number_theory", "order", "ring_theory", "system", "tactic",
  "topology", "measure_theory", "testing", "meta", "set_theory"}}

[Scott Morrison]

:-(

[Scott Morrison]

Doesn't appreciably improve if we explode data:

{{"algebraic_topology"}, {"computability"}, {"data$ordmap"}, \
{"geometry"}, {"probability_theory"}, {"data$analysis"}, \
{"data$qpf"}, {"data$pfunctor"}, {"data$fp"}, \
{"representation_theory"}, {"algebra", "algebraic_geometry",
  "analysis", "category_theory", "combinatorics", "control", "data",
  "data$complex", "data$equiv", "data$finset", "data$finsupp",
  "data$fintype", "data$int", "data$list", "data$matrix",
  "data$multiset", "data$mv_polynomial", "data$nat", "data$padics",
  "data$pnat", "data$polynomial", "data$rat", "data$real", "data$set",
   "data$zmod", "data$zsqrtd", "deprecated", "dynamics",
  "field_theory", "group_theory", "linear_algebra", "logic",
  "number_theory", "order", "ring_theory", "system", "tactic",
  "topology", "measure_theory", "data$array", "data$buffer",
  "data$dlist", "data$lazy_list", "testing", "data$bitvec",
  "data$string", "set_theory", "data$num", "data$seq", "data$stream",
  "meta", "data$option", "data$setoid", "data$sigma"}}

[Johan Commelin]

Scott Morrison said:

In[76]:= ConnectedComponents[t]

Out[76]= {{"algebraic_topology"}, {"geometry"}, \
{"representation_theory"}, {"probability_theory"}, {"computability"}, \
{"algebra", "algebraic_geometry", "analysis", "category_theory",
  "combinatorics", "control", "data", "deprecated", "dynamics",
  "field_theory", "group_theory", "linear_algebra", "logic",
  "number_theory", "order", "ring_theory", "system", "tactic",
  "topology", "measure_theory", "testing", "meta", "set_theory"}}

Note that there is nothing special about algebraic_topology, geometry, or representation_theory. The fact that these are their own SCC just means that we haven't gone very far in these directions yet.
There are quite-easy-to-state conjecturestheorems in commutative algebra that were only proven a couple of years ago using perfectoid spaces. The Breen-Deligne resolutions in homological algebra that we carefully avoided in LTE are proven to exist using some hammers from algebraic topology. Representation theory uses a lot of Lie theory and algebraic geometry. At the same time, motivic conjectures in number theory/algebraic geometry use a lot of representation theory.
This list can go on and on.

[Mario Carneiro]

Something looks odd about that result. I know that computability references data$nat for example. Perhaps we have the arrows the wrong way around?

[Mario Carneiro]

(I'm interested in a node in the graph and it's dependencies, since that represents a subcomponent that could possibly be extracted to a library. The lonely points in your analysis are just "endpoint theorems" that have no current applications outside their own field, like computability and representation theory.)

[Scott Morrison]

What I did was take the equivalence relation a ~ b iff there is a path from a to b, and a path from b to a. (I think...)

[Scott Morrison]

This is the strongly connected components. (And is invariant under reversing all arrows.)

What you suggested above (just take the closure under arrows in one direction) doesn't give a partition, but I agree is still useful. I'll compute it in a moment.

[Scott Morrison]

The smallest set of top-level (+data) directories closed under adding imports is sadly:

{"algebra", "analysis", "category_theory", "control", "data", \
"data.equiv", "data.finset", "data.finsupp", "data.fintype", \
"data.int", "data.list", "data.matrix", "data.multiset", \
"data.mv_polynomial", "data.nat", "data.option", "data.polynomial", \
"data.rat", "data.seq", "data.set", "data.zmod", "deprecated", \
"group_theory", "linear_algebra", "logic", "number_theory", "order", \
"ring_theory", "tactic", "topology", "combinatorics", "data.complex", \
"data.real", "field_theory", "measure_theory", "data.sigma", \
"set_theory", "data.stream", "data.array", "data.num", "data.pnat", \
"data.string", "data.setoid", "dynamics", "data.zsqrtd", \
"algebraic_geometry", "data.padics", "data.buffer", "data.dlist", \
"meta", "testing", "data.bitvec", "data.lazy_list", "system"}

[Johan Commelin]

Wait, I don't think I understand what you mean with "closed under adding imports".

[Scott Morrison]

Say directory A imports directory B if _some_ file in A imports _some_ file in B.

[Scott Morrison]

Say directory A transitively imports directory B is there is a chain of such...

[Johan Commelin]

Ooh, wow. What is the complement of that smallest set?

[Scott Morrison]

Claim, this is the smallest set of directories closed under "imports".

[Scott Morrison]

{"algebraic_topology", "computability", "data.analysis", "data.fp", \
"data.ordmap", "data.pfunctor", "data.qpf", "geometry", \
"probability_theory", "representation_theory"}

[Scott Morrison]

So just the "brand new" stuff plus some abandonware.

[Mario Carneiro]

If you take any point v in the graph and add all points it points to and all points they point to and so on, you get a set. You can do this for every point in the graph and many of them will be the same, and the ones that are minimal by subset order will also be SCCs (every point in the set will generate the set by this procedure)

[Scott Morrison]

The problem here is that blurring things out to directory level makes mathlib very much not a DAG.

[Mario Carneiro]

I think this is all making the point that every directory uses every other directory very well though

[Mario Carneiro]

for example with the graph A -> B <-> C you get the sets {A, B, C} (not a SCC) and {B, C} (a SCC)

[Eric Wieser]

I don't think that effect of directory blurring is surprising; if you have a lemma connecting two directories A and B, its file usually ends up in one of A or B without much thought as to which.

[Mac]

Any particular reason why dependencies are being analyzed at the directory level rather than the file level? I would imagine that each area of theory would be interconnected with others. However, I also imagine there exists some "basic" foundation that each area defines without reference to others that could be extracted out into some "prelude" that could be imported by each area that leverages it. The interconnected components would then be add latter in the main file.

For example, you could have prelude/algebra which defines all the type classes relevant to algebra and that may be imported by other things like ring_theory and then algebra proper that imports prelude/algebra along with stuff in others areas to fill in the interconnections.

[Johan Commelin]

I guess that means we'll have north of 50 pkgs. Which is probably fine. As long as they don't have to be maintained manually.

[Mario Carneiro]

Yeah I have no problem with having 50 packages if it can all be handled transparently and doesn't affect the naming of things. The problem is that naming things prelude27/algebra makes it absolutely atrocious to find anything. I really want a solution that allows the packaging to work on a level orthogonal to file layout and module naming (which is topical, not based on dependency order)

[Brandon Brown]

Is just splitting mathlib into two things still on the table, a "complib" and a "mathlib" where complib (or whatever it would be called) just contains tactics and other basic things that mathlib or any computation-focused people alike would need?

[Mario Carneiro]

quite frankly I would like to call that other lib "std"

[Mario Carneiro]

I do think there is a place for a more separate piece of mathlib which is more focused on comp sci, tactics, and the basic mathematics needed to support it, while still being batteries-included like mathlib

[Mario Carneiro]

That is at least topically separate enough that people can probably get their heads around it (although there is conceivably a good deal of overlap when it comes to the kind of stuff that ends up in data)

[Mac]

Mario Carneiro said:

Yeah I have no problem with having 50 packages if it can all be handled transparently and doesn't affect the naming of things. The problem is that naming things prelude27/algebra makes it absolutely atrocious to find anything.

I am not sure this would be a problem. For example if I have I want all of algebra I importAlgebra, if I just want algebra's prelude I import Algebra.Prelude. The prelude, if necessary, could be split into separate modules as well (ex. Algebra.PreludeAand Algebra.PreludeB -- the real modules would have more informative names -- like Classes or Basic or whatever). If said splits are sequential (i.e. PreludeB imports PreludeA) then only the relevant level would need to be imported by users. If said splits are independent than the user can imported whichever of PreludeA and/or PreludeB they need.

[Mario Carneiro]

if said splits are independent than the user can imported whichever of PreludeA or PreludeB they need.

Right, this is the problem - you won't be able to tell which one you want most of the time because the names are likely to be very difficult to make informative

[Mario Carneiro]

We already have this kind of thing, at the file level. Mathlib almost always uses precise imports to combat dependency creep. I just want to leverage that instead of adding another thing for users to deal with

[Mac]

Mario Carneiro said:

you won't be able to tell which one you want most of the time because the names are likely to be very difficult to make informative

Why? What makes it so hard to give informative names? For example, If have a module with foo, bar, and baz. I could, in the worst case, call it FooBarBaz.

[Mac]

Mario Carneiro said:

We already have this kind of thing, at the file level. Mathlib almost always uses precise imports to combat dependency creep. I just want to leverage that instead of adding another thing for users to deal with

I thought we were talking about the file level?

[Mario Carneiro]

What if it's foo and then bar and then more foo and then foo and bar together?

[Mario Carneiro]

sometimes it gets hard to name things beyond Foo1, Bar, Foo2, FooBar

[Johan Commelin]

Or what if there are 10 files that progressively treat more and more theory of foo?

[Mario Carneiro]

and then if you have a foo fact you want you have to go looking through several files

[Mac]

Mario Carneiro said:

What if it's foo and then bar and then more foo and then foo and bar together?

If there is no greater logical grouping than I really should have six modules: Foo.Basic, Bar.Basic, Foo.Extra, FooBar, Foo (Foo.Basic + Foo.Extra + FooBar), and Bar (Bar.Basic + FooBar).

[Mario Carneiro]

mathlib has this issue a lot, because that's how math works: the concepts are few but the layers of theorems keep coming. Reminder that FLT is a theorem about the natural numbers

[Mario Carneiro]

So Foo is the complete theory of foo? Does that mean that it conceptually could import literally anything in mathlib?

[Mario Carneiro]

because that means it will be unusable (in mathlib)

[Mac]

That is what I would expect, yes

[Mac]

(as an end user)

[Mario Carneiro]

Unfortunately a lot of mathlib files fall in roughly this category which is why the dependency graph is such a rats nest

[Mac]

In what category do you mean?

[Mario Carneiro]

From an end user perspective (someone importing the library), there aren't any dependency issues, you can just use whatever you like. I'm talking about the within-mathlib perspective. (When I said "users" earlier I meant contributors)

[Mario Carneiro]

Almost every new file conceptually builds on everything that came before. If you are a mathematician expanding the theory in some area you don't want to be bothered with this dependency tetris, you just import what you need

[Mac]

Mario Carneiro said:

Almost every new file conceptually builds on everything that came before. If you are a mathematician expanding the theory in some area you don't want to be bothered with this dependency tetris, you just import what you need

That's fine for prototyping, but upon actual addition to the library, optimizing imports should be done.

[Mario Carneiro]

As a maintainer, this approach doesn't bother me so much, because dependency pruning is an activity that can be dealt with separately and requires very little mathematical skill

[Mac]

Okay so we seem to be on the same page there.

[Mac]

In which case a contributor could write their new file using the complete endpoints (ex. Foo and Bar) and the later dependency pruning step could optimize the dependencies and add that file to its relevant theories (including, possibly Foo and/or Bar).

[Mario Carneiro]

However, what this means is that the actual intended position of most files in the dependency graph is not clear. Is this a high-end theorem? Something foundational? Many files mix a bit of both, and high-end theorems often try to race each other to the top

[Mac]

Maybe some tooling could be written to take a Lean file and inject its definitions into the proper place in the dependency graph based on used name?

[Mario Carneiro]

Given that, a naming/foldering convention that makes dependency height important is a distraction for most contributors. Dependency organization is important but should be centralized in a way that doesn't impact the contributor experience

[Mario Carneiro]

for example, a build file that explicitly orders everything

[Mario Carneiro]

although full dependency inference is also possible

[Mario Carneiro]

the advantage being that you never have to worry about dependency order unless you hit a cycle

[Mac]

Yeah that is what I was thinking. The idea would be contributors would all stick their contributions in a newstuff folder (or something like that) that would use the easy-to-access endpoints (ex. Algebra or Foo/Bar) and a latter dependency pruning / build step would reorder things to be reasonable (by refactor additions into Foo.Basic / Bar.Basic or whatever).

[Mario Carneiro]

We want people to organize new material though. The organization is based on topic, not dependency order, though

[Mac]

okay, so the contributions in the postulated newstuff folder (or whatever) could be organized into folders based on topic?

[Mario Carneiro]

and the other part?

[Mac]

which other part?

[Mario Carneiro]

right now all of mathlib is organized like your newstuff folder

[Mario Carneiro]

it sounds like you are trying to add an explicit transition point to a different organization scheme which is based on dependencies

[Mac]

So then the dependency pruning step involves taking those definitions and sticking them into the proper modules based on their dependency order (and topic).

[Mario Carneiro]

but then users have to know about that dependency order in order to import the file

[Mac]

Yes, that is generally how end user importing of files/libraries works? If they want to be specific about things, otherwise they also just use the easy endpoints.

[Mac]

The point in this whole effort would be for those users who specifically only want to leverage stuff at higher levels of the dependency chain.

[Mac]

It would also then help in migrating some of that stuff into a separate less mathy, more standard library.

[Mario Carneiro]

Why can't the naming just not be related to dependency order?

[Mario Carneiro]

It is strange to me that this needs to be so intertwined

[Mario Carneiro]

Just let people name things as they like

[Daniel Fabian]

When you start going to the very fine grained approach, your packages again won't make much sense. You need the packages to talk about a topic, at least roughly

[Mac]

Yes, but I think we are talking about files within packages though.

[Mario Carneiro]

If end users have the ability to make a la carte sub-packages from mathlib according to whatever they feel like importing, then that pretty much solves the problem without having to do solve the hardest problem in computer science (naming things)

[Patrick Massot]

Why don't we simply have a MacLib organized and developped by Mac the way Mac thinks is good and keep mathlib the way it works so great for everyone else?

[Mac]

Patrick Massot said:

Why don't we simply have a MacLib organized and developped by Mac the way Mac thinks is good and keep mathlib the way it works so great for everyone else?

Fyi, I wasn't the one who proposed partitioning mathlib here.

[Mac]

I was simply providing some ideas as to how that could occur.

[Daniel Fabian]

I asked about topical packages early in the thread and I got legitimate issues. The idea of splitting up must make sense in order to happen.

[Daniel Fabian]

The idea of doing ad hoc packages sounds like dead code elimination which is something we could do in the compiler domain

[Mario Carneiro]

this would be more like leanpkg domain, but that's the general idea

[Daniel Fabian]

Not really... Why bother with files. Might just as well do it on the definition level

[Daniel Fabian]

It's like dead code elimination and you choosing to re export what you want to reuse

[Mario Carneiro]

that would be even better, but it's almost science fiction level I think

[Daniel Fabian]

It's what Javascript does more of less

[Mac]

The domain of leanpkg is download/building/running packages, it has more-or-less nothing to do with how those packages are used in code.

[Mario Carneiro]

dependency management is definitely in the purview of cargo

[Daniel Fabian]

To get that fine grained dependency management that you like about mathlib, the most logical approach is a source dependency with dead code elimination

[Mac]

Daniel Fabian said:

It's like dead code elimination and you choosing to re export what you want to reuse

For the latter, this should actually be pretty possible once Lean gets it module system. The former would require retooling the compiler to keep track of which imported symbols are used and prune the unused ones from the result olean and providing that information in a way that the rebuilder (which is part of leanpkg) can figure out whether or not to rebuild the file when its dependencies change.

[Daniel Fabian]

That could totally be a way of depending on mathlib, effectively as a submodule with pruning

[Mario Carneiro]

How do you know if an import is dead though? Simon looked at this problem a while back and unfortunately the most reliable method is just to take the import line out and see if lean complains

[Mario Carneiro]

because lean imports can have so many kinds of side effects on the environment and parsing

[Mac]

Yeah, that is the major problem with automatic approach.

[Daniel Fabian]

Interesting. I think we will learn more about the problem space when we build the module system

[Mario Carneiro]

You can still do it, but it is computationally expensive enough that it's worth just taking the import lines at face value and relying on external processes to optimize them

[Daniel Fabian]

I could for instance see having an isolated environment per module or similar

[Mac]

@Daniel Fabian In fact, this also sounds similar to the discussion around changing Notation.lean and having to rebuild all of Lean.

[Daniel Fabian]

It is certainly worth thinking about

[Mac]

Mario Carneiro said:

You can still do it, but it is computationally expensive enough that it's worth just taking the import lines at face value and relying on external processes to optimize them

Alternatively, the ad-hoc package approach (within the module system) where someone just imports the entirety of Mathlib and then only manual exports select symbols would also work (and remove the need for optimizing imports).

[Mac]

ala JavaScript and Haskell

[Brandon Brown]

If mathlib becomes more narrowly math-focused, then it seems that it makes sense to keep it a monolith since a monolith is simple and many of the math-focused users are not well-versed with complexities of all these dependency/build issues and just want to be doing math, and it's easy to contribute to a monolith. Packages that are meant for writing practical programs can do the typical programming language package dichotomization.

[Daniel Fabian]

Another option might be ex post dead code elimination. After elaboration it might be much easier

[Mario Carneiro]

It is definitely easier post elaboration, but it's also "wrong", you miss out on imports that were required for the lean file to build

[Mario Carneiro]

If you only care about the output files then that's quite doable. olean files have an easily accessible explicit dependency relation

[Eric Wieser]

If lean4 compiles to C, can't the gcc linker do the dead code elimination? If we're not eliminating dead code to reduce binary sizes, what are we eliminating it for?

[Mario Carneiro]

Regarding "Packages that are meant for writing practical programs can do the typical programming language package dichotomization.", keep in mind that a big part of the draw (for me, at least) is the ability to write programs and then prove things about them. This is an anti-modular pattern though, because you need to know what a program is doing to prove it is correct. So splitting the mathy stuff from the programming stuff doesn't really work, or rather it works as long as you accept that the packages are separate but actually tightly coupled

[Mario Carneiro]

This is part of why I have argued against the pervasive use of private in lean core, because it hinders reusability and introspection from external packages like mathlib

[Mac]

Eric Wieser said:

If lean4 compiles to C, can't the gcc linker do the dead code elimination? If we're not eliminating dead code to reduce binary sizes, what are we eliminating it for?

The idea is to create ad-hoc packages that only have some subset of the functionality of mathlib. So let's say I want to create the package OpenPrivate that only has the open private command from mathlib. I could import all of mathlib export open private and its related syntax and then the dead code elimination would remove the rest of the code in mathlib so that the resulting binary library for OpenPrivate only has the code it needs to support open private.

[Mario Carneiro]

If you are building a binary, the linker should already do that

[Gabriel Ebner]

open private seems like one of those this-should-actually-be-in-core modules that could be easily split from mathlib.

[Mac]

Mario Carneiro said:

Regarding "Packages that are meant for writing practical programs can do the typical programming language package dichotomization.", keep in mind that a big part of the draw (for me, at least) is the ability to write programs and then prove things about them.

However the idea is that Lean is now going to be a general purpose language. That is, many people will write programs and libraries without necessarily proving anything about them. Then, if someone else comes along and wants to verify the contents of said libraries they can create a separate (but related) library that proves things about it. Thus, the dichotomization can still appear.

[Mac]

Mario Carneiro said:

If you are building a binary, the linker should already do that

I'm pretty sure it doesn't. In fact, I believe that resulting library will be the entirety of math lib plus whatever code you write (because transitive imports).

[Mario Carneiro]

That is, many people will write programs and libraries without necessarily proving anything about them. Then, if someone else comes along and wants to verify the contents of said libraries they can create a separate (but related) library that proves things about it.

Yes, that's exactly the situation we currently find ourselves in. The unverified package is lean core, and the someone else is mathlib

[Mac]

Yes? So? I'm confused as to what you are getting at.

[Mario Carneiro]

But the dependent proofy package needs to be able to couple to the unverified package and encapsulation mechanisms from traditional programming languages are actively hostile to this effort

[Mac]

I agree completely with your desire to remove private as concept.

[Mac]

I think, if desired, being able to get at any definition should be possible.

[Mario Carneiro]

I am vaguely uncomfortable with discussions about a module system because I expect it to be another, possibly stronger, iteration of the same idea

[Daniel Fabian]

why not do an in-between thing? private could hide intellsense, making the UX nice and clean, but you might eg do something like obj.#privateMethod to access privates?

[Daniel Fabian]

There's value to private stuff due to encapsulation, but in a pure language you don't need to worry about corrupting state.

[Daniel Fabian]

so maybe making it a UX thing is good enough?

[Mario Carneiro]

That kind of privacy is totally fine by me

[Mario Carneiro]

I think python also does something like that

[Mario Carneiro]

privacy by ugly naming convention

[Mac]

Sounds good to me as well.

[Daniel Fabian]

but in python you can shoot yourself into the foot.

[Daniel Fabian]

In a pure language, not so much...

[Brandon Brown]

In Python the "private" methods start with underscores. Not really hidden just a prefix naming convention

[Mac]

I would suggest leaving # to mean side-effecting commands though and use something else for the notation.

[Mac]

Brandon Brown said:

In Python the "private" methods start with underscores. Not really hidden just a prefix naming convention

Yeah I like the underscore / double underscore naming convention unfortunately that clashes with placeholders in Lean.

[Daniel Fabian]

sounds at least worth an RFC, we can see what others think?

[Mac]

This would also have the possible side effect of fixing #418.

[Brandon Brown]

How about obj.@private_method since the @ symbol is already used to make the implicit explicit in functions, so sort of semantically in the same ballpark

[Mac]

That's a good idea! The only qualm I have is that users may confuse it to mean explicit applying a function field.

[Daniel Fabian]

not @, please. Because private still can have implicits.

[Brandon Brown]

ah right, of course

[Mario Carneiro]

I don't think anything like this is really needed, though. We already have a convention of using fooAux or foo.impl and such for internal function names, that is generally sufficient

[Mario Carneiro]

leading underscore is also used in some places, although lean takes a harder stance here since you can't actually use it in definition names

[Mac]

But that would appear in auto-complete which we want to avoid by marking the definitions private.

[Mario Carneiro]

you could have the effect of private or an equivalent attribute be to hide it from such displays, or the tooling could pick up on the naming convention

[Mac]

The goal is to make private definitions "hidden" in some sense (ex. from auto complete) while still providing a means to access them.

[Daniel Fabian]

private serves three encapsulation purposes in a normal programming language: Hiding stuff in the namespace, preventing corruption of state, and making it impossible to depend on internal details to lower coupling.

[Daniel Fabian]

we need all 3 to still be true after we weaken the restrictions imposed by private.

[Daniel Fabian]

State corruption we get for free due to being a pure language.

[Daniel Fabian]

the other two we have to solve somehow.

[Mac]

In Lean, (2) isn't a concern (as you said), and (3) is just undesirable, because as @Mario Carneiro said proofs sometimes need to do just that.

[Mac]

so only real use is (1)

[Mac]

and since we need to violate that sometimes for the same reason as (3), even it should only hold conditionally.

[Daniel Fabian]

yeah, I see how (3) is a potential concern. We might restrict accessing privates to proofs? It feels a bit weird. But on the other hand, if someone goes through enough effort to access privates, I wouldn't care too much to break them by refactoring. (E.g. in .net you can use reflection to access privates).

[Mac]

Mario Carneiro said:

you could have the effect of private or an equivalent attribute be to hide it from such displays

The disadvantage here is that it would then always hide it (which would be annoying in proofs that rely heavily on it). The .# or whatever syntax would allow for auto-completion in such contexts.

[Johan Commelin]

local attribute [-private] foobar would fix that

[Mario Carneiro]

But on the other hand, if someone goes through enough effort to access privates, I wouldn't care too much to break them by refactoring. (E.g. in .net you can use reflection to access privates).

Exactly. open private isn't a code smell, it is explicitly opting out of stability of the upstream package. When you have dependent types, dependent packages can be a thing too

[Mario Carneiro]

it doesn't need to be easy, but it does need to be possible

[Daniel Fabian]

open private is a bit like .net reflection to access privates.

[Mac]

I think the "private" as an attribute seems reasonable. I would also probably rename it to "hidden" as that is more indicative of what is actually doing.

[Mario Carneiro]

rust has doc(hidden)

[Daniel Fabian]

the experience for writing production code needs to be natural. You can easily have a large-ish development with only very light proving, e.g. lean4 compiler itself.

[Daniel Fabian]

And that kind of thing needs to be natural, so a keyword for private stuff seems warranted.

[Mac]

seems reasonable

[Daniel Fabian]

so... long story short... open private would pretty much cover all the requirements?

[Mario Carneiro]

I think avoiding accidental use of an unstable internal implementation detail is a good reason to have private as a language concept

[Mario Carneiro]

so something like open private is probably the best UX to give it just enough syntax salt. The only thing I would change is that it shouldn't need to be open private foo in bar, which is currently needed due to the absolute hackery going on in the implementation

[Mac]

Daniel Fabian said:

so... long story short... open private would pretty much cover all the requirements?

That and export private as well (for cases where an dependent package disagrees on visibility). It is also currently defined/used in mathlib

[Mario Carneiro]

I have more misgivings about export private, because it's basically saying the upstream author was wrong about their decision

[Mac]

Which as the fallible humans we are, that can, in fact, sometimes be the case. ;)

[Daniel Fabian]

plus you can always emulate it by def foo := private.foo

[Sebastian Ullrich]

I don't mind open private as an escape hatch, but I can almost guarantee that it will not become part of the stdlib, nor will the semantics of private change. On the positive side, that means the current open private code is relatively unlikely to break in the future.

[Mario Carneiro]

I would prefer if private just kept the name as is but made it an error to directly reference

[Mario Carneiro]

rather than mangling the name and/or sticking some _hyg's in there

[Mario Carneiro]

those names are way too hard to reference, even after you have paid the "I know what I'm doing" tax

[Mac]

Daniel Fabian said:

plus you can always emulate it by def foo := private.foo

Sadly, that is semantic different from an alias like that created by export in many cases.

[Sebastian Ullrich]

Mario Carneiro said:

I would prefer if private just kept the name as is but made it an error to directly reference

That would preclude using the same name for privates in module diamonds, which would be super counterintuitive. We went through multiple designs before converging on the current one.

[Mac]

Mario Carneiro said:

those names are way too hard to reference, even after you have paid the "I know what I'm doing" tax

So hard, in fact, that it creates issue #418.

[Mario Carneiro]

Module diamonds?

[Sebastian Ullrich]

private foo in two files you import

[Gabriel Ebner]

Mario Carneiro said:

so something like open private is probably the best UX to give it just enough syntax salt. The only thing I would change is that it shouldn't need to be open private foo in bar, which is currently needed due to the absolute hackery going on in the implementation

You can also do open private something from MyModule now. Not sure if that helps you.

[Mario Carneiro]

While we're on the topic, I've seen some issues with excessive privacy around deriving instance DecidableEq and other automatic constructions

[Gabriel Ebner]

DecidableEq might not be the best example here. The type already contains everything you could prove about it.

[Mario Carneiro]

Actually it was BEq. I'll post the example in another thread