DIP1000

[Timon Gehr via Digitalmars-d]

On 14.09.2016 21:49, Andrei Alexandrescu wrote:
> 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.
> ...

There probably should be typing rules for that.


> * 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.
> ...

I would support an arbitrary number of parameters. Leaving that out does 
not buy much in terms of simplicity, and it makes miniD quite a lot less 
relevant for arguing about the soundness of the full language.


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

How so? You still allow return statements at arbitrary places in the 
function.

> * There are no rvalues in MinbiD1000,

Yes there are. Function calls might be rvalues because 'ref' is optional 
on them.

> 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.
> ...

That should be fine. I think a better way is to special-case only the 
lhs though. I.e. x=e, *e₁=e₂, f(e₁,…,eₙ)=eₙ₊₁.


> * 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:
>

Looking good, except:

- struct types are not checked for existence.

E.g. the following program type checks:

void main(){
     Undefined x;
     Undefined* y=&x;
}

- 'fields' is not defined. (And how is it supposed to know what the 
fields of some syntactic type are?) Probably struct declarations should 
be part of the environment, then 'fields' can take the environment as an 
additional argument. I think it would make sense if your grammar 
enforced that all struct declarations come before all global variables 
which come before all function declarations.

- Functions cannot call each other, because they cannot look up each 
other's names.


> * 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?
> ...

I think it is fine.


> * 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.

Well, the notation does not really make a lot of sense.

> Is there a better way to enforce that succintly?
> ...

Typing rules for structs need to state that all struct declarations 
together are fine if each struct is fine individually given all other 
structs present in the environment.

Then define something like

transitiveFieldTypes(Γ,S) :=
     μX. {T | ∃x. T x; ∈ (fields(Γ,S) ∪ ⋃{ fields(Γ,T') | T'∈X }) }

(In English: transitiveFieldTypes(Γ,S) is the smallest set such that all 
field types of S and field types of other types in the set are also in 
the set.)

You can then require that S∉transitiveFieldTypes(Γ,S)

> 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.
> ...

Maybe we should define the semantics first (it is easier and it is 
necessary for providing formal counter-examples for the soundness of 
proposed typing rules).