DIP1000

[Andrei Alexandrescu via Digitalmars-d]

Some progress with the DIP1000 semantics. So I made a few changes to the 
grammar of the mini-language (call it MiniD1000), which is at 
http://erdani.com/d/DIP1000-grammar.html. Notable aspects:

* Programs are a sequence of function definitions, struct definitions, 
and global variable definitions. A pass is supposed to go through all 
and create the initial typing environment.

* Functions now only have one parameter. This is to reduce the size of 
the language (two parameters increase the numbers of typing and 
evaluation rules). Aliasing can be studied with globals. I'm unclear 
whether we need the second parameter for investigating things like 
cross-parameter aliasing; if so, I'll add it back.

* All functions are required to end with a return statement. This avoids 
any need for flow control.

* There are no rvalues in MinbiD1000, which I thought is quite clever. 
That means `null` and integral literals are not expressions; they are 
explicitly present in assignment statements. This simplifies MiniD1000 a 
great deal, but again will require us to be careful when we "port" 
whatever conclusions we draw back to D.

* The `if` statement has no `else` clause. It only increases the size of 
the language without an increase in expressiveness.

Next, I defined a baseline set of typing rules at 
http://erdani.com/d/DIP1000-typing-baseline.html for "bad" MiniD1000: 
all ref, scope and return attributes are ignored, so there's no special 
protection against bad escapes. Based on these rules we'll later define 
better rules that enforce safety. A few notes:

* For a general understanding on how to read these rules, see the 
Featherweight Java (FJ) paper or see e.g. 
http://www.hedonisticlearning.com/posts/understanding-typing-judgments.html.

* Like in FJ, sequences of zero or more things are shown with an overbar.

* In order to identify the current function being compiled, I introduce 
the symbol f_{crt}. For example, in rule S-VarDeclaration, a 
prerequisite of the judgment is that f_{crt} exists, i.e. the rule 
S-VarDeclaration only applies inside a function, not outside. For the 
outside rule see D-GlobalVarDeclaration.

* S-VarDeclaration introduces a new name visible to the statements that 
follow. This is done by typing not only the variable declaration, but 
also all following statements in its scope. The typing environment for 
the statements is the union of the preexisting typing environment and 
the new variable.

* In fact the typing rules of all statements carry the appendix "and 
here are the following statements in the scope" which is workable but 
possibly a bit goofy. Any cleverer idea?

* For that matter I need the rule S-NoStmts: "a sequence of zero 
statements types just fine".

* In D-Struct, I vaguely state that a struct shall not be a transitive 
field of itself. Is there a better way to enforce that succintly?

Please let me know of anything I missed or got wrong. Once the baseline 
typing is in place, the hard part starts: defining the enhanced typing 
that enforces safe scoping rules.


Thanks,

Andrei