Is sound gradual typing dead? | Hacker News Reader

Is sound gradual typing dead?

blog.acolyer.org

70 pointsmrry17 comments

This paper both introduces a method for evaluation, which the paper's authors say is their primary contribution, and then use the method to identify some performance problems in Typed Racket. Fortunately, we've been able to make some of those performance issues a lot better just by fixing small things. Some of those fixes will be in the next Racket release, and some in the one after that.

However, some of the performance overhead requires a more sophisticated compiler, just like higher order functions or objects. I'm working on this using jit compilers, and other people are looking at other approaches. I think this will be a major area of research in the near future.

Full disclosure: I'm the author and maintainer of Typed Racket.

I really like Racket, but never gave Typed Racket a chance and probably should. I sort if fell in love with types after tinkering in Rust. My main issue was I saw no hope for targeting mobile platforms for Racket. Is this still the case, do you know?

It's likely that the big overhead slowdowns come from points where an object containing many typed elements is passed through without processing. This requires field by field checking, in the form of dynamic checks in a naive implementation. This could be repeated through several levels of function calls before the object is used. Mixing typed and untyped code makes this very likely.

It's a big concern that Python is going this route. With terrible syntax, too. Some type info is in comments, because it couldn't be crammed into the syntax, but some type info is in non-comment "annotations". I've been saying for a while, "Stop Python's little tin god before he kills again". Python 4 may be headed for another Python 3 like debacle.

I am wondering what would happen if you left out the addition of run-time checks, and performed only those static checks that the partial typing has enabled? (I guess that would make it unsound, but perhaps it is worth it.)

I would not be at all surprised to learn that little or no static checking is possible until quite a lot of typing has been completed. We see, however, that the performance lattice in the article shows (for that particular example) that the net cost begins falling after about half of the typing is completed. Is it valid to assume that this is a result of additional type information allowing static analysis to remove or simplify run-time checks? If so, we can also note that this is a net effect, so static analysis could be having some benefit earlier in the transformation.

Yes, unsound gradual typing is clearly worth it. For example, using Typescript shouldn't have any performance penalties over JavaScript since it's purely a compile time thing.

> if you left out the addition of run-time checks, and performed only those static checks that the partial typing has enabled?

This is effectively what "optional types" are, which is a sort of sister technology to "gradual types". With optional types, they are only used to show static type errors to the user during development time. At runtime, all of the type annotations are ignored and the program runs like it is fully dynamically typed.

This is how Dart, TypeScript, and (I think) ActionScript, Hack, and Flow work. You'll note that those are all languages from industry and have had various degrees of success and real-world usage.

Dart can also be run in "checked mode", which means it will also do the runtime checks with worse—but not catastrophically so— performance. Sort of like running a debug build with asserts enabled. (And, in fact, checked mode also enables the assert() statement in Dart.)

Where does Julia fit in here? Is it optionally typed or gradually typed? Because from what I understand its design choices make it a much simpler language to JIT-compile than JavaScript or Lua.

Julia is in a category by itself because it requires runtime reflection on types to do just-in-time compilation of code at the time of a method call.

It looks like it would be quite hard to translate Julia code to another language that doesn't have multi-method dispatching, so you pretty much need a Julia VM to run it.

This sentence deserves to be examined for alternatives:

"To make all this work, you have to insert runtime checks between the typed and untyped portions of the program."

That makes it sounds as if there are 2 choices:

1.) insert runtime checks

2.) don't insert runtime checks

I'll point out that many platforms (in particular, the JVM) allow us to pursue a 3rd option:

3.) insert runtime checks in development and whenever you are debugging, but strip them out when you are in production and things are going well

You can fill your code pre and post assertions on functions. These slow your software but they give you most of the benefits of gradual typing. You can run your code with these assertions whenever you need to debug. But if you ever want a speed boost, and you feel like your software is stable and bug-free, then you can simply pass a flag to the JVM compiler, and it will strip out the assertions for you.

Short of a formal proof (or a sound type system), you can't be sure that you never hit a type error in production that now wouldn't be caught.

Typescript (an extension to JS that adds type-safety) essentially does option 3 as well.

As the sibling noted, there are instances during runtime where the type checking fails, especially because Typescript is compiling to Javascript. I have had moments where a numeric observable in KnockoutJS had to be forced to a number when receiving a new value; the form that the observable is bound to is simply returning a string, and while the TS interface for KnockoutJS says the observable is a number, the actual JS doesn't care and just returns what the form gives it.

In some ways this is a failing of Typescript; it shouldn't allow strongly-type interfaces to be wrapped around JS that can return varying types.

Typescript doesn't insert any runtime type checks at all. It also can't know that interfaces for raw JS are typed wrong, because Typescript is only a static checker.

Dart in checked mode does insert runtime type checks, but leaves them out in production mode.

Can someone explain why the performance is effected so dramatically? It seems, you would need to add type checking overhead, but it also seems like you could make better optimizations and remove a layer of indirection.

Doing the type checking increases the minimum cost of evaluating a block of code. For instance consider this simple function.

function int_id(x: int): int { return x; }

If this code is executed with no run time checks then the body will do no work and return x. However if we are forced to perform run time type checks to enforce soundness then the body will look something like.

function int_id(x: int): int { assert(x is int); return x; }

Nice paper. After reading the paper I was motivated to read the Typed Racket Guide. I have been using Haskell a lot but I am open to alternative typed languages.

BTW, the premise of the paper seems very intuitive: better to either use a strongly typed language or a dynamic scripting Lange. Avoid the middle ground.

Previous discussion on a related paper: https://news.ycombinator.com/item?id=10773457

I'm not sure why people keep using the word "dead" regarding code annotations. They're easily stripped out for release builds and clearly provide value in many debugging and maintenance scenarios. And yes, like everything else in the static vs dynamic debate, there's no free lunch.

Re: why people are using the word "dead" regarding code annotations:

Without getting into a discussion about the title being clickbaity (I think it is), the paper's point is still entirely valid. Yes, you can ignore the annotations for production builds as you point out, but then you don't get the soundness guarantees at the edges of untyped and typed code, and that's the entire crux of the paper.

Reply on news.ycombinator.com