Is this “unsound”-ness that you’re referring to because it uses structural typin...

cstrahan · 2024-07-25T15:18:20 1721920700

No, TypeScript is not unsound because it uses structural typing.

A language has a sound type system if every well-typed program behaves as defined by the language's semantics during execution.

Go is structurally typed, and yet it is sound: code that successfully type checks is guaranteed to abide the semantics of the language.

TypeScript is unsound because code that type checks does not necessarily abide the semantics of the language:

  function messUpTheArray(arr: Array<string | number>): void {
      arr.push(3);
  }
  
  const strings: Array<string> = ['foo', 'bar'];
  messUpTheArray(strings);
  
  const s: string = strings[2];
  console.log(s.toLowerCase())

`strings` is declared as a `Array<string>`, but TypeScript is happy to insert a `number` into it. This is a contradiction, and an example of unsoundness.

`s` is declared as `string`, but TypeScript is happy to assign a `number` to it. This is a contradiction, and an example of unsoundness.

This code eventually fails at runtime when we try to call `s.toLowerCase()`, as `number` has no such function.

What we're seeing here is that TypeScript will readily accept programs which violate its own rules. Any language that does this, whether nominally typed or structurally typed, is unsound.

nyssos · 2024-07-25T13:35:25 1721914525

There's not much connection. Typescript's record types aren't sound, but that's far from its only source of unsoundness, and sound structural typing is perfectly possible.

lolinder · 2024-07-25T13:44:36 1721915076

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 · 2024-07-25T17:36:25 1721928985

> 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 · 2024-07-25T19:40:21 1721936421

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 · 2024-07-26T11:32:46 1721993566

> 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 · 2024-07-26T08:58:39 1721984319

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_ · 2024-07-25T16:14:31 1721924071

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 · 2024-07-30T13:25:01 1722345901

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 · 2024-07-25T16:46:47 1721926007

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.