[agentultra]

Nice course, and nice site.

Although, as a Haskell developer, I am curious what type system TS is using (System F? Intuitionist? etc) and what limitations one can expect. Aside from the syntax of TS being what it is, what are the trade-offs and limitations?

I was under the impression, and this was years ago -- things are probably different now?, that TS's type system wasn't sound (in the mathematical logic sense).

[AaronFriel]

I don't believe it is using any type system described outside of the TypeScript compiler. The goal of the system is to accurately describe real-world JavaScript programs and semantics, not to introduce a formalization that existed elsewhere and impose it on JS.

As a consequence, it has aspects of structural types, dependent types, type narrowing, and myriad other features that exist solely to model real-world JavaScript.

As far as soundness: it's not a goal of the type system. https://www.typescriptlang.org/docs/handbook/type-compatibil...

[323]

Non-soundness is sort of a feature, it lets you force your way through and just say "trust me, this is a Thing" when it's just hard (or impossible) to make TypeScript see that. In practice, you can write large code bases where you only need to do this every 1000 lines or so. Not ideal, but better than no typing.

[hither_shores]

Being able to opt in to unsoundness is arguably a feature, but TypeScript is still unsound even without using assertions or `any`.

[agentultra]

Is it fair to say that the limitation is that the type checker can admit programs that are not type correct?

[spion]

You can make "believe_me" assertions, which is incredibly useful when writing advanced (metaprogramming heavy) library code. The idea is to try and contain / and heavily test the small "unsafe" library part and isolate it from the rest of the code, then enjoy the advanced type transformations and checks in the "normal" application code.

For example, an SQL query builder library may internally do unchecked assertions about the type of the result row that a query transformation would produce (e.g. group_by), however assuming that part is correct, all application code using the query builder's group_by method would benefit from the correct row types being produced by `group_by` which can then be matched against the rest of the application code.

[323]

Yes. For example it has the "any" type which will bypass any sort of type check.

But I think it's more nuanced. Depends of what you mean by type correct. Even in Haskell you can override the compiler and say "trust me on this".

[jakear]

Any isn’t required. The go-to example of unsoundness is the Cat[] ref that you alias as an Animal[], append a Dog to, then map over the original ref calling ‘meow()’ on each entry.

[AaronFriel]

JavaScript arrays are heterogeneous and TypeScript permits covariance here because the underlying language lacks any mechanism to freeze any shared references to the array to prevent it.

TypeScript could restrict this to be through an operation that creates a new array (e.g.: via .slice()), however that would impose a performance deficit versus vanilla JavaScript. It's not acceptable to the TypeScript project to impose a cost on what would, in JS, just be array assignment or argument passing.

It would be a neat idea to allow a "strictCovariance" mode to allow covariance only with readonly arrays - I think that might solve the issue? i.e.: I can cast "Cat[]" to a "readonly Animal[]", but not to a mutable "Animal[]".

[diroussel]

Yea, because typescript is trying to model what can be done in JavaScript, which is a very permisssive runtime.

[Tade0]

That's by design, considering that its original purpose was to introduce static typing in JS codebases.