8 ms·

I think we need new, better concepts to judge type systems by. Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property

• xixixao 6y ago
  I think TS had better tooling and implementation. Flow continues to improve and had some better design decisions early on. Flow has focused on internal FB needs over open source needs. All in all, I think the soundness is not a negative / defining character and Flow could still gain in popularity, especially for projects closer in requirements to FB’s codebase.
  • lhorie 6y ago
    We use flow extensively at work (we have a monorepo w/ some 400 projects in them). `ag FlowFixMe | wc -l` gives me almost ten thousand hits. Which means that in practice, there's a lot of unsoundness going on even if one chooses to use flow over TS. A lot of people at work dislike flow because while it is generally sounder than TS, it throws some really stupid "errors" (e.g. Array prototype.filter doesn't refine arrays of nullables, it can't tell property access isn't a getter w/ side effects so it errs on the side of assuming it always is, etc). Typescript simply draws the line in the sand clearly from the beginning so that its scope as a project stays well defined and it doesn't end up accidentally falling into obscure gaps like flow.
    • yen223 6y ago
      Flow also used a ton of memory, and would crash pretty frequently with really bizarre errors, at least back when I had to work with it 2 years ago.
• diob 6y ago
  That last sentence really resonated with my Ruby experience. After using typescript for a few years, it feels like stepping back to JavaScript development in 2012.
• chrismorgan 6y ago
  TypeScript and Flow exist on top of JavaScript; given JavaScript (the language and ecosystem), an unsound type system is pragmatic, and a sound type system sometimes inconvenient. It is not obviously correct to generalise that property of soundness making life hard to other languages that are designed from scratch. (I think it is unwise to so generalise, but opinions may easily differ; my point is purely that the generalisation is not manifestly correct.)
• username90 6y ago
  I think that having a compromise between types and untyped is best. So first, have a type all other types can be cast to, call it object and allow it to perform generic operations. Then have a type that can be cast to all other types, call it null. These two gives you a lot of the nice parts of untyped languages while still allowing for tooling like quick refactoring or name completions. When I code in a system lacking any of these I feel way slower.
  • yoneda 6y ago
    On the contrary, I find myself more productive in languages that do not have pervasive null because then I don't have to manually reason about which values might be null.
    • username90 6y ago
      People build huge programs in untyped languages, reasoning about null is trivial in comparison. The cost of not having null is that all initialization and generic code gets much harder to write and work with, the benefit is that once in a blue moon you get a hard to debug null pointer error. I've worked as a software engineer at large companies for years and never had a hard to debug null pointer error, so at least to me they don't exist. Edit: I feel the main problem with over engineered type systems is the same as for any over engineered library. Instead of just cleanly solving a few key issues they recreate a programming language in their types and even worse they force you to use said programming language if you want to code. The C# style type system has all guarantees I need with very few limitations, if I need more guarantees I'll just write them in code.
      • rowanG077 6y ago
        People also used to build huge castles without any power tools. That something can be done with a tool is not an argument for that tool to be efficient or even good at it.
        • username90 6y ago
• KMag 6y ago
  Ideally, we'd have different strictness subsets of a single language, a generalization of JavaScript's strict mode. In a REPL, you'd want the type system to warn you of provable mistakes ("x will always be an int here, but you're array indexing on it" type things) but still let you make them, as you're often in the middle of breaking compatibility. In a library packed up for a package manager, you'd want strictness dialed up quite a bit, probably enforcing soundness. For something security-critical like a TLS implementation, you'd want very pedantic type checking. Libraries used across or between large organizations are often used in contexts unexpected or at least incompletely understood by the libraries' authors, and are therefore much more likely to encounter inputs that violate implicit assumptions made by the library authors. The more remote and varied the contexts in which a library is used, the more you'd want to force these assumptions to be made explicit in the library's interface. The strictness isn't one-dimensional, either. For instance, in a CRUD webapp, you'd probably want an effects system in your type system capable of expressing which inputs are un-vetted untrusted inputs (similar to Perl's taint mode), but you might or might not want other effects to be enforced by the type system.
• dwhitney 6y ago
  I need to write a blog entry titled, "Your test suite is basically a sh*tty type system." -- I'm in the "totally anal" camp of type system aficionados :)
  • bottled_poe 6y ago
    I like it, but try convincing the client that we don’t need to test the software :)
    • dtwhitney 6y ago
      Do you take me for a fool, sir? I know this can't be done.
  • wutbrodo 6y ago
    The earliest example of a remedy for impostor syndrome was during the second year of my professional life, seeing someone on HN say sithour much pushback that "types are superfluous, because you should be writing good unit tests" with reference to engineering systems written in Python. I still think about it sometimes.
  • seanmcdirmid 6y ago
    Or the converse “your type system is basically a very limited test suite.” Seriously though, these two concepts have some overlap that should be explored more.
    • uyt 6y ago
      Whenever I do leetcode, I use python. This is because most of the constraints that are useful to check in an algorithm can't be encoded as types. Instead I sprinkle a lot of asserts (possibly using slower bruteforce version of the code) to check invariants and properties that I expect to be true. I think dependent types is supposed to solve this problem (for example, rather than just a list of ints, it can encode that it's currently a sorted list of ints) but they don't seem practical to use at the moment.
    • 6y ago
• lmm 6y ago
  > Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Only if that crowd has never used a good typed language, IME. I spent two weeks trying to get things done in TypeScript and then two days writing them in Scala.js. It's amazing how much of a productivity drag it is when you can't quite trust your types, but you'd never know that if you've not used an ML-family language. > So what if the type checker can infloop? It won't in practice. It absolutely will, and it's a massive pain when it does. You type something in your IDE and your error squiggles don't update, maybe (if you're lucky) you get a warning that compilation is taking a long time. It's very hard to distinguish between "it's just being slow" and "it's gone into an infinite loop".
  • refenestrator 6y ago
    Consider that you might be the weirdo here. Kotlin is eating scala's lunch by specifically jettisoning the advanced type stuff. If you can give 80% of the value with 20% of the confusion, that's a win for most devs.
    • lmm 6y ago
      Kotlin is eating Scala's hype by hyping how much better their ad-hoc informally-specified implementation of half the advanced type stuff is. Having had to actually debug errors from their "suspend functions", "platform types" and goodness knows what else, there's nothing simpler about it.
      • KMag 6y ago
        I think optimally, you have a powerful effect and dependent linear type system with adjustable strictness of checking. You'd use the very weakest level for a REPL : warn if there is no set of types that allows a function to execute without throwing a runtime type error. Most applications would be run/compiled with stricter checking. Libraries packed up for package managers would presumably be checked with full effects checking and without implicit soundness escape hatches of the kind you get in TypedScript. Security-critical libraries, such as TLS implementations, would hopefully be compiled to make full use of dependent types. Hopefully you'd also have a lifetime system integrated with the malloc implementation. Your malloc implementation needs at a minimum a size_t header on each allocation, and you could use this similarly to how OpenJDK / Oracle's JVM lazily allocates rwlocks by "promoting" the object header's GC word to a tagged pointer to an rwlock and a copy of the original GC word. In this case, you'd probably use 2 bits of the malloc header for tagging, limiting arrays and other large objects to a maximum of 1 GB in 32-bit processes. Code for which lifetimes checked properly would completely ignore the dynamic lifetime accounting, but any code that didn't check properly would need to pass around potentially unsafe references as "fat references" as a pair of reference and rwlock. The first time an object reference hit potentially unsafe usage, its malloc header would need to be inflated to a pointer to the original size_t allocation_size and the rwlock, so that the "fat reference" could safely be made skinny and fat again as it passed between lifetime-safe and lifetime-unsafe libraries. Unfortunately for Rust-like systems that have both atomic and non-atomic reference counting, I think this means having the dynamic library headers contain a list of offsets of the non-atomic reference count operations so they can be dynamically patched if lifetime-unsafe code is ever loaded. (Or, make the safe libraries twice as big and modify the program linkage table and patch up all return addresses on stacks the first time any lifetime-unsafe code is loaded.) The two bits for tagging the size_t allocation_size in the malloc implementation would be one bit for tagging if it was a size_t or a *struct {size_t allocation_size; size_t rwlock;} The other bit would be a "one bit reference count" for optimizing the common case where there's at most one reference to the object. Edit: actually, the mixing of lifetime-safe and lifetime-unsafe code falls down for statically compiled systems that allow references into the middle of objects. IBM's OS/400's (i5/OS's) Technology Independent Machine Interface (TIMI) uses 128-bit pointers for everything, so maybe it's not so bad to make all references "fat references", and optimize them to regular references when escape analysis shows they will never leave lifetime-safe libraries. In any case, it's more complicated than I originally thought to efficiently mix dynamic race condition detection along with compile time elision via Rust-like compile-time borrow checking. You could use an atomic hash map to keep track of locations of the rwlocks in order to inflate thin references to fat references every time lifetime-unsafe code gets a reference from lifetime-safe code, but all of those lookups sound prohibitively expensive.
• scubbo 6y ago
  > infloop I had never seen this word before, and while I assume it's probably short for "infinite loop", I initially parsed it as "in-floop", as opposed to "out-floop".
  • skrebbel 6y ago
    Yep, correct! Thanks :-) Btw i love "out-floop" and I'm going to try to find applications for it.
    • scubbo 6y ago
      Perhaps via reference to https://en.wikipedia.org/wiki/BlooP_and_FlooP https://en.wikipedia.org/wiki/BlooP_and_FlooP ? EDIT: though, in that context, I would parse "out-floop" as a transitive verb meaning "to FlooP more, to a greater extent, or faster, than <something else>", rendering its opposite actually "under-floop".
      • skrebbel 6y ago
        "He out-flooped the infloop with bloop" (which would be pretty impressive)
• jbluepolarbear 6y ago
  Typescript taught me that I actually don’t care about types and all I care about is the shape of data. In most cases I think of types/interfaces in Typescript as strict data definitions. A function takes in a collection of data; as long as the data matches the shape I expect, don’t care what the data represents.
  • leafario2 6y ago
    That's exactly what types are for dude
  • adwn 6y ago
    > Typescript taught me that I actually don’t care about types and all I care about is the shape of data. Seconding leafario2 here, that's exactly what types do: They give guarantees about the shape of data. Maybe what you meant was you don't care whether an object is of type Customer or Supplier, as long as it has an element/field named address. That's called "structural typing" (as opposed to "nominal typing"). Few static type systems have structural typing, probably because in practice, you actually do care whether the object is a Customer or a Supplier, even if their fields have the same names. Rust, for example, is nominally typed, but you can define a trait "HasAddress" with a trait function "fn address(&self) -> &str" and implement it for Customer and Supplier, to simulate structural typing where you need it.
    • jbluepolarbear 6y ago
      I don’t know if I do care that customer is or isn’t a supplier. I have been using Nominal type systems in C++ and C# for a long time and I’ve started drifting into an architecture style that leverages interfaces as my types which I just learned is structural typing. I really liked the concept in Golang and then I really started using it in TypeScript and got hooked. It makes so many programming problems easier to implement, maintain, and understand. I now mix and match nominal and structural types in my projects, using them where they best fit.
  • seanmcdirmid 6y ago
    What you use the word “type” for is a nominal type and your shapes are structural types. The utility and different trade offs between nominal and structural types were explored a lot back in the 90s.
• benjaminjackman 6y ago
  FWIW I think the core devs of Typescript would disagree with you on the characterization that they were in any way attempting to show a large crowd "that soundness isn't an important property." I just say that because such had been my view of the language as well (pragmatism & productivity over type-system strictness) until I had a feature request rejected on soundness grounds a few days ago.
• nathias 6y ago
  TypeScript has shown me that I hate TypeScript.
• inbx0 6y ago
  I've used both Flow and TS, and we are currently using Flow. I disagree with the notion that Flow's lack of success is due to differences in soundness. Today, I think Flow's exact-by-default object types are the biggest selling point for it and it catches real mistakes that I sometimes make when I'm using TypeScript. What made Flow fail in terms of popularity is that it lagged so far behind in editor support, the openness of development (what's a roadmap?), performance, and just overall usability and utility. They have since picked up on performance and added some features that - you know - actually leverage the types to help you write code. Autocompleting property types works at least half the time. There are some very simple refactorings available. We are _finally_ getting autoimports. But it's too little too late, when you use TS for a while you notice that the refactoring tools are like from some other planet than those in Flow, and then coming back to Flow and, say, rewriting imports by hand feels like coming back to stone age. Even worse, it's a self-perpetuating cycle, because the community has overwhelmingly settled behind TS and created these amazing tools to complement it, while Flow is left as a niche at Facebook's mercy. I look at projects like ESBuild or Prisma with envy. At the end of the day, Flow feels like it was never meant to actually compete with TypeScript. It's Facebook's internal development tool that you are free to use if your priorities happen to align with Facebook's.
  • eyko 6y ago
    I've also used both Flow and TS and love Flow, but the tooling and community in TypeScript is in a different league. Right now I feel like picking Flow over TypeScript on anything other than personal or individual projects is a disservice to your team. It's very much reminiscent of the Beta vs VHS format wars.
• gurkendoktor 6y ago
  > And I don't even see how "decideable" is a desireable property at all. So what if the type checker can infloop? It won't in practice. I am not so optimistic after having worked with Swift, where simple arithmetic expressions and array literals can bring the compiler to its knees: https://twitter.com/steipete/status/1361596975150493700 https://twitter.com/steipete/status/1361596975150493700 (As noted in a reply, this particular bug has been fixed...but still.)
• Person5478 6y ago
  > Eg TypeScript has convincingly shown to a large crowd that soundness isn't an important property for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Typescripts goal was to interoperate with existing javascript in an easy manner, and doing so forced them to relax the type system in specific ways. It turns out more typing is better than less typing so typescript > javascript. That doesn't mean something with stronger typing than typescript isn't strictly better in all of the facets you mentioned, just that typescript made that particular tradeoff and had MS behind it.