Package names being PascalCase

Stream: mathlib4

[Tesla Zhang]

What is the motivation behind package names being in PascalCase? I've read https://leanprover.zulipchat.com/#narrow/stream/270676-lean4/topic/what.20naming.20scheme.20to.20use.20in.20mathlib4 and https://github.com/leanprover-community/mathlib4/wiki/Porting-wiki#naming-convention but they don't seem to explain why. I'm curious.

[Mario Carneiro]

Package names aren't in pascal case for the most part. E.g. the package names for batteries and mathlib4 are batteries and mathlib respectively. Other packages include Qq, aesop, proofwidgets, Cli, importGraph so there isn't a strict enforcement of whether they should be uppercase or lowercase, but I think lowercase is winning. The Qq and Cli packages are using the rule that the package is named after the library, and these are always in PascalCase.

[Tesla Zhang]

I think there's a misunderstanding: when I said package name I should've said module names

image.png

[Kyle Miller]

I'm curious what would count as a motivation. Are you trying to work out some of the history of Lean 4's design? What's your own motivation?

Usually the choice of this naming convention style is arbitrary. Pascal case for module names is what Lean 4 uses, so that's what Mathlib uses.

[Utensil Song]

Personally I'm a bit confused by the naming of Module (PascalCase), Package (could be any case pattern without a - or _ except for «doc-gen4») and Repo (could be anything with a - or _, and possibly a lean prefix/postfix, and a 4 postfix), the naming pattern between them are not consistent and quite arbitary.

Mostly a user would only need to require mathlib (or just batteries) , «doc-gen4», checkdecls, Duper, LeanCopilot etc. but almost all variants are already there (except for camelCase).

[Utensil Song]

I've lost a preference on the naming convention after learning many languages, but in one language, I simply hope it to be consistent. (One exception is C++, I can only hope so for one library, that means I have to switch styles in one function if it calls multiple libraries.)

[Tesla Zhang]

Kyle Miller said:

I'm curious what would count as a motivation. Are you trying to work out some of the history of Lean 4's design? What's your own motivation?

Usually the choice of this naming convention style is arbitrary. Pascal case for module names is what Lean 4 uses, so that's what Mathlib uses.

I'm trying to develop a competitor of Lean and I'm learning from Lean. Right now it features in a better treatment of mutually recursive definitions and fully constructive funExt & quotients via a set-level cubical type theory (LEM/AC will still need to be an axiom though), very similar to Arend, but Arend is based on HoTT, and we are more aligned with Lean in this regard.

But it does not yet have a class system & tactic framework therefore we're not ready to work on the ecosystem, but I am overlooking.

I've already realized an unfortunate fact that if you imitate Haskell, using data as the keyword will clash with the lowercase module name data for functional programming data structures, such as lists and options, I think that's why Haskell used Data.List capitalized. But Lean uses inductive and has lowercase in mathlib3, but mathlib4 is uppercase. I just want to know if there's some motivations that I can learn.

[Kyle Miller]

Ah, ok, interesting.

Just so you know, module names in Lean will never clash with keywords. Modules are only for imports, but there's also a namespace system which is orthogonal to modules. This is somewhat reminiscent of Common Lisp, which differentiates between modules (for loading files) and symbol packages (for namespacing).

Lean and mathlib also use Pascal case for namespaces. I hadn't really thought about how this ensures that namespaces will never conflict with keywords (which are all(?) lower case), but I suppose that could be convenient. I can't immediately think of an example clash between existing namespaces and keywords if suddenly they all became case insensitive however.

[Tesla Zhang]

Our language design is closer to Rust and Agda in this case, where we have file level modules and file-local modules. But it is true that file level modules are significant in type checking, as we don't allow cross-module mutual recursion. But for file-local modules this is easily doable, I'm not sure if it's implemented or not, I need to check.

But thanks for your questions & answers! They are very helpful

[Tesla Zhang]

https://www.aya-prover.org/guide/prover-tutorial.html here's some code snippets of the language