Is Sound Gradual Typing Dead? Performance Problems in Typed Racket (2016)

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

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?