cognitive psychology. PhD 
Are there any programming languages with *intentionally* unsound static type systems?
-
No, this is no correct. TypeScript and Dart are both unsound became expressions of type Integer do not always produce values of type Integer (or errors). Soundness is not only (or even mostly) about error states.
I agree that the type system doesn't satisfy preservation. But soundness is usually defined as not reaching a stuck state, right? (At least, I double checked TAPL and that's what it says.) And so long as the runtime still has dynamic type checks, the whole system is sound.
-
-
I don't have my copy of TAPL here but I'm pretty sure it defines soundness as progress plus preservation, and preservation fails for these languages.
-
Anyway, progress and preservation are lemmas in the standard proof technique for proving soundness, not soundness itself. If you look at Wright and Felleisen this is called Strong Soundness, and it's a corallary of progress and preservation.
- Show replies
New conversation -
-
-
Not familiar with Typescript, but soundness is tricky. The paper by Wright and Felleisen defines both "weak soundness" and "strong soundness". The former is what you are referring to, the latter also adds that the final result must have the same type as the original expression.
-
Additionally, strictly speaking, a type system may violate progress + preservation and still satisfy soundness. Progress and preservation are a stronger requirement, since type soundness only speaks about the final result (not about the intermediate terms in a reduction).
- Show replies
New conversation -
Loading seems to be taking a while.
Twitter may be over capacity or experiencing a momentary hiccup. Try again or visit Twitter Status for more information.