[lolinder]

Soundness is also a highly theoretical issue that I've never once heard a professional TypeScript developer express concern about and have never once heard a single anecdote of it being an issue in real-world code that wasn't specifically designed to show the unsoundness. It usually only comes up among PL people (who I count myself among) who are extremely into the theory but not regularly coding in the language.

Do you have an anecdote (just one!) of a case where TypeScript's lack of type system soundness bit you on a real application? Or an anecdote you can link to from someone else?

[nyssos]

> Do you have an anecdote (just one!) of a case where TypeScript's lack of type system soundness bit you on a real application?

Sure. The usual Java-style variance nonsense is probably the most common source, but I see you're not bothered by that, so the next worst thing is likely object spreading. Here's an anonymized version of something that cropped up in code review earlier this week:

    const incomingValue: { name: string, updatedAt: number } = { name: "foo", updatedAt: 0 }

    const intermediateValueWithPoorlyChosenSignature: { name: string } = incomingValue

    const outgoingValue: { name: string, updatedAt: string } = { updatedAt: new Date().toISOString() , ...intermediateValueWithPoorlyChosenSignature }

[lolinder]

I mean... yes, there's a footgun there where you have to know to spread first and then add the new properties. That's just a good practice in the general case: an intermediate type that fully described the data wouldn't have saved you from overwriting it unless you actually looked closely at the type signature.

And yes, TypeScript types are "at least these properties" and not "exactly these properties". That is by design and is frankly one reason why I like TypeScript over Java/C#/Kotlin.

I'd be very interested to know what you'd do to change the type system here to catch this. Are you proposing that types be exact bounds rather than lower bounds on what an object contains?

[nyssos]

> That's just a good practice in the general case: an intermediate type that fully described the data wouldn't have saved you from overwriting it unless you actually looked closely at the type signature.

The issue isn't that it got overridden, it's that it got overridden with a value of the wrong type. An intermediate type signature with `updatedAt` as a key will produce a type error regardless of the type of the corresponding value.

> I'd be very interested to know what you'd do to change the type system here to catch this.

Like the other commenter said, extensible records. Ideally extensible row types, with records, unions, heterogeneous lists, and so on as interpretations, but that seems very unlikely.

[haskman]

Look into "Row types" and how PureScript, Haskell, and Elm (to a limited extent) do it.

'{foo :: Int | bar} is a record with a known property 'foo' and some unspecified properties 'bar'. You cannot pass a `{foo :: Int, bar :: Int}` into a function that expects `{foo :: Int}`.

A function that accepts any record with a field foo, changes foo, keeping other properties intact has the type

    {foo :: Int | bar} -> {foo :: Int | bar}

[kcrwfrd_]

Ah someone else posted a link and I understand the unsoundness now.

The only time an issue ever came up for me was in dealing with arrays

  let foo: number[] = [0, 1, 2]

  // typed as number but it’s really undefined
  let bar = foo[3]

But once you’re aware of the caveat it’s something you can deal with, and it certainly doesn’t negate the many massive benefits that TS confers over vanilla JS.

[AfterAnimator]

For this case, I've switched to using `foo.at(3)` now instead, as it returns `T | undefined`, so you have to handle the undefined case.

[lolinder]

Yeah, that example is unsound in the same way that Java's type system is unsound, it's a compromise nearly all languages make to avoid forcing you to add checks when you know what you're doing. That's not the kind of problem that people usually are referring to when they single out TypeScript.