3 ms·
There’s no such thing as “fully sound” type system, outside theorem provers like Lean. Every type system has a trapdoor. Rust has “unsafe”. Haskell has “unsafeP
by zarzavat 4y ago
There’s no such thing as “fully sound” type system, outside theorem provers like Lean. Every type system has a trapdoor. Rust has “unsafe”. Haskell has “unsafePerformIO”. And TypeScript has “any”. Soundness is just as much a property of a language’s culture as its implementation. Practically I find that TypeScript is sound enough for my purposes when most of the strictness options are enabled.
- graftak 4y agoAbout 90% of any can and should be replaced with unknown which is infinitely more useful and a lot safer. There is an example signature at the end of the article; (x: any) => string, this error would not fly if x were unknown. On of the few remaining scenarios where any might be necessary is to narrow down a generic param, ie <T extends Something<any>>.