[dart-misc] Dart 2.0 and Types

I think it's worthwhile to point out that the theory of Dart can be that it
is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

To me, that's far beyond "documentation". I'm not sure that it is covered
by the words "static analysis" that you include. It is a property which is
expressed using type annotations, but the crucial fact is that it is
strictly maintained at runtime.

Post by kc
*late 90's *
Java - 'bondage and discipline' OO typing.
*early-mid 2000's*
Frustration with above - the rise of the dynamic lang's Python, Ruby, PHP
on the server. JS with ajax on client.
C# eventually acquires 'dynamic' under pressure from these langs.
*mid 2000's onwards*
rise of the static functional langs via Scala, F# and a renewed
appreciation of ML/Haskell.
anon objects. Dev's seem to prefer it to 'dynamic'
*2014*
Apple goes from trad OO Objective C to something more functional - Swift.
TypeScript wins on the web with static analysis.
But ClojureScript keeps the dynamic spirit alive.
Dart has a 'theory' - everything is an object - methods resolution is
dynamic at runtime - types are for documentation and static analysis. But
do developers understand or appreciate this theory?
(I like it - especially if combined with value objects/immutability and
concurrency).
Will the developers who may take a look at Dart when Flutter firms up
understand this theory?
K.
--
For other discussions, see https://groups.google.com/a/dartlang.org/
For HOWTO questions, visit http://stackoverflow.com/tags/dart
To file a bug report or feature request, go to http://www.dartbug.com/new
To unsubscribe from this group and stop receiving emails from it, send an

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

2015-10-05 13:14:35 UTC

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be that
it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

Do developers understand or care about this theory? Has the Dart team
communicated/sold this theory to developers? And most importantly for
mobile - does the checked mode sound heap offer performance advantages.
Currently I think production mode does not - or is that wrong?

K.

Post by 'Erik Ernst' via Dart Misc
To me, that's far beyond "documentation". I'm not sure that it is covered
by the words "static analysis" that you include. It is a property which is
expressed using type annotations, but the crucial fact is that it is
strictly maintained at runtime.

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

'Erik Ernst' via Dart Misc

2015-10-05 13:33:23 UTC

I think developers can _benefit_ from caring about guaranteed properties of
program executions. In this case it would be "in checked mode you can trust
all type annotations", which should be useful for programmers to have in
mind, even if they are not the kind of people who would want to go and
prove it.

With respect to the performance advantages: As soon as checked mode checks
are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.

You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md) where
many of the same ideas have been applied.

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

Benjamin Strauß

2015-10-05 14:32:53 UTC

In hindsight I think maybe it would have been better if typed code would
always be running in checked mode. I think many developers struggle with
the idea of an unsound typesystem. I once tried to explain it to someone,
it took me an hour, after which I gave up. Some people have been living in
the typed world for so long, they have problems to grasp other concepts.

I think the simpler approach would have worked better, while keeping the
current semantics (no type overloading, etc.):

typed code -> has to be sound
untyped code/type dynamic -> works like javascript

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode checks
are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984

'Erik Ernst' via Dart Misc

2015-10-05 15:01:09 UTC

I think you have just described checked mode. ;-)

I've often argued similarly "why not run in checked mode, also in
deployments?", but the (not so crazy ;) counter-argument is typically that
crashes are crashes for the end-user, and it does not help much that your
heap is sound until the last nanosecond. The counter-counter-argument is of
course that running with an unsound heap means running with an inconsistent
state, so you don't want that inconsistent state to bleed into persistent
objects like disk files. You could even use this to make the choice: Some
applications will do local work for an end-user in a browser, and anything
that it comes up with will not really matter before it has been received
and validated by a server; in contrast, a Dart process running on a server
(or a process on a "client host" that stores data locally) would benefit
from avoiding those definitely-inconsistent states, even if it means that
it will "crash" a little earlier, and maybe even a little more often.

Post by Benjamin StrauÃ
In hindsight I think maybe it would have been better if typed code would
always be running in checked mode. I think many developers struggle with
the idea of an unsound typesystem. I once tried to explain it to someone,
it took me an hour, after which I gave up. Some people have been living in
the typed world for so long, they have problems to grasp other concepts.
I think the simpler approach would have worked better, while keeping the
typed code -> has to be sound
untyped code/type dynamic -> works like javascript

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984
--

For other discussions, see https://groups.google.com/a/dartlang.org/
For HOWTO questions, visit http://stackoverflow.com/tags/dart
To file a bug report or feature request, go to http://www.dartbug.com/new
To unsubscribe from this group and stop receiving emails from it, send an

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

Benjamin Strauß

2015-10-05 15:19:13 UTC

Isn't performance also a point for 'always checked mode'? Bob mentioned in
another thread that it would help with optimizations.

I get the idea and benefits of optional typing. But Dart's unsoundness
always seemed a bit strange to me.

Post by 'Erik Ernst' via Dart Misc
I think you have just described checked mode. ;-)
I've often argued similarly "why not run in checked mode, also in
deployments?", but the (not so crazy ;) counter-argument is typically that
crashes are crashes for the end-user, and it does not help much that your
heap is sound until the last nanosecond. The counter-counter-argument is of
course that running with an unsound heap means running with an inconsistent
state, so you don't want that inconsistent state to bleed into persistent
objects like disk files. You could even use this to make the choice: Some
applications will do local work for an end-user in a browser, and anything
that it comes up with will not really matter before it has been received
and validated by a server; in contrast, a Dart process running on a server
(or a process on a "client host" that stores data locally) would benefit
from avoiding those definitely-inconsistent states, even if it means that
it will "crash" a little earlier, and maybe even a little more often.

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984
--

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

'Erik Ernst' via Dart Misc

2015-10-05 15:34:01 UTC

C++ performance can be quite good (not counting problems that may arise
because of the GC-less memory management), and that's a good example of an
approach where dynamic checks are _never_ inserted even when you step
outside the scenarios foreseen by static typing.

In Dart you have the object-level soundness that Smalltalk pioneered in
1972 .. OK, some would say LISP in 1958..: You can never ever obtain a
pointer to an address unless that address is the beginning of an object in
your heap. This makes it possible to trust that when you call a method that
doesn't exist, you _will_ get an invocation of `noSuchMethod`, etc.

Being able to run faster because you have type annotations will work if you
have soundness, but you cannot rely on a vtable if you are calling `foo` on
an object o expected to be an instance of a class `A`, but it actually
turns out to be an instance of an unrelated class `B` (not a subclass, just
a "wrong" class, according to your expectations). So if you are not ready
to accept arbitrary C++ style low-level failures then you cannot use
vtables (so you won't get much of a performance benefit out of your types)
unless you will (1) check all the time (eating up that performance boost,
and maybe even more), or (2) accept the much more strict discipline
associated with traditional strict typing.

Post by Benjamin StrauÃ
Isn't performance also a point for 'always checked mode'? Bob mentioned in
another thread that it would help with optimizations.
I get the idea and benefits of optional typing. But Dart's unsoundness
always seemed a bit strange to me.

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed
properties of program executions. In this case it would be "in checked mode
you can trust all type annotations", which should be useful for programmers
to have in mind, even if they are not the kind of people who would want to
go and prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984
--

For other discussions, see https://groups.google.com/a/dartlang.org/
For HOWTO questions, visit http://stackoverflow.com/tags/dart
To file a bug report or feature request, go to
http://www.dartbug.com/new
To unsubscribe from this group and stop receiving emails from it, send

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

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

Gen

2015-10-05 15:04:09 UTC

I had already forgotten that "var" stands for "dynamic". The plugin for
intellij/webstorm offers (guessed) code completion based on type inference.
I do not understand the purpose of "checked mode" either.
How or when will "strong mode" be available for the IDE (eclipse, intellij)
?
Could "strong mode" allow the compilation of Dart programs into efficient
native executables that do not require the VM ?

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984

'Erik Ernst' via Dart Misc

2015-10-05 15:17:40 UTC

Honestly, I tend to think that checked mode is easy to motivate, but the
question is whether you want the performance benefits of omitting all those
checks so badly that you will accept that this reduces type annotations to
mere noise (except that you may have covered some execution scenarios in
testing, such that the invariants won't actually be violated, "typically").

Strong mode is currently an approach to compilation (so you won't need a
different platform to run it) where checks are required in more locations
and more strict requirements enforced. The hope is that this will enable
the compiler to omit the required checking code in a lot of cases, because
the check is statically known to always succeed.

But I shouldn't try to dive into the details, because I'm not working on
it; use https://github.com/dart-lang/dev_compiler/issues to check or report
any issues that you may have.

On top of that, I'd say that it is worthwhile to have a strictly enforced
heap discipline in the more dynamic Dart style where potentially lots of
type annotations are missing, and lots of data-flow constructs (assignment
etc) use implicit downcasts. The point is that you can actually trust the
type annotations that are present, and then you can study your dynamic code
and maybe annotate it if it tries to deliver a wrong-type object into a
typed context.

Post by Gen
I had already forgotten that "var" stands for "dynamic". The plugin for
intellij/webstorm offers (guessed) code completion based on type inference.
I do not understand the purpose of "checked mode" either.
How or when will "strong mode" be available for the IDE (eclipse,
intellij) ?
Could "strong mode" allow the compilation of Dart programs into efficient
native executables that do not require the VM ?

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984
--

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

'Vijay Menon' via Dart Misc

2015-10-05 15:44:51 UTC

This is a short term goal for us. We're actively working on the plumbing
to make this possible right now. There are still details to be worked out
on how to surface it.

Post by Gen
Could "strong mode" allow the compilation of Dart programs into efficient
native executables that do not require the VM ?

In theory it could help, but we're not actively working on this. Note:
strong mode would not obviate the need for garbage collection.

Post by Gen

Post by 'Erik Ernst' via Dart Misc
I think it's worthwhile to point out that the theory of Dart can be
that it is _capable_ of maintaining a sound heap. It relies on checked mode
execution and the absence of "reified dynamic objects" (such as instances
of `List<dynamic>`), and it requires a tiny twist on function type
subtyping (it should be changed to require covariant return types).

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode
checks are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984
--

2015-10-05 23:50:09 UTC

I think developers can _benefit_ from caring about guaranteed properties
of program executions. In this case it would be "in checked mode you can
trust all type annotations", which should be useful for programmers to have
in mind, even if they are not the kind of people who would want to go and
prove it.
With respect to the performance advantages: As soon as checked mode checks
are turned off it becomes (essentially) impossible to promise heap
soundness, so you couldn't generate code that relies on it. The obvious
alternative would be to eliminate as many checked mode checks as possible
(based on strictly guaranteed properties of the execution), and then
tolerate the runtime costs of the remaining checks in return for having
performance benefits based on heap soundness.
You might want to take a look at the work on strong mode (
https://github.com/dart-lang/dev_compiler/blob/master/STRONG_MODE.md)
where many of the same ideas have been applied.

Well aware of Strong Mode in ddc. The question is Strong Mode going to be
the basis of Dart's type system going forward - and will performance
optimizations result on mobile. (I'm only interested in Dart re Flutter).

Post by 'Erik Ernst' via Dart Misc
best regards,
--
Erik Ernst - Google Danmark ApS
Skt Petri Passage 5, 2 sal, 1165 KÃžbenhavn K, Denmark
CVR no. 28866984

'John Messerly' via Dart Misc

2015-10-05 15:55:45 UTC

For what it's worth, your timeline of these two is backwards:

* C# eventually acquires 'dynamic' under pressure from these langs.
* C# evolves in a functional direction via @headinthebox with Linq, var,
anon objects. Dev's seem to prefer it to 'dynamic'

LINQ was in C# 3.5, `dynamic` was in C# 4.

(source: I worked on `dynamic` and a large expansion of the Expression
Trees that had already shipped in LINQ 3.5.)

C# still takes inspiration to functional languages, if you look at their
notes (now on github
<https://github.com/dotnet/roslyn/issues?q=is%3Aopen+label%3A%22Design+Notes%22+label%3ALanguage-C%23>,
previously
on codeplex
<https://roslyn.codeplex.com/wikipage?title=CSharp%20Language%20Design%20Notes&referringTitle=Documentation>
).

2015-10-05 23:43:52 UTC

Post by 'John Messerly' via Dart Misc

Post by 'John Messerly' via Dart Misc
* C# eventually acquires 'dynamic' under pressure from these langs.
anon objects. Dev's seem to prefer it to 'dynamic'
LINQ was in C# 3.5, `dynamic` was in C# 4.

Right - got the timeline wrong. But I think the point stands that dev's
preferred the 'functional static' rather than the 'dynamic' approach to
development.

Post by 'John Messerly' via Dart Misc
(source: I worked on `dynamic` and a large expansion of the Expression
Trees that had already shipped in LINQ 3.5.)
C# still takes inspiration to functional languages, if you look at their
notes (now on github
<https://github.com/dotnet/roslyn/issues?q=is%3Aopen+label%3A%22Design+Notes%22+label%3ALanguage-C%23>, previously
on codeplex
<https://roslyn.codeplex.com/wikipage?title=CSharp%20Language%20Design%20Notes&referringTitle=Documentation>
).

I've argued here and on core-dev that the C# github design process would be
good for Dart 2.0 and that the direction of C# 7 looks very interesting:

https://groups.google.com/a/dartlang.org/d/msg/core-dev/53e5IubdfcQ/i76TUu7xrt0J

https://github.com/dotnet/roslyn/issues/2136

K.

'John Messerly' via Dart Misc

2015-10-06 00:15:10 UTC