Counter proposal: Is a strong type system really impossible for JavaScript?

[theScottyJam]

In the frequently asked questions of this proposal, it stated that EcmaScript generally operates by favoring "local, sound checks", and in contrast, TypeScript gained its success without trying to make any sound checks in their type system, therefore, a native JavaScript type system should not be sound, and should not be in the control of EcmaScript (EcmaScript carves out the syntax space, but lets everyone else deal with the type-checking).

I think this logic is making a lot of jumps. The part I want to focus on is the fact that TypeScript was very limited in what it could do when it was created, making it much harder for it to provide a performant, sound type system. I feel this proposal would be incomplete, unless we also spend time to actually see what a sound type-system would look like if we decide to go that route.

So, I decided to start up a conversation related to this topic. I want to find out what the pros and cons of a sound type system would be, before we burry the idea and proceed with this current proposal. The main conversation is intended to happen in the TC39 forms over here, or in a strawman proposal repo I threw up over here.

This thread is mainly intended to let others know about this angle that I feel is an important angle to explore, and not to just "brush away".

[dfabulich]

I agree that this FAQ answer should be updated, but, yes, it's really impossible, because of the structure of TC39, which requires (approximately) 100% consensus to change the language.

The rest of the FAQ answer explains the real problem:

In contrast, trying to add a full type system to JavaScript would be an enormous multi-year effort that would likely never reach consensus. This proposal recognizes that fact, and also recognizes that the community has evolved type systems that it is already happy with.

Why wouldn't TC39 reach consensus? Another FAQ answer explains:

How could runtime-checked types be added in future? It seems unlikely that JavaScript would adopt a pervasive runtime-checked type system due to the runtime performance overhead that it would bring. While it's possible that there may have been room for improvement, past efforts such as TS* (Swamy et al) have shown that runtime type-checking based on annotations adds a non-negligible slowdown. That is one reason why this proposal endorses purely static types.

It's unlikely that TC39 will agree to any runtime-checked type system at all, for performance reasons. But let's say they did. Would they then agree to TS-like best-effort checks, or to a "strong" type system like Hegel? The developer ecosystem has overwhelmingly chosen TypeScript over Hegel, but there's no doubt that strong type systems have appealing features.

What is obviously impossible is convincing every TC39 member that JS should standardize on a Hegel-like type system that is checked at runtime. The performance implications alone make it a complete non-starter. And the developer ecosystem has strongly spoken in favor of best-effort systems like TS and Flow, so that's another insurmountable objection.

As long as anyone on TC39 objects to a strong type system checked at runtime, the whole project fails. It is therefore impossible.

[guitarino]

@dfabulich

As long as anyone on TC39 objects to a strong type system checked at runtime, the whole project fails. It is therefore impossible.

How confident are you that there will be objections that cannot ever be addressed? What's the main reason for having the same amount of confidence?

[dfabulich]

TC39 is a notoriously challenging forum within which to reach consensus, even for "slam dunk" proposals like decorators (which only just last week turned Stage 3 after a decade of "bikeshedding"). This isn't because TC39 members are especially difficult or cantankerous, but because there are a bunch of members with different points of view, and advancing to the next stage requires perfect consensus.

Decreasing performance at runtime is, itself, a showstopper. If anyone on TC39 cares about runtime performance more than language purity, (and, I assure you, more than one of them does—much more), then the task of implementing a strong type system at runtime is impossible. (Did you click that link to TS* (Swamy et al) provided in the FAQ?)

I don't think I'm being too bold when I say that it is impossible to implement a non-trivial type system that runs on slow mobile browsers, at runtime, but doesn't impact runtime performance!

As for "strong" type systems, much depends on what you mean by "strong." (If you think TypeScript and Flow are "strong," then, uh, sure, this proposal will allow you to implement most of TypeScript and Flow. But it is certainly reasonable to want something stronger than that.)

@theScottyJam used the term in contrast with the terms used in the FAQ:

TC39 has a tradition of programming language design which favors local, sound checks. By contrast, TypeScript's model -- which has been highly successful for JS developers -- is around non-local, best-effort checks. TypeScript-style systems are expensive to check at application startup, and would be redundant every time you run your JavaScript applications.

So when @theScottyJam asks about a "strong" type system, I think he's asking why we should settle for TypeScript's "non-local best-effort" approach, and specifically whether we should prefer non-local sound checks, like Hegel.

(A "sound" type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is String, at runtime you are guaranteed to only get a string when you evaluate it. Hegel makes soundness guarantees; TypeScript does not.)

There is obviously no industry consensus that programming languages with non-local sound type systems are better than "best-effort" type systems. Literally none of the top 10 languages on any major survey use non-local sound typing; they all make it possible to have type errors at runtime. (Github Octoverse, Stack Overflow, TIOBE Index)

Languages that guarantee soundness put a lot of counterintuitive constraints on language designers and the users of sound languages. Sound languages are especially difficult for newbies to learn, especially as a first programming language. (IMO, this is a major reason why none of the most popular programming languages ensure non-local soundness.)

So, now imagine trying to get perfect consensus from every TC39 member that we should convert JavaScript, a dynamically typed language, into a language with a sound type system, like Hegel.

Surely one of them will say "non-local soundness is bad for the web; we should go with best-effort typing, which has clearly won over developers' hearts and minds, in both TypeScript and Flow."

Indeed, I predict that at least one of them will say, "on the contrary, if we ship a type system in browsers, we should accept nothing less than global soundness."

The only way to cut that knot is to allow Hegel and TypeScript to co-exist in the grammar, which is what this proposal will do.

[ljharb]

I’m not sure that’s an accurate characterization of TC39, and while i like decorators, in no way is that a “slam dunk” proposal.

Idiomatic JS already has runtime type checks, and is perfectly performant enough. I don’t see any inherent inability to do a runtime type system based on performance claims, given that the alternative (actual JS doing the checks) already exists.

[theScottyJam]

Indeed, I predict that at least one of them will say, "on the contrary, if we ship a type system in browsers, we should accept nothing less than global soundness."

And with this proposal, I predict a delegate would say "on the contrary, if we ship a type system in browsers, we should accept nothing less than a single, unified type system". In the end, there's only one path forwards when it comes to bringing a type-system into JavaScript. Should we bring in a types-as-comments proposal that has no runtime semantics, and no single official type system? There's a lot of downsides to this approach. Sure, it's what we have today, but that doesn't mean it's the best option. Or, instead of carving out syntax space to let anyone make a type-system, perhaps we should standardize on a single type-system, but still treat types as comments. Or, maybe we can mix in some runtime behaviors to make something a little more sound (What I'm proposing here). Each of these paths are mutually exclusive, we can only have one, so which should it be?

The overall path to take is something the committee members will need to decide on, and to come to consensus on. In order for this to happen, we ought to explore what the different paths actually look like, which is why I'm trying to explore this path (how can we say one path is better than the others if we don't know what the other paths look like?). I believe the largest hurdle for any of these paths is achieving consensus on the path, after that, the rest of the details are relatively smaller to work out (the details can still be large, but not as large as picking an overall path). And yes, I agree that some paths will require a much larger proposal than other paths. What I'm proposing would be a huge change to the language, and could take many years to come through. For what I know, it could even take 20 years to work out all of the details of a proposal this large, I accept that. (For this reason, I think it would be good to split it up into smaller proposals that advance through the proposal pipeline together, but still, it will be a large task). Still, I'd rather have a high quality, single official type-system in JavaScript in 20 years, then basically what we have today, but without a build process in a few years.

You say that a proposal like this is too big to go through the TC39 proposal process, I say, lets give it a chance, to see if this is actually true. Lets let the committee work on something a little larger, and see if they can work out the details of a fairly large change. If the committee can't provide what's best for the language because the changes required is too big for them to discuss, then perhaps something needs to be changed in the proposal process in order to allow them to deliver what's best for the community.

(A "sound" type system means you can never get into a state where an expression evaluates to a value that doesn’t match the expression’s static type. For example, if an expression’s static type is String, at runtime you are guaranteed to only get a string when you evaluate it. Hegel makes soundness guarantees; TypeScript does not.)

Yeah, so what I meant by "sound" is that, if you say a value is going to be a "string", then that's what you're going to get. There's no way to get around the type-checker and get something else into the function. This sort of sounds like what you're explaining here as well.

However, I don't intend "sound" to mean "no runtime type errors". I'm ok providing, for example, x as y syntax that lets you narrow the type of a value. At runtime, such an expression would run assertions to make sure this narrowing is really allowed, and if its not, a type-error will be thrown. Sorry if this isn't what "sound" means, I can start using a different word if you want to suggest one.

Decreasing performance at runtime is, itself, a showstopper.

In the proposal I linked to, my primary objective is to make it so you can have a sound type system, without any major performance penalties. Declaring the types of function parameters will inevitably require assertions to be made (though, it's possible engines could optimize out some of those assertions). The goal is to make these assertions be quick, O(1) assertions. If the performance cost for assertions like this is unacceptable for committee members, then yes, this proposal will be dead.

Sometimes, O(1) assertions isn't possible to achieve. For example, you might declare a public-facing function that takes an options object, and the only way to validate that the passed-in options object is of a valid shape, is to look over all of the properties in the options object and ensure is conforms to a provided interface. I'll call this an O(n) assertion. In the proposal, if you want to do a more expensive assertion like this, you have to explicitly flag that that's you intention (by using a !). In the end, this sort of assertion is a good thing for public-facing functions, it's good to validate, at runtime that users are passing in a valid options object and not garbage data (and it's good for the end-user to get a nice error about how they passed in a bad options object, instead of a cryptic error coming deep within your library about trying to read property "whatever" off of an undefined value). This is the type of assertions that people should already be writting today, using for loops and what-not, the type syntax is simply making it easier to write this sort of assertion.

So, now imagine trying to get perfect consensus from every TC39 member that we should convert JavaScript, a dynamically typed language, into a language with a sound type system, like Hegel.

Note that what I'm proposing is not Hegel. Hegel can't do the kinds of things I put in the proposal repo, it has limitations that we don't have when making proposals.

[benjamingr]

Idiomatic JS already has runtime type checks, and is perfectly performant enough. I don’t see any inherent inability to do a runtime type system based on performance claims, given that the alternative (actual JS doing the checks) already exists.

Idiomatic JS only has trivial type checks (like the type of primitives or branding of objects). The impossible part isn't performing those checks but performing the significantly more expensive ones with generics, mapped types or inferred types.

[benjamingr]

Sometimes, O(1) assertions isn't possible to achieve. For example, you might declare a public-facing function that takes an options object, and the only way to validate that the passed-in options object is of a valid shape, is to look over all of the properties in the options object and ensure is conforms to a provided interface

I don't think that'd work? It means that some type annotations are validated and some are ignored?

[theScottyJam]

I don't think that'd work? It means that some type annotations are validated and some are ignored?

You'll need to take a peek at the proposal repo when you have time. It's a long read - sorry about that. But, it goes into detail describing a potential tagging system we could add. The idea is, if an object conforms to a particular interface, you set a tag on that object. Once the tag is in place, you cas pass the object around to any function that expects a value that conforms to that interface. Such checks would be simple O(1) checks. If you ever mutate the object in a way that causes it to not conform to the interface anymore, it will loose its tag.

Idiomatic JS only has trivial type checks (like the type of primitives or branding of objects). The impossible part isn't performing those checks but performing the significantly more expensive ones with generics, mapped types or inferred types.

Surely, it's possible to do regular JavaScript type-checks for these sorts of things as well. If we think about it, when you use any built-in function, you're always going to get a well-thought-out deterministic response, no matter what value you provided to the function. Perhaps you were supposed to provide a mapped object type to the built-in function (like with the URLSearchParam class's constructor), but you can still give it a bad value, and it'll run some assertions and give you a nice error message if you fail to give it an expected value.

A public-facing API should ideally be designed to always have a deterministic response for each type of input value you could give it, and this means it should properly throw errors if you give it a bad value, no matter how complex of a type you were expecting from the end-user.

The proposal I linked to lets you do these sorts of assertions with your public-facing API. It's with these public functions where these assertions might be a little more expensive, and might be O(n) instead of O(1), but that's permissible, considering we want these assertions to be in place, whether or not we're using a type system. What is not permissible is if every single function behind the scenes needed to do the O(n) check over and over again. It's the behind-the-scenes functions that need to have O(1) assertions, and its for this reason the objects get tagged, so that future behind-the-scenes checks become more performant.

[dfabulich]

Yeah, so what I meant by "sound" is that, if you say a value is going to be a "string", then that's what you're going to get. There's no way to get around the type-checker and get something else into the function. This sort of sounds like what you're explaining here as well.

However, I don't intend "sound" to mean "no runtime type errors". I'm ok providing, for example, x as y syntax that lets you narrow the type of a value. At runtime, such an expression would run assertions to make sure this narrowing is really allowed, and if its not, a type-error will be thrown. Sorry if this isn't what "sound" means, I can start using a different word if you want to suggest one.

If you're prepared to allow runtime type errors, the word you're looking for is not "sound." The word you're looking for is "best-effort."

I've read your repository, and I think you're taking the first step toward re-inventing TypeScript/Flow, because you haven't finished thinking through what your goals are. What are you trying to prove during ahead-of-time static analysis? (Why not everything, like Hegel? Why not nothing? If it's something in the middle, that's "best-effort." If you're doing "best-effort," why verify those things and not others?) What are you attempting to verify at runtime? (Why not everything? Why not nothing? Why some things and not others?) Is your goal to implement something "strong," "strict," or "sound"? (Your proposal repo is called "strict JS types" but your high-level objective is to have "strong" types, and you've expressed uncertainty here in the thread about whether this means the same thing as "sound.")

For what I know, it could even take 20 years to work out all of the details of a proposal this large, I accept that.

I say, lets give it a chance

It's funny that you should say "20 years." Here's a draft from 2000, the earliest such draft I'm aware of, that attempted to specify types in JavaScript. https://www-archive.mozilla.org/js/language/js20-2000-07/libraries/types.html

Some of the folks working on this repo have been working on types in JavaScript for more than a decade already.

This repo's FAQ has a "Relevant proposals and discussions in TC39" section, which links to this 2017 proposal linking to other prior discussions:

• 2002 Javascript 2.0: Evolving a Language for Evolving Systems
• 2006 Type parameters, Type System and Structural Types and typing of initializers
• 2011 Dependent Types for Javascript (pdf)
• 2011 Guards and Trademarks
• 2014 TC39 Discussion on Types: adding syntax without semantics.
• 2015 ES8 gradual typing and part2 and ecmascript-types.

We have "given it a chance" already. Don't ask anyone to "just give it a chance" for another 20 years, and when they fail in 2042, have a bright-eyed engineer come in and say, "Come on, it's gotta be possible; just give me a chance!"

[theScottyJam]

I've read your repository, and I think you're taking the first step toward re-inventing TypeScript/Flow, because you haven't finished thinking through what your goals are. What are you trying to prove during ahead-of-time static analysis? (Why not everything, like Hegel? Why not nothing? If it's something in the middle, that's "best-effort." If you're doing "best-effort," why verify those things and not others?) What are you attempting to verify at runtime? (Why not everything? Why not nothing? Why some things and not others?) Is your goal to implement something "strong," "strict," or "sound"? (Your proposal repo is called "strict JS types" but your high-level objective is to have "strong" types, and you've expressed uncertainty here in the thread about whether this means the same thing as "sound.")

Ok, how about we use the phrase "the types do not lie". If you declare that a variable has a string type, then it has a string type, and nothing you can do at runtime will change that. TypeScript does not provide this guarantee, In TypeScript, I can alway get around the type declarations at runtime (just mask a value with an any type before passing it into a function that expects a specific type). This is the guarantee I'm wanting to provide for JavaScript's native type system, and I feel like what I proposed offers this. Do you disagree? Can you find a way to get around the type-safety it offers? (Actually, I do know of one way to get around the type-safety, I hope to update the README soon with a fix for this).

And, please note that I'm not necessarily saying that we should or should not go this route. I just want to explore it a bit and figure out the pros and cons of such a route, to see if it's a viable route or not.

Your proposal repo is called "strict JS types" but your high-level objective is to have "strong" types, and you've expressed uncertainty here in the thread about whether this means the same thing as "sound."

Well, sorry. When writing up the actual proposal, I did look up the meaning of "strong types" to make sure I had that right before I started using the term. And, what I found is that there's not really a consensus on what the term "strong types" means, so I didn't worry too much about how I used it. I did not look up the term sound before I commented on this repository, I should have, but I didn't, and as you said I've been using it wrong.

It's funny that you should say "20 years." Here's a draft from 2000, the earliest such draft I'm aware of, that attempted to specify types in JavaScript. https://www-archive.mozilla.org/js/language/js20-2000-07/libraries/types.html [...] This repo's FAQ has a "Relevant proposals and discussions in TC39" section, which links to this 2017 proposal linking to other prior discussions

Thanks for doing that research, I'll read over those links to see what these older proposals and discussions had to offer. Perhaps I can find ways to improve the proposal I'm presenting, using the past conversations on this topic.

We have "given it a chance" already. Don't ask anyone to "just give it a chance" for another 20 years, and when they fail in 2042, have a bright-eyed engineer come in and say, "Come on, it's gotta be possible; just give me a chance!"

Proposals come and go all of the time. Many die out simply because the champions stop trying so hard to peruse them, or in some cases, the champion simply leaves the committee and no one picks up where they left off. Most of the links you shared were links to general discussion by the community, some of them were proposals, but all of the proposals are over 10 years old, and it's hard to gather much information about them. I can't tell how hard the champions tried to pursue the proposal, or how much pushback those proposals had. As far as I can tell, there aren't any meeting notes available that showed us the discussions around those proposals. The "type parameters" proposal had a link to some discussion, which seemed to be fairly positive in nature, so I don't know what happened to it.

A couple of those links, including your "20 year old" one was related to JavaScript 2.0, an overbloated standard that failed to achieve consensus - even if the JavaScript 2.0 standard had types-as-comments embedded in it instead of the type system they were running with, I'm sure it still would have failed to achieve consensus, simply because the problem wasn't in the proposed standard's content, but in the fact that the "champions" didn't do a great job at collaborating with others and making sure it met everyone's needs (At least, this is how I'm understanding the history when I read up on it). The TC39 proposal process has improved a lot since then, and I feel like they do a much better job at trying to consider everyone's needs.

Most of those actual proposals you linked to existed even before EcmaScript 3 came out, which was during the time when the committee was really struggling to collaborate. Many ideas failed to come to fruition during that time, but ended up appearing later.

From what I can tell, there hasn't been any attempts to get type-safety into JavaScript in the past ten years, this proposal by Microsoft being the first in a long time. While this proposal is discussed and worked with, I see no problem in trying to dig up some of the other possible avenues we could take if we want to bring type-safety into JavaScript. If these other avenues don't work, we can close the proposal and document why this path should not be taken.

So, no, I'm not asking that we put this proposal on hold while we "give it yet another chance" for 20 years. I'm asking that we peer down in a general direction to see if we want to venture that way or not. 20 years was, I'm sure, an exaggeration of how long it will take to figure out each minor detail relating to a full type system, it is not a measurement of time for how long it should take to decide the general direction we want to travel when it comes to type systems in JavaScript, that should be much, much shorter.

[dfabulich]

From what I can tell, there hasn't been any attempts to get type-safety into JavaScript in the past ten years

But… I just pasted you these links!

• 2014 TC39 Discussion on Types: adding syntax without semantics.
• 2015 ES8 gradual typing and part2 and ecmascript-types.

And are you forgetting that those links came from the 2017 proposal? Which was followed up by a 2018 proposal? (These are both mentioned in the "prior art" section of the readme of this repository.)

And let's not forget Google's "Strong Mode" experiment, which was intended to use types to improve site performance. Google canceled the experiment in failure in 2016. "In the end we had to give up on this one."

FWIW, I've filed a PR to update the README to include more of those links directly.

20 years was, I'm sure, an exaggeration of how long it will take to figure out each minor detail relating to a full type system, it is not a measurement of time for how long it should take to decide the general direction we want to travel when it comes to type systems in JavaScript, that should be much, much shorter.

And yet TC39 hasn't "decided on the general direction" in 20 years so far, including 14 years since the failed ES4 proposal, which also included a type system.

I'm asking that we peer down in a general direction to see if we want to venture that way or not.

And the links I've provided are proof that we have already peered down several general directions, and none of them have achieved perfect consensus at TC39.

Today's proposal incorporates the history of those failed attempts, and builds upon them, as well as the prior art of TypeScript and Flow as successful projects.

Ok, how about we use the phrase "the types do not lie".

Instead of inventing terminology, consider using industry-standard terms for type safety.

You define "the types do not lie" like this:

If you declare that a variable has a string type, then it has a string type, and nothing you can do at runtime will change that.

But you've also said this:

However, I don't intend "sound" ["the types do not lie"] to mean "no runtime type errors". I'm ok providing, for example, x as y syntax that lets you narrow the type of a value. At runtime, such an expression would run assertions to make sure this narrowing is really allowed, and if its not, a type-error will be thrown.

You're contradicting yourself here. You just don't know what you're trying to achieve, say nothing of what's possible, and as a result, you're asking us to put this proposal on hold until you, personally, have thought more about type systems.

I can't really expect you to trust me on this, but, seriously, trust me on this. When you finish learning how to build your own type system, and when you finish exploring what TC39 has already rejected and will refuse to accept, you will eventually conclude that a proposal like the one offered in this repo is the only way forward, and that this is actually a good thing.

As you learn more about type systems and TC39, you'll learn facts like these:

• Detecting type errors ahead of time is the whole point; waiting to throw type errors at runtime was exactly the problem we were trying to solve in the first place.
• Detecting non-local type errors ahead of time takes CPU time; it's silly to do it on a slow mobile phone, when the developer could do just it once before deploying.
• If a type system is both sound (meaning that it rejects all incorrect programs) and decidable (meaning that it is possible to write an algorithm that determines whether a program is well-typed), then it must be incomplete (meaning there are correct programs, which are also rejected, even though they do not encounter runtime errors).
• Therefore, some developers will prefer stricter type systems that reject lots of useful programs, because it guarantees their safety, while other developers will prefer looser type systems that run somewhat higher risk.
• Therefore, TC39 will not agree to standardize on a very strict static type system that rejects lots of useful programs, nor to standardize on a loose type system that runs higher risk, because perfect consensus cannot be achieved in either case.
• Since different developers have different needs, there are significant advantages to allowing developers to choose their own type system, to "plug in" their own type system to fit their needs.
• TC39 really won't accept anything else. (And perhaps not even this; who knows!)

[ljharb]

@dfabulich i don’t believe either of the 2017 and 2018 proposals you mentioned were actually presented at TC39; i can’t find any mention of them in the notes.

[theScottyJam]

For your 2015 links, those proposals/discussions were all by the same person, who from what I can tell is just a community member like me. That proposal never got championed. So, that too is simply community discussion, just like what's going on here. Your 2014 link seems to be about reserving a syntax space for type systems without adding any functionality, to make sure EcmaScript never adds syntax that overlaps with TypeScript or Flow syntax. From what I can tell, this isn't an ask for a type-system in JavaScript, it's asking that JavaScript doesn't trample on TypeScript syntax with new features.

EDIT: I just had the chance to look over the strong mode. It was certainly interesting and informative. I'll point out that, in that article they mentioned that they hadn't given up hope on adding types to JavaScript, just that they don't believe their particular approach was the correct way to go. From the "what didn't work well" section, a key take-away I got was the troubles they had with inheritance and mutability. I still haven't had time to update the proposal repo with some fixes, but I'll be sure to keep in mind to explicitly state how it'll handle the fact that users can mutate the base class when I do get around to updating it, I believe there's a safe way to handle it, but it may be a little annoying.

You're contradicting yourself here. You just don't know what you're trying to achieve, say nothing of what's possible, and as a result, you're asking us to put this proposal on hold until you, personally, have thorught more about type systems.

Please don't take this attempt to explore as a threat against this proposal. I'm not asking that we put this proposal on hold while I personally dallop around in type safey. I just wanted to discuss a different angle I found interesting. And, please note that I myself am not convinced of this particular angle I'm trying to discuss here (yet) - it's certainly going to have some issues - I'm doing what I can to work through the different issues and solve what I can, but its very possible that some issues are just going to be too big.

I also don't feel like this is contradictory. If I have a function definition, like function fn(x: string) { ... }, then within the function body, the type of x should only ever be a string. If it can be anything else, then the types have lied to me. If I have x as string, then you should be able to know with certainty that the value of x within the code following the assertion will always be a string. In both scenarios, runtime assertions are being used to ensure that when we say a type is something, it's really going to be something, that way we never end up with a funny Can not read property whatever of undefined error, instead, if we made a bad assumption, we're going to get a much nicer type error explaining what went wrong.

So, I'm not trying to make a type-system that never throws an error, I don't think that would be a good fit for JavaScript as it's not possible to do that while interopting with any existing, untyped code. I'm trying to see if it's possible to make a type system with honest types. What I'm describing here is to try and bump the safety-level of our type system up to that of Java or C++, which function in a similar way - if you declare a function in Java takes a string, then it's impossible to hand it a number, and if you coerce a type to another type, runtime checks will happen to ensure the coercion was valid, and after the coercion is over, you can be sure that the type is what you feel it is.

If you don't feel like the specific objective of having honest types is important, that's fine. You don't have to like it. But rebranding the objective as "best-effort" (what TypeScript already is), or never-throw-a-type-error is a fundamental change in what I'm trying to accomplish. I don't feel never-throw-a-type-error is a good fit, and a single, standard best-effort type-system is what I would want to explore next if this proposal has too many holes.

I can't really expect you to trust me on this, but, seriously, trust me on this. When you finish learning how to build your own type system, and when you finish exploring what TC39 has already rejected and will refuse to accept, you will eventually conclude that a proposal like the one offered in this repo is the only way forward, and that this is actually a good thing.

I have built a type system before. I love exploring language development, and have been toying around with my own general purpose "toy" language that has a full type system with generics, unknown/never types, type inference, etc, etc. Type systems are very hard to build, as I learned.

In regard to some of the points you listed:

• "Detecting type errors ahead of time is the whole point; waiting to throw type errors at runtime was exactly the problem we were trying to solve in the first place". -- Though, as you said, and I agree, a 100% sound type system isn't a good fit for JavaScript. So, a valid secondary point would be throwing nice error messages when a type error does happen. I mean, can you imagine what would happen if Java didn't do runtime assertions with their type coercion operators? You would get the most cryptic, hard-to-debug error messages when the type coersion fails, when the engine crashes while trying to use a value of the wrong type (Granted, JavaScript is not Java, so this is a bit of an invalid analogy). In general, it's good to have assertions in a program to make sure it's still in the state you expected it to be in, so you can catch odd errors earlier, type errors ought to be included in these assertions. What's even worse is when you don't catch these errors at all, and end up with odd things you might not spot, like undefined showing up in your UI. You don't have to feel like this secondary point is a big deal, I do, and that's why I'm going after it.
• "Therefore, some developers will prefer stricter type systems that reject lots of useful programs, because it guarantees their safety, while other developers will prefer looser type systems that run somewhat higher risk". -- And some developers, like myself, just want a single, standard type system no matter how strict or loose it is. I'm advocating for a stricter type system in this thread, but if it has too many holes, the next thing I'll advocate for carving out a types-as-comments syntax for a single, standard type-engine, instead of trying to do it for a bunch of different, community-provided ones.
• "Since different developers have different needs, there are significant advantages to allowing developers to choose their own type system" -- No one's stopping the community from making their own type systems for JavaScript that's different from whatever the standard one is. We can bless a standard type system without throwing out all other existing type systems.

Again, please don't try and take this exploration as some major time-consuming threat to Microsoft's proposal. That's not the intention at all. I merely want to spark conversation around the idea and see where it leads. And if it leads somewhere interesting, awesome! And if some committee members like the idea and want to run with it, that's cool too (however, my intentions right now is to just discuss it, not to solicit for a champion). if things turn sour for this proposal, that's fine as well. At least we had a discussion around it, which can help us feel better when we decide to not go that route. You obviously have different priorities for a JavaScript type system standard than I do, and that's perfectly fine - I'm not going to try and convince you that the objectives I'm persuing here are objectively better, there's trade-offs, and you've listed some valid ones.

[theScottyJam]

I've been working on trying to iron out this issue:

interface User {
  name :: string
}

function fn(obj :: User) {
  doThing()
  return user.name
}

When you get to user.name, you don't have any guarantee that the name property is still present on user. doThing() could technically be calling a stored callback that was supplied by the end-user, and that callback could be mutating the user object in unexpected ways. There's a handful of other variants to this issue of mutable data types, all of them pointing to the fact that providing type safety for mutable data types is a thorny issue.

I did come up with a set of interesting features that could be used to protect against this sort of thing, but I ultimately decided that these features were adding a fair amount of complexity and magic to the proposal, and putting a fair amount of work on the end-user to constantly validate the shape of their data, when in the end, this sort of thing doesn't usually matter (because, for example, it's much more likely that doThing() does not call a user-supplied callback, and you as the code author know this).

So, I'm thinking I'm going to scale back on the strictness level of this proposal. In general, I think it would be better for this proposal if, instead of having a single concrete objective of "I want honest types", to instead simply say "I want a standard type system, that balances type-safety with ease-of-use". The proposal will guarantee type safety in certain scenarios that will be documented. In the places where type-safety is not guaranteed, it's up to you to ensure that everything works properly.

For example, in the current proposal, any time you have a type assertion (via as, or ::), it's guaranteed that right after that assertion, the value conforms to the type. However, as soon as you start executing other code, you loose any guarantees related to mutable object types, and it's up to you to know how your code works, to know when you need to do another assertion to make sure it's still in a good state or not. Luckily, this proposal makes it very easy to do type assertions (compared to the current language), so it should become much easier to make these guarantees.

If this proposal does gain any traction, I might, at a later point, present some of the ideas I came up with to help improve type safety of mutable object types to see if we want to incorporate any of them in, but for now I think I'll just put that on the back-burner.

I'll work on adding a note to the proposal repo about this change in objective, and the fact that there's no guarantee that a mutable object will keep it's type.

[Jamesernator]

Just something worth noting, the proposals for WebAssembly of both Typed function references and Garbage collection add a considerable amount of stuff that would approach nearer to a full type system. Really the only thing these proposals lack is full generics, however, they do have type imports which allow functions to at least be generic up to instantiation time where concrete types must be provided.

So ultimately, assuming browsers do eventually support those proposals, browsers will need to implement fairly expansive type systems regardless of whether JavaScript supports runtime/compile-time types or not.

[jithujoshyjy]

An Idea that comes to mind when thinking about typing semantics in JS is structural typing. Take destructuring for example:

function foo([a, b, c]) {}

Here we're hinting to the JS engine the following facts:

1. first argument to foo is an iterable
2. the iterable contains atleast 3 elements.

The JS engine can rely on first fact but not the second, however it may use this information for optimization. It can do the same with object destructuring. I was wondering if the typing semantics could be derieved partially from pattern matching and similar means.

[theScottyJam]

I'm going to go ahead and close this. In the last tc39 meeting, they discussed the idea of having runtime semantics, sort of like what I presented here, and collectively decided not to pursue it (for now). I too am becoming more of the opinion that having automatic runtime semantics everywhere won't be a good idea for JavaScript.