4 ms·

> Its better to have no types at all than wrong types. I agree - but the type systems of both Python and TypeScript are unsound, so all type hints can potentia

by pansa2 2y ago

> Its better to have no types at all than wrong types. I agree - but the type systems of both Python and TypeScript are unsound, so all type hints can potentially be wrong. That's one reason why I still mostly use untyped Python - I don't think it's worth the effort of writing type annotations if they're just going to sit there and tell lies. Or maybe the unsoundness is just a theoretical issue - are incorrect type hints much of a problem in practice?

zoul 2y ago
In my experience unsoundness is almost never a problem in practice, see here for details: https://effectivetypescript.com/2021/05/06/unsoundness/ https://effectivetypescript.com/2021/05/06/unsoundness/
- hajile 2y ago
  Unsound types are never a problem until they are at which point you are staring at code that SHOULD be working, but is somehow breaking.
lolinder 2y ago
I've been using TypeScript professionally for 6+ years and have only ever run into issues at the border between TypeScript and other systems (usually network, sometimes libraries that don't come with types). There are a few edge cases that I'm aware of, but they don't really come up in practice.
kcrwfrd_ 2y ago
Is this “unsound”-ness that you’re referring to because it uses structural typing and not nominal typing? Fwiw I’ve been working with TypeScript for 8+ years now and I’m pretty sure wrong type hints has never been a problem. TS is a God-send for working with a codebase.
- nyssos 2y ago
  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 2y ago
    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?
    - kcrwfrd_ 2y ago
      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.
      - lolinder 2y ago
        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.
      - AfterAnimator 2y ago
        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.
    - 2y ago
- cstrahan 2y ago
  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.

by pansa2 2y ago

zoul 2y ago

In my experience unsoundness is almost never a problem in practice, see here for details: https://effectivetypescript.com/2021/05/06/unsoundness/ https://effectivetypescript.com/2021/05/06/unsoundness/

hajile 2y ago
Unsound types are never a problem until they are at which point you are staring at code that SHOULD be working, but is somehow breaking.

lolinder 2y ago

I've been using TypeScript professionally for 6+ years and have only ever run into issues at the border between TypeScript and other systems (usually network, sometimes libraries that don't come with types). There are a few edge cases that I'm aware of, but they don't really come up in practice.

kcrwfrd_ 2y ago

Is this “unsound”-ness that you’re referring to because it uses structural typing and not nominal typing? Fwiw I’ve been working with TypeScript for 8+ years now and I’m pretty sure wrong type hints has never been a problem. TS is a God-send for working with a codebase.

nyssos 2y ago
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 2y ago
  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?
  - kcrwfrd_ 2y ago
    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.
    - lolinder 2y ago
      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.
    - AfterAnimator 2y ago
      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.
  - 2y ago
cstrahan 2y ago
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.