Don't understand imports and opens?

Stream: new members

[aron]

After a lot of trial and error I figured out that I can import the HashMap data structure by importing Std.Data.HashMap.Basic and referencing it like Std.HashMap:

import Std.Data.HashMap.Basic

abbrev MyMap := Std.HashMap String Nat

and I can avoid the Std prefix by opening Std:

import Std.Data.HashMap.Basic
open Std

abbrev MyMap := HashMap String Nat

1. But why is HashMap in the Std namespace when it's defined in Std.Data.HashMap.Basic?

2. It looks like I can skip the Basic in the import path. Is that because lean/Std/Data/HashMap.lean imports Std.Data.HashMap.Basic? Does that mean that importing Std.Data.HashMap includes everything HashMap.lean imports, i.e. it works sort of like an include?

3. Even if that's the case, I still don't get how import Std works, because there is no lean/Std.lean file, so what module does that import actually reference?

[Markus Himmel]

1. There is no one-to-one correspondence between namespaces and files.
2. Yes, imports are transitive.
3. There is in fact such a file: https://github.com/leanprover/lean4/blob/master/src/Std.lean

[Damiano Testa]

Also, import gives you access to the declarations in a given file, regardless of their namespace. open allows you to refer to the available declarations by shorter names depending on what you opened. The two mechanisms are independent of each other, although modules and namespaces tend to have similar names, since those are often chosen semantically.

[aron]

@Markus Himmel:

1. so when I import a module I'm referring to a file location, not a namespace? but hm yeah I can see now that lean/Std/Data/HashMap/Basic.lean type declares the HashMap type as being in namespace Std
2. ok :+1:
3. oh yeah you're right :man_facepalming: I was looking at the wrong location (inside the lean/Std/ directory instead of inside lean/)

[aron]

I'll be honest I find it very confusing that you import based on file location but you reference a type/value based on namespace. That seems inconsistent.

In the .NET world for example if you want to import a type, you import and qualify the type name by the same thing: its full module name (which is namespace based)

[Markus Himmel]

aron said:

1. so when I import a module I'm referring to a file location, not a namespace?

Yes, this is correct. I would say this makes sense in Lean because we must make sure that there is some notion of "before" such that every declaration only refers to declarations that came before it, to prevent introducing logical inconsistencies through circular reasoning. A natural way to ensure this is by having files import each other and forbidding cyclic imports.