[dart-misc] Notes from 8/26 DEP meeting

['Bob Nystrom' via Dart Misc]

Here's my notes:

https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md

Cheers!

- bob

[Günter Zöchbauer]

Thanks for the update!

Post by 'Bob Nystrom' via Dart Misc
https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md
Cheers!
- bob

[Patrice Chalin]

Bob et al.,

Excellent resolutions at the last meeting! In particular:

broaden the scope of this meeting to be more proactive about driving the

evolution of the language

As for other topics ...

*Splitting the spec
<https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md#splitting-the-spec>*

... suggests we would split the spec in two: the dynamic and static

[semantics].

Very good suggestion too. This will bring us one step closer to support of
a theoretical and tooling infrastructure for pluggable type systems ---
which Gilad mentioned in slide 24
<https://www.dartlang.org/slides/2011/11/stanford/dart-a-walk-on-the-dart-side.pdf#page=24>
of
this presentation on Dart:

*What about a real, sound, type system?*

There is no privileged type system, but pluggable types are possible

B.t.w, if such major rework is to be done to the spec, I suggest that edits
be made to the grammar so that a *reference implementation of the parser
can be auto generated from the spec*. Right now, I don't think that *any*
of the Dart tooling front-ends match the grammar in the specification
exactly.

*Nullable types
<https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md#nullable-types>*

Florian started a discussion about whether we think a nullable type should

be assignable to a non-nullable one. In other words, can you implicitly
"cast" the nullability away.

This is the type of one-off semantics that I was warning against earlier
<https://groups.google.com/a/dartlang.org/d/msg/core-dev/aNbvqxIPiI4/EkOb27mvBwAJ>
(one-off vs. a semantics we might have for generalized union types (and the
rest of Dart types for that matter), of which nullable types are a special
case) --- and to which Bob issued a response here
<https://groups.google.com/a/dartlang.org/d/msg/core-dev/aNbvqxIPiI4/zVZvyAnJBwAJ>
.

But, if the dynamic and static semantics are split off into separate
artifacts, then maybe any final decisions about permitting implicit nullity
downcasts can be delayed (or left under the control of an experimental flag
for some variant of the type system).

I'll address other topics in separate threads so that we can keep
discussions focused.

On Mon, Aug 31, 2015 at 5:24 PM, 'Bob Nystrom' via Dart Core Development <

https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md
Cheers!
- bob

--
Patrice [image: View my LinkedIn Profile.]
<http://www.linkedin.com/in/patricechalin> [image: Google+ Profile.]
<https://plus.google.com/+PatriceChalin>

['Brian Wilkerson' via Dart Misc]

Patrice,

B.t.w, if such major rework is to be done to the spec, I suggest that edits

Post by Patrice Chalin
be made to the grammar so that a *reference implementation of the parser
can be auto generated from the spec*. Right now, I don't think that *any*
of the Dart tooling front-ends match the grammar in the specification
exactly.

I'm not disputing your claim, but I would love to see some examples and get
those examples turned into tests. If you know of specific issues, could you
please provide some of those examples?

Brian

[Patrice Chalin]

Hi Brian,

Post by 'Brian Wilkerson' via Dart Misc
I'm not disputing your claim, but I would love to see some examples and
get those examples turned into tests. If you know of specific issues, could
you please provide some of those examples?

See Section 4 of the DEP for Metadata for Type Annotations
<https://github.com/chalin/DEP-metadata-for-type-annotations>. As explained
in section 4.1

there are discrepancies between the grammar contained in the language

Post by 'Brian Wilkerson' via Dart Misc
program points where annotations are accepted by tooling but should be
rejected according to the grammar. The converse situation is marked using

The @X and /*@!*/ markings are used in the "general sample library
declaration" given in Section 4.2
<https://github.com/chalin/DEP-metadata-for-type-annotations/blob/master/proposal.md#42-library-and-part-declarations>.
These discrepancies surfaced during implementation, in the Analyzer, of DEP
30 (non-null types) via annotations, rather than via changes to the syntax
<https://github.com/chalin/DEP-non-null/blob/master/doc/dep-non-null-AUTOGENERATED-DO-NOT-EDIT.md#ii1-variant-of-proposal-implemented-in-the-dart-analyzer>.
(Btw, I may not have identified/noted all discrepancies since I used a
convenient work-around (embedding annotations inside comments) and decided
to focus on the Analyzer implementation instead of grammar issues.)

Cheers
--
Patrice [image: View my LinkedIn Profile.]
<http://www.linkedin.com/in/patricechalin> [image: Google+ Profile.]
<https://plus.google.com/+PatriceChalin>

['Brian Wilkerson' via Dart Misc]

Patrice,

Thanks! I had forgotten about those. I suppose that the analyzer ought to
produce an error in those places where it's accepting an annotation and it
shouldn't be, but it doesn't seem like a very high priority task :-)
Certainly not as concerning an issue to me as I thought you might have
found. But then, I wouldn't mind allowing annotations in more places, so
perhaps that's coloring my perception.

Brian

Post by Patrice Chalin
Hi Brian,

Post by 'Brian Wilkerson' via Dart Misc
I'm not disputing your claim, but I would love to see some examples and
get those examples turned into tests. If you know of specific issues, could
you please provide some of those examples?

See Section 4 of the DEP for Metadata for Type Annotations
<https://github.com/chalin/DEP-metadata-for-type-annotations>. As
explained in section 4.1
there are discrepancies between the grammar contained in the language

Post by 'Brian Wilkerson' via Dart Misc
program points where annotations are accepted by tooling but should be
rejected according to the grammar. The converse situation is marked using

declaration" given in Section 4.2
<https://github.com/chalin/DEP-metadata-for-type-annotations/blob/master/proposal.md#42-library-and-part-declarations>.
These discrepancies surfaced during implementation, in the Analyzer, of
DEP 30 (non-null types) via annotations, rather than via changes to the
syntax
<https://github.com/chalin/DEP-non-null/blob/master/doc/dep-non-null-AUTOGENERATED-DO-NOT-EDIT.md#ii1-variant-of-proposal-implemented-in-the-dart-analyzer>.
(Btw, I may not have identified/noted all discrepancies since I used a
convenient work-around (embedding annotations inside comments) and decided
to focus on the Analyzer implementation instead of grammar issues.)
Cheers
--
Patrice [image: View my LinkedIn Profile.]
<http://www.linkedin.com/in/patricechalin> [image: Google+ Profile.]
<https://plus.google.com/+PatriceChalin>

[Patrice Chalin]

... Certainly not as concerning an issue to me as I thought you might have
found.

I'm sorry if I gave a wrong impression about things being way off. That
wasn't my intent.

But then, I wouldn't mind allowing annotations in more places, so perhaps

that's coloring my perception.

I agree. In fact, DEP 32 is asking that annotations be allowed in more
places :)

Cheers,
Patrice

Post by Patrice Chalin
Hi Brian,
On Tue, Sep 1, 2015 at 4:18 PM, Brian Wilkerson <

Post by 'Brian Wilkerson' via Dart Misc
I'm not disputing your claim, but I would love to see some examples and
get those examples turned into tests. If you know of specific issues, could
you please provide some of those examples?

See Section 4 of the DEP for Metadata for Type Annotations
<https://github.com/chalin/DEP-metadata-for-type-annotations>. As
explained in section 4.1
there are discrepancies between the grammar contained in the language

Post by 'Brian Wilkerson' via Dart Misc
program points where annotations are accepted by tooling but should be
rejected according to the grammar. The converse situation is marked using

declaration" given in Section 4.2
<https://github.com/chalin/DEP-metadata-for-type-annotations/blob/master/proposal.md#42-library-and-part-declarations>.
These discrepancies surfaced during implementation, in the Analyzer, of
DEP 30 (non-null types) via annotations, rather than via changes to the
syntax
<https://github.com/chalin/DEP-non-null/blob/master/doc/dep-non-null-AUTOGENERATED-DO-NOT-EDIT.md#ii1-variant-of-proposal-implemented-in-the-dart-analyzer>.
(Btw, I may not have identified/noted all discrepancies since I used a
convenient work-around (embedding annotations inside comments) and decided
to focus on the Analyzer implementation instead of grammar issues.)
Cheers
--
Patrice [image: View my LinkedIn Profile.]
<http://www.linkedin.com/in/patricechalin> [image: Google+ Profile.]
<https://plus.google.com/+PatriceChalin>

['Erik Ernst' via Dart Misc]

Post by Patrice Chalin
Bob et al.,
broaden the scope of this meeting to be more proactive about driving the

evolution of the language

As for other topics ...
*Splitting the spec
<https://github.com/dart-lang/dart_enhancement_proposals/blob/master/Meetings/2015-08-26%20DEP%20Committee%20Meeting.md#splitting-the-spec>*
... suggests we would split the spec in two: the dynamic and static

[semantics].

Very good suggestion too. This will bring us one step closer to support of
a theoretical and tooling infrastructure for pluggable type systems ---
which Gilad mentioned in slide 24
<https://www.dartlang.org/slides/2011/11/stanford/dart-a-walk-on-the-dart-side.pdf#page=24> of
*What about a real, sound, type system?*

There is no privileged type system, but pluggable types are possible

B.t.w, if such major rework is to be done to the spec, I suggest that
edits be made to the grammar so that a *reference implementation of the
parser can be auto generated from the spec*. Right now, I don't think
that *any* of the Dart tooling front-ends match the grammar in the
specification exactly.

We actually need to specify two languages at runtime (Dart-checked-mode and
Dart-production-mode) and one static analysis of a given piece of code; the
relationship between Dart-checked-mode and the static analysis as well as
the relationship between Dart-production-mode and the static analysis are
separate topics as well. Soundness (and various variants thereof such as
message-safety) may or may not apply, depending on the decisions made about
various details. On top of that, we may choose to describe more than one of
those topics in one document. But Dart-checked-mode is a runtime semantics,
not a part of static analysis!

With that, there could be a sound type system for Dart-any-mode (no need to
talk about runtime type checks if they are provably going to succeed), and
there could be a message-safe type system for Dart-checked-mode (which
implies heap soundness: every reference refers to an instance of a class
which is a subtype of the class denoted by the type annotation, if any, or
it is null (if nullable ;)), and there could be many other variants
(possibly supporting additional concepts like nullability or ownership or
un-taintedness etc.etc.).

But, as Gilad usually notes, it is going to be difficult if your 500
library program relies on 500 different pluggable type checkers (well, 2 is
probably enough), each of which will inevitably fail on some of those
libraries.

best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÞbenhavn K, Denmark
CVR no. 28866984