N4JS: JavaScript language extension with sound type system

290 views
Skip to first unread message

Jens von Pilgrim

unread,
Apr 27, 2016, 9:46:21 AM4/27/16
to Strengthen JS
At Numberfour, we are writing a relatively large JavaScript framework (~2000 classifiers), and one of our main requirements was (and still is) to write maintainable code. Three years ago we evaluated TypeScript to be used for our frameworks. Unfortunately we found some, in this group probably well-known, TypeScript type-system problems. So we decided to create our own JavaScript language extension providing a sound type system (its compiler translates N4JS to V8-compatible JavaScript).

We made the language together with its IDE open-source a couple of weeks ago, and I thought that this approach may be interesting for some of you. 

Here are some links which may be interesting:
- N4JS project page: http://numberfour.github.io/n4js/
- Full language spec (PDF): https://goo.gl/2Lv2Te

We are very interested in your feedback (either here or, probably the better place, use the N4JS group: http://groups.google.com/group/n4js)!

Cheers,
Jens


Andreas Rossberg

unread,
Apr 27, 2016, 10:06:27 AM4/27/16
to Jens von Pilgrim, Strengthen JS
Thanks, this is very interesting! We'll have a look.

--
You received this message because you are subscribed to the Google Groups "Strengthen JS" group.
To unsubscribe from this group and stop receiving emails from it, send an email to strengthen-j...@googlegroups.com.
To post to this group, send email to streng...@googlegroups.com.
To view this discussion on the web, visit https://groups.google.com/d/msgid/strengthen-js/0007005e-0574-4572-9f78-5714eacac6ba%40googlegroups.com.
For more options, visit https://groups.google.com/d/optout.

Shelby Moore

unread,
Sep 11, 2016, 6:04:27 AM9/11/16
to Strengthen JS
I am interested to consider sound typing alternatives to TypeScript, because of for example decisions to add features such as the following to TypeScript which (unless I am mistaken in my analysis?) make me doubt their commitment/priorities to sound typing:


However, I will approach this from a reasonable degree of skepticism (in spite of your admirable open source attempt to improve on the typing of ECMAScript), simply because there appears to be considerable existing inertia and investment in TypeScript, so IMO any alternative has to be very compelling and/or be very (at least syntactically) compatible.

Below for some of specific observations thus far...

On Wednesday, April 27, 2016 at 9:46:21 PM UTC+8, Jens von Pilgrim wrote:
At Numberfour, we are writing a relatively large JavaScript framework (~2000 classifiers), and one of our main requirements was (and still is) to write maintainable code. Three years ago we evaluated TypeScript to be used for our frameworks. Unfortunately we found some, in this group probably well-known, TypeScript type-system problems. So we decided to create our own JavaScript language extension providing a sound type system (its compiler translates N4JS to V8-compatible JavaScript).

We made the language together with its IDE open-source a couple of weeks ago, and I thought that this approach may be interesting for some of you. 

Here are some links which may be interesting:
- N4JS project page: http://numberfour.github.io/n4js/

THE ANY TYPE

The TypeScript inference engine apparently avoids subsuming to type `any`:

https://www.typescriptlang.org/docs/handbook/type-inference.html

And TypeScript's implicit use of `any` can be turned off with the --noImplicitAny compiler flag, which will force explicit declarations of `any` (and ditto --strictNullChecks for not allowing implicit/implied `null | undefined` types):

https://www.typescriptlang.org/docs/handbook/compiler-options.html

So afaics in essence explicit declarations of `any` in TypeScript would be equivalents to explicitly declaring `+any` in N4JS, with all other instances of `any` type doing nothing in both projects so configured. Thus I don't see any compelling advantage of H4JS in terms of the `any` type.


THE COVARIANCE OF GENERICS

Correct typing of the covariance of class type parameters whether it be use-site (Java, N4JS) or declaration site (Scala, Ceylon, etc) will force subsumption (for covariant or supersumption for contravariant) to the best common super (for covariant, or sub for contravariant) type parameter for reading and for writing any sub (for covariant, or super for contravariant) type of that common type.

Any type parametrized type, e.g. `List<T>`, is indeed invariant which is easy to visualize if one assumes that only disjoint (not sub nor supertypes of each other) types will be employed for instance of `T`, because then obviously a type `List<A>` can never be assigned to a type of `List<B>` (nor `List<A | B>` to either `List<A>` or `List<B>`) when `A` and `B` are disjoint.

The point being that writing of disjoint types would not provide any advantage for N4JS over TypeScript, i.e. the use-site covariance typing would be inapplicable. This is an important observation for me, because it is my intention to introduce disjoint typeclasses as a superior paradigm to subclassing (not be confused with subtyping in expressions). I have come to view subclassing as an anti-pattern to be avoided and I am in the process of attempting to document my reasoning, as well attempt to provide a compelling case for typeclasses as a suitable model for the prototype chain of ECMAScript:

https://github.com/Microsoft/TypeScript/issues/10844


NOMINAL TYPING

Note that nominal typing can be achieved in TypeScript and there is issue #202 being considered for version 2.1 to make some syntactical sugar it.


VERBOSITY

I note that N4JS is favoring to trade verbosity for greater explicitness of protections, e.g. that all member properties are by default not `public`. I strongly dislike this choice. One thing I hate about Java is the verbosity. I similarly derided the explicit `abstract` keyword in TypeScript (because I can see with my eyes when I declared abstract by not providing an implementation and I will certainly get an error on instantiation if that was not my intent).


MISSING/INCOMPLETE FEATURES


The lack of complete support of generators and ES6 (2015) default function parameters might be a show stopper for me. TypeScript supports these already.


LACK OF TRANSPILING

N4JS apparently doesn't transpile to older versions of ECMAScript for compatibility with more platforms. I am not sure yet whether this would be a significant problem for my desired application.


ANNOTATIONS

I suppose the intent of not introducing any new keywords is for the syntax of N4JS to compatible to ECMAScript with the annotations stripped out? Is that going to be practical, i.e. I don't see how your `int` type or a typeclasses feature could work in that way. I am thinking annotations are just fuglier keywords.
I find it ironic that TypeScript claims to want to be erased as much as possible, yet I read it supports method overloading and the above states N4JS doesn't. I remember Martin Odersky remarking that function overloading would add many corner cases (at least for Scala). I am not knowledgeable about which is better, but I presume TypeScript has to create mangled overload method names in the emitted ECMAScript.

Jens von Pilgrim

unread,
Sep 15, 2016, 6:17:36 AM9/15/16
to Strengthen JS
Thank you very much for the feedback. Although I will give a short feedback here, I would suggest to use the N4JS group (https://groups.google.com/forum/#!forum/n4js) in the future for N4JS specific topics (since it is kind of off-topic here).

On Sunday, September 11, 2016 at 12:04:27 PM UTC+2, Shelby Moore wrote:
> I am interested to consider sound typing alternatives to TypeScript, because of for example decisions to add features such as the following to TypeScript which (unless I am mistaken in my analysis?) make me doubt their commitment/priorities to sound typing:


Hmm.. actually I would say that this is quite interesting. We also thought about adding features like that to N4JS. The whole topic is related to effect systems in general (including type guards and null analysis, which is not implemented in N4JS yet), and we have related features in our backlog as well ;-). I don't see a general problem with that. But I didn't look into the details.

> However, I will approach this from a reasonable degree of skepticism (in spite of your admirable open source attempt to improve on the typing of ECMAScript), simply because there appears to be considerable existing inertia and investment in TypeScript, so IMO any alternative has to be very compelling and/or be very (at least syntactically) compatible.

We try to make the syntax of N4JS syntactically compatible to TypeScript as far as possible. For example, we have updated our type expression syntax (e.g., definition of union or intersection types) to match TypeScript's syntax.

> THE ANY TYPE
> The TypeScript inference engine apparently avoids subsuming to type `any`:
> And TypeScript's implicit use of `any` can be turned off with the --noImplicitAny compiler flag, which will force explicit declarations of `any` (and ditto --strictNullChecks for not allowing implicit/implied `null | undefined` types):
[..]
> So afaics in essence explicit declarations of `any` in TypeScript would be equivalents to explicitly declaring `+any` in N4JS, with all other instances of `any` type doing nothing in both projects so configured. 

Yet, that's (partially) true. When we started with N4JS, these compiler flags were not available in TypeScript. I haven't checked the latest TypeScript version, but I remember that there are cases, in particular when using generics, in which any is inferred. I don't know exactly whether this cases are reported when the above mentioned compiler flags are set. In any case, there is always a big difference between "any+" in N4JS and "any" in TypeScript: any is a super type to anyother type in TypeScript, while "any+" is not.

The smarter the compiler will become, the less often any is inferred. This is true for both, N4JS and TypeScript. From that point of view, the problem is becoming less and less important or obvious. Still, it is a fundamental difference between N4JS and TypeScript. And I wouldn't say that one concept is better than the other -- they are just different.


> THE COVARIANCE OF GENERICS

Actually we have to update this paragraph on our webpage (I just didn't had time to do that). The thing is a little bit more substantial.
The basic concept in TypeScript leading to our observations is called "Function Parameter Bivariance" (see https://www.typescriptlang.org/docs/handbook/type-compatibility.html). From the TypeScript handbook:

"When comparing the types of function parameters, assignment succeeds if either the source parameter is assignable to the target parameter, or vice versa. This is unsound because a caller might end up being given a function that takes a more specialized type, but invokes the function with a less specialized type."

As the handbook already observes: this is UNSOUND! And they explain why they added it nonetheless:

"In practice, this sort of error is rare, and allowing this enables many common JavaScript patterns."

When I wrote the section on our website, I wasn't aware of this "bivariance". So I wrongly interpreted that as "assumed covariance".

Anyway, N4JS tries to provide a SOUND type system, this is why we cannot allow that in N4JS. The consequences of this bivariance, in particular in the context of method overriding, are quite surprising, at least for Java developers. And I wouldn't agree on their statement that "this sort of error is rare" -- it is the sort of error you immediately run into when you use generics. 

> Correct typing of the covariance of class type parameters whether it be use-site (Java, N4JS) or declaration site (Scala, Ceylon, etc) 

Note that we are now supporting user-site and definition-site typing in N4JS :-)

> will force subsumption (for covariant or supersumption for contravariant) to the best common super (for covariant, or sub for contravariant) type parameter for reading and for writing any sub (for covariant, or super for contravariant) type of that common type.

I'm not quite sure I understand that. "Best common super type" ("best"? I assume you mean "least", aka join) requires at least to types (for which the common super type is computed). In case of generics, often the lower or upper bound is used (i.e., inferred) in certain cases. But that's a different story. Also note that the concept of "join" is kind of trivial in languages providing union types: the join of two types A and B is simply the union type of A and B.

> Any type parametrized type, e.g. `List<T>`, is indeed invariant which is easy to visualize if one assumes that only disjoint (not sub nor supertypes of each other) types will be employed for instance of `T`, because then obviously a type `List<A>` can never be assigned to a type of `List<B>` (nor `List<A | B>` to either `List<A>` or `List<B>`) when `A` and `B` are disjoint.

Well, this is why we have the concept of wildcards with upper or lower bounds in Java (or N4JS); or definition site structural typing to enable sub-type relations between parameterized types. E.g.  for use site: A<:B => List<? extends A> <: List<? extends B>. Or, in case of definition site:  (List<out T> and A<:B) => List<A> <: List<B>


Sounds interesting, although I'm not quite sure how this is related to generics and the variance problem.


> NOMINAL TYPING
> Note that nominal typing can be achieved in TypeScript and there is issue #202 being considered for version 2.1 to make some syntactical sugar it.

Well... nominal typing IS structural typing -- with an additional relation explicitly declaring the subtype relation. Note that JavaScript itself is using nominal typing in case of the "instanceof" operator (in which the prototype/constructor chain defines the relation). But it would be interesting to have nominal typing in TypeScript as well.


> VERBOSITY
> I note that N4JS is favoring to trade verbosity for greater explicitness of protections, e.g. that all member properties are by default not `public`.

We simply followed the Java way :-) 

>I strongly dislike this choice. One thing I hate about Java is the verbosity. I similarly derided the explicit `abstract` keyword in TypeScript (because I can see with my eyes when I declared abstract by not providing an implementation and I will certainly get an error on instantiation if that was not my intent).

Well, there is no right or wrong. One of our main goals was maintainability. And for that, verbosity is often quite helpful.


> MISSING/INCOMPLETE FEATURES
> The lack of complete support of generators and ES6 (2015) default function parameters might be a show stopper for me. TypeScript supports these already.

We definitely want to add support, it's only a question of resources (so feel free to contribute :-)). Our parser already supports generators of course. And with the built-in support for async/await, we hope that you do not need generators that urgently. But it is definitely on our list of things to do!

> LACK OF TRANSPILING
> N4JS apparently doesn't transpile to older versions of ECMAScript for compatibility with more platforms. I am not sure yet whether this would be a significant problem for my desired application.

Again: lack of resources. Out transpiler is quite modular, so it should be possible to add support for elder platforms. But since the latest versions of browsers nowadays support ES2015 (even node.js thanks to V8), we hope that this problem will become less and less important over time.


> ANNOTATIONS

> I suppose the intent of not introducing any new keywords is for the syntax of N4JS to compatible to ECMAScript with the annotations stripped out?

Well, there is a ES proposal for "decorators", which is more or less "user defined annotations". At the moment, we do not support that, but our (usage) syntax is already quite similar. With decorators, we can "move" some functionality currently hard-coded in the compiler to N4JS libraries. Also, we used annotations when there were similar annotations in Java (e.g. @Override).

> Is that going to be practical, i.e. I don't see how your `int` type or a typeclasses feature could work in that way. I am thinking annotations are just fuglier keywords.

Type expressions have to be removed by the compiler anyway ;-)
 
> I find it ironic that TypeScript claims to want to be erased as much as possible, yet I read it supports method overloading and the above states N4JS doesn't. I remember Martin Odersky remarking that function overloading would add many corner cases (at least for Scala). I am not knowledgeable about which is better, but I presume TypeScript has to create mangled overload method names in the emitted ECMAScript.

Overloading is a very complicated thing for compilers (because you need to know the type before binding a reference to a declaration, and often you need the binding in order to infer the types correctly -- so it is a hen-egg-problem). And JavaScript does not support overloading (well, simply because there are no types).

In TypeScript, the "overloading" methods are only declarations (i.e., without a body), and you always need to define one method which parameters are compatible with the parameters defined in the overloading declarations. I think it is a quite nice concept. Still, we have not added overloading due to the complexity introduced by it.

Regards,
Jens
Reply all
Reply to author
Forward
0 new messages