Dart 2.0 and Types

[kc]

A potted history of types in the last 15 years:

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.

C# evolves in a functional direction via @headinthebox with Linq, var, 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.

[Erik Ernst]

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.

--
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 email to misc+uns...@dartlang.org.

--

Erik Ernst  -  Google Danmark ApS

Skt Petri Passage 5, 2 sal, 1165 København K, Denmark

CVR no. 28866984

[kc]

On Monday, October 5, 2015 at 2:01:06 PM UTC+1, Erik Ernst wrote:

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.

[Erik Ernst]

On Mon, Oct 5, 2015 at 3:14 PM, kc <kevin...@gmail.com> wrote:

On Monday, October 5, 2015 at 2:01:06 PM UTC+1, Erik Ernst wrote:

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?

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,

[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 current semantics (no type overloading, etc.):

typed code -> has to be sound

untyped code/type dynamic -> works like javascript

[Erik Ernst]

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.

--
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 email to misc+uns...@dartlang.org.

[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 ?

[Erik Ernst]

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.

--
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 email to misc+uns...@dartlang.org.

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

[Erik Ernst]

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.

[Vijay Menon]

On Mon, Oct 5, 2015 at 8:04 AM, Gen <gp78...@gmail.com> wrote:

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) ?

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.

 

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. 

Am Montag, 5. Oktober 2015 16:32:53 UTC+2 schrieb 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 current semantics (no type overloading, etc.):

typed code -> has to be sound

untyped code/type dynamic -> works like javascript

Am Montag, 5. Oktober 2015 15:33:27 UTC+2 schrieb Erik Ernst:

On Mon, Oct 5, 2015 at 3:14 PM, kc <kevin...@gmail.com> wrote:

On Monday, October 5, 2015 at 2:01:06 PM UTC+1, Erik Ernst wrote:

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?

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

[John Messerly]

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, previously on codeplex).

--

[kc]

On Monday, October 5, 2015 at 4:56:30 PM UTC+1, John Messerly wrote:

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.

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.

 

(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, previously on codeplex).

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.

[kc]

Well aware of Strong Mode in ddc. The question is will 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).

[John Messerly]

On Mon, Oct 5, 2015 at 4:43 PM, kc <kevin...@gmail.com> wrote:

On Monday, October 5, 2015 at 4:56:30 PM UTC+1, John Messerly wrote:

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.

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.

Good point. Yeah, that certainly seems to have been the C# experience.