Comment by ashton314 | Hacker News Reader

Comment by ashton314 | Hacker News Reader

This is called “the dead horse paper” for some reason. There’s been some interesting work since. This isn’t my exact area of research, but I’m pretty well versed in it and I work with one of the authors on this paper so I’m happy to try and answer any questions.

The chief issue here is how do you assign blame to typing violations? Typescript is unsound: since it just erases types, an untyped library that a typed component is using might return something the typed component isn’t expecting leading you to get a type error in typed code. Gradually typed python variants typically are better, though they usually just inspect the shape of the data and don’t check that eg every element in a list is correctly typed as well. This can lead to more unsound behavior. Typed Racket is fully sound, but performance can degrade spectacularly.

There’s been some work reviving the dead horse being beaten in this paper. Lmk if you have questions.

More papers:

Muehlboeck, Fabian, and Ross Tate. “Sound Gradual Typing Is Nominally Alive and Well.” Proceedings of the ACM on Programming Languages 1, no. OOPSLA (October 12, 2017): 56:1-56:30. https://doi.org/10.1145/3133880.

Moy, Cameron, Phúc C. Nguyễn, Sam Tobin-Hochstadt, and David Van Horn. “Corpse Reviver: Sound and Efficient Gradual Typing via Contract Verification.” Proceedings of the ACM on Programming Languages 5, no. POPL (January 4, 2021): 53:1-53:28. https://doi.org/10.1145/3434334.

Lazarek, Lukas, Ben Greenman, Matthias Felleisen, and Christos Dimoulas. “How to Evaluate Blame for Gradual Types.” Proceedings of the ACM on Programming Languages 5, no. ICFP (August 18, 2021): 68:1-68:29. https://doi.org/10.1145/3473573.

> Typescript is unsound: since it just erases types, an untyped library that a typed component is using might return something the typed component isn’t expecting leading you to get a type error in typed code. Gradually typed python variants typically are better, though they usually just inspect the shape of the data and don’t check that eg every element in a list is correctly typed as well

This is not typically what is meant by soundness. Most gradual type systems erase types (see also Python, Ruby, Elixir), and provide ways of overriding the type system's inference and forcing a certain expression to be typed a certain way, even if that type cannot be proven by the type checker.

What makes TypeScript unsound is that, even if you don't override the type checker at all, there are certain expressions and constructs that will produce no compile-time error but will produce a runtime error. This is a deliberate choice by the TypeScript team to make the type checker less correct, but simpler to use and adopt. The Flow type checker took the opposite approach and was sound, but was occasionally harder to use.

I believe most type checkers in other languages tend to hew closer to the TypeScript approach, and favour being intuitive to use over being completely sound. However, they do work in the same way of being compile-time constructs only, and not affecting runtime at all. Python is slightly exceptional here in that the type annotations are available as metadata at runtime, but are not used for type checking unless the user explicitly checks them at runtime. There are a couple of runtime libraries that add decorators that automatically do this runtime type checking, but (a) their usage is fairly rare, and (b) their presence does not change how the type checker behaves at all.

No, this is exactly what is meant by soundness. Using the `Any` type in TypeScript can result in values that have type `integer` being actually strings, which is unsoundness.

Type erasure has nothing to do with soundness - ocaml also erases types at runtime but it is sound. In typescript "any" type, unsafe casting, non null assertions and couple of other constructs are unsound. Gradual typing at package level was addressed by (also unsound) declaration repository (overall successful I'd say - primary reason it won over flow in my opinion).

I have a problem reconciling "sound gradual typing" - is there such thing at all? Sounds like contradiction to me, no? Untyped function's result can be considered "unknown" (as opposed to "any" using typescript terminology) and require runtime checks at call site (as if it was i/o boundary) - that's fine but arguments on the other hand must have some type declaration on its signature to be considered sound. Injecting runtime checks in untyped library for arguments feels nonsensical because if you can do it then you already did static code analysis that did infer argument types and you can shove it into function signature as static type declaration - ie. that's just more sophisticated static inference that doesn't require runtime code injection.

You could argue that there may be some dynamism that cannot be expressed at type level and that requires runtime checks deeper in the untyped code but if it cannot be expressed then by definition it's unsound and frankly who cares about runtime checks nested deeply in untyped code - what's the difference if it blows up at runtime in the middle of that untyped function with type error or some other error?

Reply on news.ycombinator.com