5 ms·

Safe TypeScript: Safe and Efficient Gradual Typing for TypeScript

99 points by AlexeyBrin 12y ago

thanksgiving 12y ago
Server Error However, you can still reach the paper at http://research.microsoft.com/pubs/224900/safets.pdf http://research.microsoft.com/pubs/224900/safets.pdf bibliography: http://research.microsoft.com/apps/pubs/bibtex.ashx?id=224900 http://research.microsoft.com/apps/pubs/bibtex.ashx?id=22490... Cached at https://webcache.googleusercontent.com/search?q=cache:w8TMT0p2TqoJ:research.microsoft.com/apps/pubs/%3Fid%3D224900+ 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.
- pfraze 12y ago
  loading for me now, but thanks for gathering all that
  - fizzbatter 12y ago
    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)_
    - ripberge 12y ago
      Optimizing the research.microsoft.com blog for heavy traffic is probably low on their priority list.
      - aikah 12y ago
        > 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.
        fizzbatter 12y ago
        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.
- smrtinsert 12y ago
  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?
  - secoif 12y ago
ufo 12y ago
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...
- dandare 12y ago
  I, for one, welcome our new sound overlords if it means better performance.
  - chr1 12y ago
    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
    - discreteevent 12y ago
      You would only turn on the runtime checks during testing.
      - pekk 12y ago
        Which goes to show how much type systems are really adjuncts to testing, rather than something qualitatively different from and better than testing.
- gecko 12y ago
  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.
hencq 12y ago
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.
bernadus_edwin 12y ago
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

99 points by AlexeyBrin 12y ago

Server Error However, you can still reach the paper at http://research.microsoft.com/pubs/224900/safets.pdf http://research.microsoft.com/pubs/224900/safets.pdf bibliography: http://research.microsoft.com/apps/pubs/bibtex.ashx?id=224900 http://research.microsoft.com/apps/pubs/bibtex.ashx?id=22490... Cached at https://webcache.googleusercontent.com/search?q=cache:w8TMT0p2TqoJ:research.microsoft.com/apps/pubs/%3Fid%3D224900+ 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.

pfraze 12y ago
loading for me now, but thanks for gathering all that
- fizzbatter 12y ago
  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)_
  - ripberge 12y ago
    Optimizing the research.microsoft.com blog for heavy traffic is probably low on their priority list.
    - aikah 12y ago
      > 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.
      - fizzbatter 12y ago
        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.
smrtinsert 12y ago
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?
- secoif 12y ago

ufo 12y ago

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

dandare 12y ago
I, for one, welcome our new sound overlords if it means better performance.
- chr1 12y ago
  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
  - discreteevent 12y ago
    You would only turn on the runtime checks during testing.
    - pekk 12y ago
      Which goes to show how much type systems are really adjuncts to testing, rather than something qualitatively different from and better than testing.
gecko 12y ago
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.

hencq 12y ago

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.

bernadus_edwin 12y ago

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