4 ms·
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 f
by Too 9y ago
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.
- wereHamster 9y agoAny 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.
- alangpierce 9y agoWhen 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.
- catnaroek 9y agoIt is good at neither. Union types and sum types are veeery different from each other.
- alangpierce 9y agoTo 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. [1] https://www.typescriptlang.org/docs/handbook/advanced-types.html#discriminated-unions https://www.typescriptlang.org/docs/handbook/advanced-types.... [2] https://en.wikipedia.org/wiki/Tagged_union https://en.wikipedia.org/wiki/Tagged_union
- catnaroek 9y ago> My understanding is that "tagged unions" and "sum types" are the same thing Well, your understanding is wrong. Sum types satisfy a specific universal property, which union types don't.
- dhucerbin 9y agoWhat specific universal property?
- catnaroek 9y agoThe 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.
- alangpierce 9y agoInteresting, 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. https://www.typescriptlang.org/play/index.html#src=type%20A%20%3D%20%7BnumValue%3A%20number%7D%3B%0D%0Atype%20B%20%3D%20%7BstrValue%3A%20string%7D%3B%0D%0Atype%20Sum%20%3D%20%7Btype%3A%20'A'%2C%20a%3A%20A%7D%20%7C%20%7Btype%3A%20'B'%2C%20b%3A%20B%7D%3B%0D%0A%0D%0Afunction%20foo%3CX%3E(f%3A%20(s%3A%20Sum)%20%3D%3E%20X)%3A%20%5B(a%3A%20A)%20%3D%3E%20X%2C%20(b%3A%20B)%20%3D%3E%20X%5D%20%7B%0D%0A%20%20return%20%5B%0D%0A%20%20%20%20(a%3A%20A)%3A%20X%20%3D%3E%20f(%7Btype%3A%20'A'%2C%20a%7D)%2C%0D%0A%20%20%20%20(b%3A%20B)%3A%20X%20%3D%3E%20f(%7Btype%3A%20'B'%2C%20b%7D)%2C%0D%0A%20%20%5D%3B%0D%0A%7D%0D%0A%0D%0Afunction%20bar%3CX%3E(fa%3A%20(a%3A%20A)%20%3D%3E%20X%2C%20fb%3A%20(b%3A%20B)%20%3D%3E%20X)%3A%20(s%3A%20Sum)%20%3D%3E%20X%20%7B%0D%0A%20%20return%20(s%3A%20Sum)%3A%20X%20%3D%3E%20%7B%0D%0A%20%20%20%20if%20(s.type%20%3D%3D%3D%20'A')%20%7B%0D%0A%20%20%20%20%20%20return%20fa(s.a)%3B%0D%0A%20%20%20%20%7D%20else%20%7B%0D%0A%20%20%20%20%20%20return%20fb(s.b)%3B%0D%0A%20%20%20%20%7D%0D%0A%20%20%7D%3B%0D%0A%7D%0D%0A https://www.typescriptlang.org/play/index.html#src=type%20A%...
- devit 9y agoIt'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).
- wereHamster 9y ago> 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).
- devit 9y agoYeah but in Rust and Haskell it's isolated to clearly marked code (except for some minor bugs in Rust that will be fixed - see https://github.com/rust-lang/rust/issues?utf8=%E2%9C%93&q=is%3Aissue+label%3AI-unsound+is%3Aopen https://github.com/rust-lang/rust/issues?utf8=%E2%9C%93&q=is... ). 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 https://github.com/Microsoft/TypeScript/issues/9825 ).
- alangpierce 9y agoTypeScript 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.
- skolemtotem 9y ago
- masklinn 9y ago> 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 MLs (OCaml, F#, Reason) are hardly "extreme functional spectrum".
- lmm 9y agoAt 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)
- virtualwhys 9y agoTypeScript, 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.
- rmrfrmrf 9y agoAs 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.