Static semantics v0.1

Static semantics v0.1.  This now contains a fairly complete version of the static semantics for a core language, along with a translation into the same core language extended with a few small primitives.  The insertion of covariance type checks is handled.  Per Siggi's suggestion, I've moved the extended core language primitives into the elaboration section.  The main changes from the last checkin are the treatment of classes, class hierarchies, override checking, etc.  I've added some text to explain the general idea of what's going on.

I've gone ahead an uploaded a pdf version to the site.dev_compiler repository that matches the version in this CL.

BUG=
R=vsm@google.com

Committed: https://github.com/dart-lang/dev_compiler/commit/0727ecf1577da0da56ef9bd07f98db82636d046e

[Leaf, 2015-07-24 21:55:02]

leafp@google.com changed reviewers:
+ jmesserly@google.com, sigmund@google.com, vsm@google.com

[vsm, 2015-07-28 15:44:32]

lgtm

General question....

We currently allow this:

class Foo {
  dynamic baz(dynamic x) => ...;
}

class Bar extends Foo {
  int baz(int x) => ...;
}

Can we treat this uniformly with the generic case - at least at this level?

I.e., can callee vs caller side checking be an implementation detail?

It also occurs to me that if we have:

List<SomeSealedClass> list;  // e.g., int, String, ...
list.add(4); // No runtime checking (callee or caller) is needed ...

This is analogous to the case above - if the receiver is Bar, no checking is
needed.  If the receiver is Foo, we need checking (e.g., a dsend).

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
File doc/definition/static-semantics.tex (left):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:399: \comment{TODO(leafp): specify ground
types}
Did you add a definition of ground type?  I don't see it.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
File doc/definition/static-semantics.tex (right):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:63: \down{\tau} & = & \tau\ \mbox{if $\tau$
is base type.}
What is a "base type" in this case?

Also, if I have (for any T):

class Foo extends List<T> { ... }

Is \down{Foo}  == Foo?

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:681: to match an internal signature which is
in fact covariant in the type
"covariant" -> "soundly covariant"?  I was a little confused here as I think the
external signature is also covariant on the type parameters, but not in a sound
way.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:876: For a method override, we reqire two
coherence conditions.  As before, we
reqire -> require

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:879: $\sigma$ be a subtype of the external
type of the method in the superclass, and
I thought that external types would not soundly subtype due to covariance?

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:891: property that the overriden method must
expect to be used at type
overriden -> overridden

https://codereview.chromium.org/1253143002/diff/1/doc/definition/strong-dart.tex
File doc/definition/strong-dart.tex (right):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/strong-dart....
doc/definition/strong-dart.tex:305: operation, and explicitly checked dynamic
method load operation, and a runtime
"dynamic method load operation" -> "dynamic load operation"?

[Leaf, 2015-07-28 20:34:22]

On 2015/07/28 15:44:32, vsm wrote:
> lgtm
> 
> General question....
> 
> We currently allow this:
> 
> class Foo {
>   dynamic baz(dynamic x) => ...;
> }
> 
> class Bar extends Foo {
>   int baz(int x) => ...;
> }
> 
> Can we treat this uniformly with the generic case - at least at this level?
> 
> I.e., can callee vs caller side checking be an implementation detail?
> 
> It also occurs to me that if we have:
> 
> List<SomeSealedClass> list;  // e.g., int, String, ...
> list.add(4); // No runtime checking (callee or caller) is needed ...
> 
> This is analogous to the case above - if the receiver is Bar, no checking is
> needed.  If the receiver is Foo, we need checking (e.g., a dsend).

This is worth keeping discussing, but I'm not sure I see a way to completely
unify the treatment yet.  There are lots of connections, but in some sense what
I'm trying to do in this formalism is spell out precisely what the
implementation details are.  That is, I think the type system stays the same
with respect to what programs we allow regardless of whether we do callee or
caller side checking, but we have to pick one, and we want to at least
informally be able to see why the implementation is correct (or ideally prove a
soundness result).  Switching to callee side checks for generics would allow us
to elide the checks for concrete subclasses of generics, but would require
either a second (checked) entry point for use when used at the generic type, or
else callee side checks that might be onerous in terms of readability.  Having
two entry points might be the best solution - you might be able to produce the
entry point just once in the generic super class.  Something to consider.

[Leaf, 2015-07-28 20:34:29]

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
File doc/definition/static-semantics.tex (left):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:399: \comment{TODO(leafp): specify ground
types}
On 2015/07/28 15:44:32, vsm wrote:
> Did you add a definition of ground type?  I don't see it.

Done.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
File doc/definition/static-semantics.tex (right):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:63: \down{\tau} & = & \tau\ \mbox{if $\tau$
is base type.}
On 2015/07/28 15:44:32, vsm wrote:
> What is a "base type" in this case?

Anything which is not one of the previous three cases.  Maybe I should just say
"otherwise".

> Also, if I have (for any T):
> 
> class Foo extends List<T> { ... }
> 
> Is \down{Foo}  == Foo?

Yes.  I'm a little bit informal with the syntax in a way that doesn't matter. 
Technically in this syntax, you would have to write Foo<>.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:681: to match an internal signature which is
in fact covariant in the type
On 2015/07/28 15:44:32, vsm wrote:
> "covariant" -> "soundly covariant"?  I was a little confused here as I think
the
> external signature is also covariant on the type parameters, but not in a
sound
> way.

Rephrased and clarified.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:876: For a method override, we reqire two
coherence conditions.  As before, we
On 2015/07/28 15:44:32, vsm wrote:
> reqire -> require

Done.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:879: $\sigma$ be a subtype of the external
type of the method in the superclass, and
On 2015/07/28 15:44:32, vsm wrote:
> I thought that external types would not soundly subtype due to covariance?

In the presence of variant type parameters, you can think of their being two
aspects to sound subtyping.  1) Are the parameters used according to their
variance, and 2) are the types subtypes.  When we say that we have covariant
generics, what we mean is that we elide #1, and just pretend all type parameters
are only used covariantly, even though they aren't.  We do still require that #2
hold though.  So if we're subtyping List<int> and overriding add, our external
type needs to be a subtype  of int -> void: we don't allow you to override with
String -> void, but you could override with Object -> void.  The subtyping is
correct, but because List is not actually covariant in T, the override is still
unsound: add originally had type T -> void, which is not covariant in T.  The
internal type of add in List will be dynamic -> void, which is properly
covariant, and so the internal override is sound.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/static-seman...
doc/definition/static-semantics.tex:891: property that the overriden method must
expect to be used at type
On 2015/07/28 15:44:32, vsm wrote:
> overriden -> overridden

Done.

https://codereview.chromium.org/1253143002/diff/1/doc/definition/strong-dart.tex
File doc/definition/strong-dart.tex (right):

https://codereview.chromium.org/1253143002/diff/1/doc/definition/strong-dart....
doc/definition/strong-dart.tex:305: operation, and explicitly checked dynamic
method load operation, and a runtime
On 2015/07/28 15:44:32, vsm wrote:
> "dynamic method load operation" -> "dynamic load operation"?

The syntax is a little deceptive - there are really two load operations in this
core language: loading a method (e.m) and loading a field (this.x).  The syntax
is ambiguous in that "this" is an expression, so you can (for example) say
this.m to load a method named "m" from the expression "this", or to load a field
name "m" from "this".  Think of their being two different AST nodes that happen
to pretty-print the same.  I informally distinguish them by using the
metavariables m and x for methods and fields.  Perhaps I should make this less
ambiguous, but it's a little convenient.

[vsm, 2015-07-28 21:02:24]

lgtm

[Leaf, 2015-07-28 22:29:18]

Committed patchset #2 (id:20001) manually as
0727ecf1577da0da56ef9bd07f98db82636d046e (presubmit successful).