6 ms·

The type system is not sound… that is there are things which the type checker cannot prove. Not that the languages themselves are unsound.

creata 4y ago
1. That's a horrible description of unsoundness; you're making it sound like incompleteness! 2. What I meant to ask was: what does satvikpendem mean by "JS is unsound"? It's a dynamically typed language, so they can't be talking about soundness in the type system...
- orta 4y ago
  I did a bit of a writeup on the gaps in soundness for TypeScript in the docs, https://www.typescriptlang.org/play?strictFunctionTypes=false#example/soundness https://www.typescriptlang.org/play?strictFunctionTypes=fals...
- satvikpendem 4y ago
  I should clarify, the JS type system is unsound, and because JS is valid TS, TS is by extension also unsound. Not sure why you'd think a dynamically typed language cannot be unsound, it still has types, they're just not static.
  - creata 4y ago
    Define soundness. Here's something close to the definitions that I've seen: > The central result we wish to have for a given type-system is called soundness. It says this. Suppose we are given an expression (or program) e. We type-check it and conclude that its type is t. When we run e, let us say we obtain the value v. Then v will also have type t. - https://papl.cs.brown.edu/2014/safety-soundness.html https://papl.cs.brown.edu/2014/safety-soundness.html This only makes sense in the context of static types afaict, because you do not "typecheck an expression" in a dynamically typed language.
    - satvikpendem 4y ago
      Types can be checked at runtime too, not just compile time. A language is sound if all types, even at runtime, are what they say they are. Zod for TypeScript is one example of checking this at runtime, although it's not fully safe either.
satvikpendem 4y ago
Soundness is not decidability. The reason TS is unsound is not directly because it's undecidable, as any Turing complete system is undecidable, and the TS type system is Turing complete.

creata 4y ago

1. That's a horrible description of unsoundness; you're making it sound like incompleteness! 2. What I meant to ask was: what does satvikpendem mean by "JS is unsound"? It's a dynamically typed language, so they can't be talking about soundness in the type system...

orta 4y ago
I did a bit of a writeup on the gaps in soundness for TypeScript in the docs, https://www.typescriptlang.org/play?strictFunctionTypes=false#example/soundness https://www.typescriptlang.org/play?strictFunctionTypes=fals...
satvikpendem 4y ago
I should clarify, the JS type system is unsound, and because JS is valid TS, TS is by extension also unsound. Not sure why you'd think a dynamically typed language cannot be unsound, it still has types, they're just not static.
- creata 4y ago
  Define soundness. Here's something close to the definitions that I've seen: > The central result we wish to have for a given type-system is called soundness. It says this. Suppose we are given an expression (or program) e. We type-check it and conclude that its type is t. When we run e, let us say we obtain the value v. Then v will also have type t. - https://papl.cs.brown.edu/2014/safety-soundness.html https://papl.cs.brown.edu/2014/safety-soundness.html This only makes sense in the context of static types afaict, because you do not "typecheck an expression" in a dynamically typed language.
  - satvikpendem 4y ago
    Types can be checked at runtime too, not just compile time. A language is sound if all types, even at runtime, are what they say they are. Zod for TypeScript is one example of checking this at runtime, although it's not fully safe either.

satvikpendem 4y ago

Soundness is not decidability. The reason TS is unsound is not directly because it's undecidable, as any Turing complete system is undecidable, and the TS type system is Turing complete.