docs: add variables; rework scope

[rhendric]

Motivation

Part of #10970.

Starting in on formally specifying the language grammar. Semantics of variables and scopes are very closely coupled so I did the two pages together.

Some language here is driven by the existing error messages. I might have called ‘variables’ ‘identifier expressions’ instead, and I might have called ‘definitions’ ‘bindings’ as they were previously documented. But if you try to evaluate xyzzy, the error message says undefined variable 'xyzzy', so I figured it'd be better to standardize on those words. (Plus, not calling scope entries ‘bindings’ will make it less confusing when I start talking about ‘binds’ as the things that let-expressions and attribute set literals contain.)

There are, of course, a few equivalent ways to describe how scope and name lookup works. I went with the one I think is simplest, but I'd like to get agreement on this early, because it'll affect how I explain things like call-by-need evaluation later.

Priorities and Process

Add 👍 to pull requests you find important.

The Nix maintainer team uses a GitHub project board to schedule and track reviews.

[fricklerhandwerk]

I think this distinction is over-complicating things. We can merely list definition types and add the details in place instead of referring to more details and potentially having to duplicate information.

[rhendric]

I don't understand what you're proposing here. If you meant to mark this line, what alternative would you propose for listing definition types, and where is ‘in place’?

[fricklerhandwerk]

I would just list the definition types directly without classifying them into explicit and implicit, and explain the semantics of each in their own respective section/page.

[rhendric]

Hm. Perhaps I've written this confusingly.

The thing this paragraph is trying to express is that we have (conceptually):

enum DefinitionType { Implicit, Explicit };
using Scope = std::map<Name, std::pair<Expr, DefinitionType>>;

It happens to be the case that the expressions that extend scopes can be classified into implicit and explicit, but that doesn't matter for purposes of defining what data a scope contains. A hypothetical Nix language extension could allow let-expressions to create both implicit and explicit definitions, for example:

let
  a = 1;
  implicit b = 2;
in ...

But there is a meaningful difference between the scopes $\{ \texttt{"a"} \mapsto (1, \mathit{implicit}) \}$ and $\{ \texttt{"a"} \mapsto (1, \mathit{explicit}) \}$; the difference is revealed by the fact that with { a = 2; }; a evaluates to 2 in the former scope and 1 in the latter. So the difference should be explained in the description of what a scope is.

The previous version of this documentation achieved this goal by partitioning scopes into primary and secondary maps, like so:

struct Scope {
  std::map<Name, Expr> primary;
  std::map<Name, Expr> secondary;
}

This is isomorphic to the other Scope type, but when I tried explaining the concepts ‘primary’ and ‘secondary’, I noticed that they don't really connect to the language we naturally use to describe the special behavior of definitions created by with. We naturally describe those definitions as implicit, so I thought it would be easier to understand if I took the implicit/explicit distinction and applied it directly to definitions (map entries) in scopes.

(There's also the fact that the primary/secondary presentation allows for the same name to be a key in both ‘subscopes’, which is why the two presentations aren't isomorphic. This makes describing shadowing a little simpler, but makes describing variable resolution more complex (first check the primary subscope, then the secondary subscope). With the implicit/explicit presentation, all of that is handled in the description of shadowing.)

[fricklerhandwerk]

I understood what you were trying to achieve, but I think it front-loads a lot of complexity. IMO we have to design the manual for incremental reading, and putting too much operational detail into an overview will just destroy reader's motivation to plow through the rest. Therefore I'm suggesting working out the details in the respective definition types, and e.g. be appropriately more diligent when describing the semantics of with.

[rhendric]

I was thinking of this as a specification of what ‘scope’ means, not an overview.

There should be, somewhere, a reference-level specification of what a scope is, so that other places in the language reference can link to that when scopes are mentioned.

If not here, where should that specification go?

[fricklerhandwerk]

I gave it another thought, and yes, that's probably the best way to do it. Thanks for the productive discussion and sorry for the delay.

[rhendric]

Suggested change

	The respective definition types *extend* their enclosing scope by adding new definitions, or replacing existing ones with the same name.
	The expressions listed above *extend* their enclosing scope by adding new definitions, or replacing existing ones with the same name.

Having just defined ‘definition types’ to mean the set {implicit, explicit}, I don't think it should be used in this sentence.