Add identifiers to modules

[brprice]

Description

This is a feature request to continue the implementation of a module system started in #265. We will add module identifiers to avoid the requirement that globally-referable identifiers (Names and IDs) are unique in a Prog, which causes issues when importing.

Dependencies

None

Spec

We add module identifiers, and every global reference will now need to include a reference to a particular module. These module identifiers will be assumed to be globally unique (i.e. within one "Primer ecosystem", whatever that means). However, this will not be enforced yet -- we will tie this into a student's account, and thus needs some auth work. For now we will enforce that these identifiers are unique within one Prog by letting imports fail irrecoverably if there is a clash.

This has the effect of weakening the current requirement that identifiers must be unique within a Prog to only within a Module. Thus our fresh-name/id generation mechanism is again sound. (Previously, it was easy for two independent programs to both have a global definition with id 0, in which case it was unsound to import one into the other. This has particular implications for our testsuite and standard library)

Implementation details

Should module identifiers be human readable, or should we just have a mapping from identifiers to nice strings? If they are human readable, it makes human-naming things harder, as one needs a good globally unique name. If they are uuids (or similar) it is easy to give everything a unique name, but we then have to worry about clashes in the display names. These clashes are not problematic in theory, but may be confusing (either you cannot tell which module a thing refers to, or we will have to change how we display things in the case there is a clash). To avoid confusion, we will enforce unique-human-names in either approach. Thus we decide to just make identifiers human readable, as uuids do not buy us much and are more complex.

A module identifier will just be a list of strings (a la haskell). It is the user's responsability to use this hierarchy sensibly.

Note that module identifiers of imported modules will be immutable, but we will let students rename their local module. (And then any hypothetical "publish" action will have to freeze it)

Both local module(s) and imported modules should have identifiers, for consistency when we enable multiple local modules. Any future "publish" action will have to freeze an immutable copy of a module under a new name. Thus one component of a module identifier should be some sort of version number. We will let students rename their editable module.

All global names/IDs will have a module prefix (i.e. "be fully qualified"): both references and definitions. This is motivated by consistency: consider data Nat = Zero | Succ Nat: this contains a definition of and a reference to Nat. It would be rather odd if only one of these had a module prefix. We clearly wouldn't want to show this fully-qualified like data builtins.Numeric.Nat = builtins.Numeric.Zero | builtins.Numeric.Succ builtins.Numeric.Nat in the frontend, but that is an easy matter to deal with in rendering code.

Not in spec

Specifying exactly what a module identifier is (i.e. something like "first component is a username...") and enforcing global uniqueness (in the DB) of module identifiers. (This can wait for accounts, so we can do better scoping and only need unique-to-a-user)

Deleting modules and/or imports (we will tackle this after we tackle the same issue with type definitions)

Most not-in-spec things from #265 apply (but are obviously orthogonal).

Module dependency tracking. Now we have a nice way to refer to a module, we could use this to succinctly cache which modules depend on which others, which would be a useful optimisation when wanting to do a transitive import, or decide what to typecheck when we have multiple editible modules. However, this would be a premature optimisation.

Discussion

None

Future work

See "Not in spec"

[dhess]

Looks good. One thought:

Not in spec

Enforcing global uniqueness (in the DB) of module identifiers. (This can wait for accounts, so we can do better scoping and only need unique-to-a-user)

Any early thoughts on how we might implement the account scoping?

Presumably if we have Module.termName and Module.TypeName, then with accounts we might have "dhess@hackworthltd.com".Module.termName and "dhess@hackworthltd.com".Module.TypeName; i.e., we prefix module-scoped IDs with an account ID.

We'll eventually have built-in modules that are visible to all students in a given Primer ecosystem (as you call it); e.g., the Prelude. Using the above schema, then we'd have something like builtin.Prelude.map, where builtin is a reserved pseudo-account ID.

Anyway, what I'm getting at is this: if we're reasonably confident we'll want to use an account ID prefix, does it make sense to implement this now, in this feature spec? And that until we have accounts, everything is just builtin by default, even student-created modules?