It's compile-time safety. Virtually none of the type knowledge exists in the runtime. Still, it's far better than nothing, with the self-documenting nature of typed code being one of the biggest wins IMO.
The same way it transfers when the language is compiled to x86 instructions! By adding a pre-written and pre-compiled runtime.
So the correctness transfers in the sense that the code the compiler output should always be correct.
For example, the way you allocate memory in WASM is to link in a malloc() implementation. This malloc lives in the same linear memory block, and so its internal data structures are vulnerable to being smashed, just like classical heap smashing.
One improvement is that the call stack is maintained externally, so it is not possible to stack-smash a return address. Still heap function pointers are vulnerable to a return-to-libc style attack.
Round and round we go.
[1] https://www.typescriptlang.org/docs/handbook/advanced-types....
Well, your understanding is wrong. Sum types satisfy a specific universal property, which union types don't.
(0) There exists a procedure “foo” that recovers the functions from the summands, given a function from the sum.
(1) There exists a procedure “bar” that recovers the function on the sum, given the functions from the summands.
(2) “bar . foo” is the identity on the space of functions from the sum.
(3) “foo . bar“ is the identity on the space of tuples of functions from the summands.
It is easy to see that, if your definition of “sum” is “a JavaScript tagged union”, and your definition of “function” is “any JavaScript function”, such functions “foo” and “bar” are not constructible.
Tagged unions only work under very stringent conditions:
(0) Tags never overlap. Have fun enforcing this.
(1) Tags are only used to discriminate between cases. Again, have fun enforcing this.
Moreoever, any talk about universal properties being satisfied is utterly pointless when object identities permeate the semantics of the language.
> Tags never overlap.
Agreed that TypeScript doesn't enforce this property of the type definition, and it would be nice that it did, although my interpretation of the claim was "any sum type is expressible as a tagged union". I certainly don't claim that TypeScript has a syntax for describing tagged unions and ensuring that they're well-formed; it's just that they're expressible via other features.
> Tags are only used to discriminate between cases.
It's true that tags are string values in my case, although possibly a fancier version could use opaque values. But given that TypeScript enforces that the type is either 'A' or 'B', couldn't any other language derive that string from the case and use it?
Do you view (say) SML datatypes as being valid sum types? I'm having a hard time understanding when SML types would be strictly more powerful/expressive than TypeScript here.
https://www.typescriptlang.org/play/index.html#src=type%20A%...
I think you missed the word “broken”, before “languages”. Sums in Standard ML are really sums.
> similar to how it's nice to just pretend that computers work on real numbers instead of floats.
Computers can totally work on real numbers. (Okay, not all of them. But way many more than floats allow.) For example, you can implement an abstract type whose internal representation is Cauchy streams of rationals, and only provide operations that send equivalent streams to equivalent ones. Of course, this would be horribly slow, and few people actually need exact real arithmetic anyway.
> In this case, maybe you'd need to pretend that JS works on values rather than having object identity.
JavaScript does work on values. The values are the object identities.
> See the link at the bottom for what I think foo and bar would be in TypeScript. I'm curious if you see specific weaknesses in it.
You anticipated it yourself:
https://www.typescriptlang.org/play/index.html#src=type%20A%...
> Do you view (say) SML datatypes as being valid sum types?
Yes. On the other hand, Haskell's aren't, albeit for different reasons than the ones given in this thread.
> I'm having a hard time understanding when SML types would be strictly more powerful/expressive than TypeScript here.
In Standard ML, type abstraction actually works. You can hide the implementation of an abstract type, making it impossible for others to destroy the invariants that you worked so hard to establish. Or at least should have.
See here for why union and intersection types make type abstraction difficult: https://news.ycombinator.com/item?id=16399722
I'd say the best type systems are found in Rust (naturally models zero-cost abstractions but doesn't have dependent types) and Idris and Coq (have dependent types but don't naturally model zero-cost abstractions).
That's true in pretty much all languages. Even in Haskell you can use `unsafeCoerce`. In Rust you have 'unsafe' blocks. And any language which has a FFI you can implement the type-safety-violating functions in the foreign language (often C).
Instead TypeScript has a bunch of serious unfixed design flaws that make the problem pervasive, plus they refuse to fix them (see https://github.com/Microsoft/TypeScript/issues/9825 ).
MLs (OCaml, F#, Reason) are hardly "extreme functional spectrum".
(Really I'd like polykindedness as well. I've only needed it once in over a decade of programming but it was such an intensely frustrating experience to need it and not have it)
That you have to return from statements is such a flow-breaking PITA, one that leads to ugly, verbose code. switch is particularly painful in this regard, would be wonderful to write `let foo = switch (x) { case ... }`, but no, it's a statement, not a value.
Also, structural typing has its strengths, but equality is not one of them. In order to generate a nominal type you have to hack in a private class member (what they call "branding"). This makes newtype/value class wrappers needlessly verbose.
TS feels somehow like a Java/Javascript hybrid with some more advanced type system features (e.g. union types) mixed in. Saying that, editor support (VS Code) and JS interop are pretty amazing.