Safe TypeScript: Safe and Efficient Gradual Typing for TypeScript | Hacker News Reader

Safe TypeScript: Safe and Efficient Gradual Typing for TypeScript

research.microsoft.com

99 pointsAlexeyBrin19 comments

I wonder what the typescript community thinks of this. For a long time, one of the big things about typescript was that they didn't value soundness very highly and had a bit of a "we are a pragmatic language willing to cut corners" vibe. But now with Safe Typescript and Soundscript we see a bit of a return to traditional type systems that care a lot about soundness...

I think this is actually still on the pragmatic scale.

Start with normal JavaScript. Gradually add typing. When you hit a point where it's sufficiently typed, and the situation calls for it, you can increase things further to Safe TypeScript. There doesn't honestly see to be a contradiction here, and I for one am psyched.

I, for one, welcome our new sound overlords if it means better performance.

Though gaining better performance through sound type system seems quite unlikely, in the best case there will be small overhead, but 15% they claim now is still large.

from the article:

> we measure a 15% runtime overhead for type safety

You would only turn on the runtime checks during testing.

Which goes to show how much type systems are really adjuncts to testing, rather than something qualitatively different from and better than testing.

Server Error

However, you can still reach the paper at http://research.microsoft.com/pubs/224900/safets.pdf

bibliography: http://research.microsoft.com/apps/pubs/bibtex.ashx?id=22490...

Cached at https://webcache.googleusercontent.com/search?q=cache:w8TMT0...

Text:

Safe & Efficient Gradual Typing for TypeScript Aseem Rastogi, Nikhil Swamy, Cedric Fournet, Gavin Bierman, and Panagiotis Vekris July 2014

Abstract

Current proposals for adding gradual typing to JavaScript, such as Closure, TypeScript and Dart, forgo soundness to deal with issues of scale, code reuse, and popular programming patterns.

We show how to address these issues in practice while retaining soundness. We design and implement a new gradual type system, prototyped for expediency as a ‘Safe’ compilation mode for TypeScript.1 Our compiler achieves soundness by enforcing stricter static checks and embedding residual runtime checks in compiled code. It emits plain JavaScript that runs on stock virtual machines. Our main theorem is a simulation that ensures that the checks introduced by Safe TypeScript (1) catch any dynamic type error, and (2) do not alter the semantics of type-safe TypeScript code.

Safe TypeScript is carefully designed to minimize the performance overhead of runtime checks. At its core, we rely on two new ideas: differential subtyping, a new form of coercive subtyping that computes the minimum amount of runtime type information that must be added to each object; and an erasure modality, which we use to safely and selectively erase type information. This allows us to scale our design to full-fledged TypeScript, including arrays, maps, classes, inheritance, overloading, and generic types.

We validate the usability and performance of Safe TypeScript empirically by typechecking and compiling more than 100,000 lines of existing TypeScript source code. Although runtime checks can be expensive, the end-to-end overhead is small for code bases that already have type annotations. For instance, we bootstrap the Safe TypeScript compiler (90,000 lines including the base TypeScript compiler): we measure a 15% runtime overhead for type safety, and also uncover programming errors as type-safety violations. We conclude that (1) large TypeScript projects can easily be ported to Safe TypeScript, thereby increasing the benefits of existing type annotations, (2) Safe TypeScript can reveal programming bugs both statically and dynamically, (3) statically type code incurs negligible overhead, and (4) selective RTTI can ensure type safety with modest overhead.

The attractive part for me when considering TypeScript was that it had 0 runtime overhead, while coding in a type safe manner. If I use nothing but types via my TypeScript code, isn't Safe TypeScript simply just overhead?

The overhead of safe typescript is only in the parts of your code that interact with untyped code. For those parts the default typescript was actually unsafe.

I see. This adds soundness to an entire application ts or non ts.

The main goal of a sound gradual type system is to make it so that any type errors can be "blamed" on the untyped part of the code. For example, if untyped code calls a safe-typescript function and passes the wrong argument type safe-typescript will check and detect the error right away. On the other hand, traditional typescript would accept the invalid parameter without checking and would eventually throw a "method missing" exception somewhere down the line.

Compile-time checks can't make guarantees about 3rd party code or user input.

loading for me now, but thanks for gathering all that

failing off and on it seems. 5 minutes ago it was working for me, now it's failing every time.

Surprised to see Microsoft having issues on a blog _(don't mean that in a snarky way, just commenting)_

Optimizing the research.microsoft.com blog for heavy traffic is probably low on their priority list.

> Optimizing the research.microsoft.com blog for heavy traffic is probably low on their priority list.

You'd imagine it is hosted on azure and would scale with a single click ... it's not a question of priority.

Not to mention.. it's a blog. I thought a CDN layer made that sort of a no-brainer. We're not talking a highly dynamic experience here.. this could be static if they wanted, heh.

I think a good way to marketing typescript is provide tool converter c# to typescript. It would be fun is there is tool convert my mvvm portable library to typescript angular js. If microsoft provide this, i can porting my mobile app to mobile site easily. And then automaticly i will learn typescript

I wonder how this relates to Soundscript which was on the frontpage yesterday. They seem to have similar goals and both are based on Typescript, so they seem to overlap a lot.

Reply on news.ycombinator.com