I'm excited about compiling to WASM not for performance but for correctness. Typescript is better than nothing but it really can't compete with the safety and ease you get from a language with a really good type system.
One thing I've been confused with about transpiled languages is how does correctness transfer? How do types or lifetimes etc. transfer to WASM, for instance? Or does it just depend on the correctness to be verified in the pre-compilation/transpilation stages?
Correctness is typically checked long before code generation happens. This does mean the code generation backend must be trusted, whether the target be x86 or wasm. Just as you have to trust CPUs to not expose processes' memory to each other (oops).
Typed assembly is a thing - it’s mainly to ensure the compiler itself is correct, but it does give stronger guarantees. I think Frank Pfenning at CMU has written a language that’s dependently typed all the way down - so it’s IR and assembly are both dependently typed.
edit: I misread the question, my comment was geared toward languages transpiled to JS.
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.
No correctness isn't usually ensured with a runtime in these languages with stronger type systems, it's usually done with static analysis on an intermediate representation at compile-time.
WASM gives you a linear memory block and performs only bounds checking. It provides very few higher-order abstractions.
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.
Unlike typical assembly, WASM enforces strong guarantees around memory safety (which I'll argue is precisely what you want for something with a web browser's attack surface). This does imply a performance hit (conventional wisdom is that WASM will, at best, be half as fast as "native" code), but also insulates the user from the usual memory-related pitfalls of C. Code transpiled from Rust is forced to pay this price as well, despite Rust providing substantially stronger memory safety guarantees than C; fortunately if you're using Rust you'll probably be the sort of person who agrees that this is a good thing, because Rust still lets one drop into unsafe blocks and potential memory unsafety in untrusted code delivered over the network is pretty much a nightmare scenario.
Same way it does when compiling to C or assembly, the correctness is checked on the source and assume the codegen and platform you run on behave correctly (and fix/work around bugs which inevitably arise).
So the correctness transfers in the sense that the code the compiler output should always be correct.
What would you consider to be a "good type system"? I find typescript to have one of the most sane and still strict type systems of all languages that doesn't fall into the extreme functional spectrum or those that care about memory ownership.
Any language that doesn't have first-class support for ADTs is a waste of my time. And I say that as someone who's working with TypeScript all day long, and try to push it in my team, even though it sometimes requires verbose code and boilerplate. But I take that over plain JS any day. It took long enough for my coworkers to recognise the benefit of a type system. Can't push them too hard too far too quickly.
When you say ADTs, do you mean algebraic data types or abstract data types? My impression has been that TypeScript is quite good at algebraic data types (i.e. tagged unions). You need to use normal conditionals like if/switch or your own function instead of syntactic support for pattern matching, but IMO the static analysis makes it work out pretty well.
To be clear, I was talking about tagged unions; TypeScript supports both tagged and untagged unions[1]. My understanding is that "tagged unions" and "sum types" are the same thing, and Wikipedia[2] seems to agree.
The universal property for a sum type that having an X-valued function from a sum is equivalent to having X-valued functions from each summand, for any type X. In other words:
(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.
Interesting, thanks for the explanation. 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. Seems like maybe this is all just a clash between formalism and how languages work in practice, similar to how it's nice to just pretend that computers work on real numbers instead of floats. In this case, maybe you'd need to pretend that JS works on values rather than having object identity.
> 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.
> Seems like maybe this is all just a clash between formalism and how languages work in practice,
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.
> 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.
It's not: the TypeScript type system is unsound (accepts code that violates it), and there are no runtime checks, so it doesn't actually guarantee anything: a TypeScript variable may in fact contain any value regardless of its declared type.
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).
> a TypeScript variable may in fact contain any value regardless of its declared type.
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).
TypeScript intentionally strikes a balance between strict soundness and developer productivity, and I've personally been pretty happy with that balance. There's more to language design than soundness, and I've been happy with TypeScript's willingness to get out of my way for little snippets of unsafe code, especially when interfacing with external libraries. Within my own code, I've never had the unsoundness actually cause problems.
Hear, Hear. At the same time, Typescript's type system is getting so complicated, and the syntax so fugly because of it, that I'm tempted to go back to straight ES6.
I love Rust but its type system isn't necessarily good at modelling zero-cost abstractions. After all, one of its nicest abstractions is the iterator interface, and that is by no means "naturally" zero-cost - you really have to trust the compiler to optimize the code back into a regular loop, and even though it's pretty good at that, it isn't perfect.
TypeScript, while interesting, isn't so great if you're coming from an expression based language (i.e. where everything is a value).
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.
As someone who loves JS, your post sort of made me more comfortable with WASM as a competitor. JS is currently under seige by competing factions of OOP and FP that are constantly at odds with one another. Perhaps if these two groups had the WASM bone thrown to them, they'd leave TC39 the hell alone and let actual JS devs develop the language in its own right.
At an absolute minimum I'd want support for non-structural types and sound variance of collections; typescript also lacks real support for sum types. Honestly these days I probably wouldn't bother with a language without higher-kinded types - once you think in them it becomes very tedious to be repeating the same code over and over because your language can't express the types the code actually is.
(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)
My impression with Scala.js is that it's nice (and maybe the best option going at the moment) but you're still kind of a second-class citizen, which I'm hoping WASM will change. I imagine the experience with BuckleScript would be similar. (Whereas Typescript feels a lot more first-class, but at the cost of having to still be semantically very close to Javascript).
I am looking into TypeScript right now and I think it's just a hard problem to integrate a typed language into a dynamic environment like JavaScript. The transitions between JavaScript and the typed language will always be tricky and error prone.
PureScript doesn't do a bad job either. And even Haskell (GHCJS) has good FFI into JavaScript (I'd argue even better than PureScript!). How bad can you make interop between a higher-level language and JS? What are the bad examples?
