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 for many key goals of static typing, such as programmer productivity, refactoring support, preventing stupid mistakes and navigating large codebases. Soundness was Flow's big claim to fame and it just made day to day programming harder with mostly academic/cosmetic benefits. I'm sure that there's more reasons why TS won the popularity contest, but TS's pragmatic forgiveness surely played a part.
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.
At the same time, most people will agree that eg Go's type system is very different from Idris's. They have very different pros and cons, both in terms of how hard they are to typecheck and how great they are to use. In fact I can't think two somewhat popular type systems that could be more different from one another, but if you only read this page you might think they're comparable.
We need words for "totally anal" and "basically Ruby but some typos are caught" and everything in-between.
> 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".
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.)
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.
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 :)
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.
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".
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.
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.
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.
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.
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.
> The knowledge of the compiler in a statically typed language can be used in a number of ways, and improving performance is one of them. It’s one of the least important, though, and one of the least interesting.
Erm... no. I don't mean to invalidate the whole article from just this quote, but it's this kind of thinking is what makes today's applications slow, from browsers to office suites and web-sites. Wasting computing resources because you can, is a lazy way of thinking about development in my opinion.
> A decision problem is decidable if for any input we can compute whether the input satifies the problem in finite time. Examples of decidable problems include primality testing and boolean satisfiability. The halting problem for example is undecidable: We cannot check whether a program runs infinitely long in finite time.
This isn't important for type systems though. Any undecidable type system can trivially be made decidable by putting a cap on how many instructions you can run when evaluating the type. Such limitations works really well in practice since useful types takes relatively little to evaluate, and you can put it as a compiler option in the few edge cases where someone needs a huge complicated type that goes above the cap.
I guess, unsoundness sounds concerning.
But is undecidability? When this is an issue, it's always because someone worked to do some really elaborate or general compile-time computation. It seems a lot (literally too much) to ask that you can do really unrestrained type-level computation and also still always have termination.
To me, unsoundness doesn't sound too concerning. It is a theoretical property, and when programming I care about practice, which means that I care about consistency and predictability. If a type system is unsound because of certain edge cases, but works well in practice and those edge cases case an error later anyways, I don't care too much. I mean, most typed languages will have casting operators that can make unsafe operations precisely because programmers sometimes want to bypass the type system. Why sacrifice usability in the name of 'soundness' when in practice people are just going to bypass the type system when that happens?
I think this is an important point to focus on when writing a new type-safe language. LEAN for example has a very impressive type system (honestly seems like magic sometimes), and clearly all of the "impossibility" is shoved into the computational complexity of the type-checker.
Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.
I agree. If undecidability (or some stricter but still off-putting set)in a given language means an extremely complicated compiler that would be a mark against it, but if it's just an obscure edge case or something that is already not possible in a normal language, then I really don't care.
I would, however, like to see termination analysis applied to code more often - e.g. rather like only accepting a pure function in an interface, this function must terminate but might not be pure.
To your point, the example of Idris is sound and decidable, but in practice the decidability doesn't matter: you add fuel[1] to limit recursion, but it can just be some arbitrarily large number (but not infinite) number of loops.
Java's type system is actually unsound if you include checked exceptions as part of the type system. By using generics, you can write ExceptionUtils.rethrow[1] in Java[2]. I think that this should count as true type unsoundness because unlike type casts, you aren't relying on some explicit runtime check and because checked exceptions are essentially a subset algebraic effects. In practice, rethrow can be convenient if you are already catching everything anyway or if some library is overusing checked exceptions.
> Where are Python, Bash, etc.? [...] While there exist extensions to some dynamic languages imbuing them with static type checking these are not part of the language, and the complexity depends not on the language but the extension.
But TypeScript is included. Isn’t it an extension to JavaScript in the same way that Mypy is an extension to Python?
Is there a technical difference that justifies one being included and the other not, or is it just a case of popularity?
I think it’s an important difference: TypeScript is a language that has a typechecker bundled with it. The language and the typechecker are clearly connected, and TypeScript users are very very strongly encouraged to use the typechecker on all typescript code. Type checking is also implicitly described as a language feature.
Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any other SA tool.
Most comments here are asking guarantees from type checkers that actually belong to semantic analysis and static analysis in general but not necessarily related to type checking.
Type checking is not the only conceivable way of achieving those guarantees, but it's effective and at least somewhat understood by most working programmers, so why do something different for the sake of it?
FWIW, most (arguably any/all) non-dependently-typed languages would let that slide, as [] is of type "array of (at best) X (which could be inferred as number by working backwards from the declaration)" and one of the operations you can do on an array is to index it, by a (maybe unsigned) integer, with 0 (either way) thereby being a valid index. For this to fail, in addition to the type of the array being parameterized by its size (which is at least not too uncommon if not exactly common) the type of that index operator has to be (more notably) at least parameterized by the concrete value 0 if not the abstract expression 0 (which would let you use a proof assistant to verify it for non-constant cases).
I think I remember reading that Scala 3.0 introduced some backwards incompatibility in order to make the type system sound. Anybody aware of what had to change?
Check out Dotty and some of the papers on DOT calculus. Sorry, on mobile or I'd link you. Scala 3 has some different fundamentals. I don't think it's all the way sound like idris, but there's a lot of new rules underneath the hood to have types be much safer.
I hate Scala, but I gotta admit the future of it looks a little promising if they nail the transition
Static typing is a learning tool for junior level developers. Like training wheels on a bike.
After 10 years or so of programming experience, the training wheels need to come off.
People's attitude towards static vs dynamic typing would make a great topic for interview questions to weed out junior devs.
Senior recruiter: "How do you feel about TypeScript?"
Candidate: "I like it. It helps ensure that I don't accidentally pass the wrong type of instances to functions... Which is a very big problem for me and the people I usually work with."
Senior recruiter: "Thank you for your time... We'll be in touch..."
... Candidate walks out the door.
Recruiter: "That's a definite no... This candidate is the Neglectful type (pun intended)"
Junior recruiter: "Could have fooled me! Too bad there are no automatic candidate type checkers for us junior recruiters... That would be the greatest thing since adult diapers."
... Both recruiters break into laughter while watching their email inboxes struggle to render the massive, never-ending flow of new resumes.
[+] [-] skrebbel|5 years ago|reply
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.
At the same time, most people will agree that eg Go's type system is very different from Idris's. They have very different pros and cons, both in terms of how hard they are to typecheck and how great they are to use. In fact I can't think two somewhat popular type systems that could be more different from one another, but if you only read this page you might think they're comparable.
We need words for "totally anal" and "basically Ruby but some typos are caught" and everything in-between.
[+] [-] lmm|5 years ago|reply
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".
[+] [-] chrismorgan|5 years ago|reply
[+] [-] inbx0|5 years ago|reply
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.
[+] [-] dwhitney|5 years ago|reply
[+] [-] KMag|5 years ago|reply
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.
[+] [-] scubbo|5 years ago|reply
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".
[+] [-] jbluepolarbear|5 years ago|reply
[+] [-] benjaminjackman|5 years ago|reply
[+] [-] xixixao|5 years ago|reply
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.
[+] [-] diob|5 years ago|reply
[+] [-] gurkendoktor|5 years ago|reply
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
(As noted in a reply, this particular bug has been fixed...but still.)
[+] [-] username90|5 years ago|reply
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.
[+] [-] nathias|5 years ago|reply
[+] [-] Person5478|5 years ago|reply
[deleted]
[+] [-] whoisburbansky|5 years ago|reply
[+] [-] daurnimator|5 years ago|reply
> undecidable, since evaluation of recursive functions at compile time is possible, thus requiring the compiler to solve the halting problem.
Zig's comptime is limited to the number of backwards branches you allow, see https://ziglang.org/documentation/master/#setEvalBranchQuota
[+] [-] steerablesafe|5 years ago|reply
[+] [-] Chris_Newton|5 years ago|reply
https://cdsmith.wordpress.com/2011/01/09/an-old-article-i-wr...
It’s one of those older articles where not everyone will agree with everything, but there’s still a lot of insight and food for thought.
[+] [-] mariusor|5 years ago|reply
Erm... no. I don't mean to invalidate the whole article from just this quote, but it's this kind of thinking is what makes today's applications slow, from browsers to office suites and web-sites. Wasting computing resources because you can, is a lazy way of thinking about development in my opinion.
[+] [-] username90|5 years ago|reply
This isn't important for type systems though. Any undecidable type system can trivially be made decidable by putting a cap on how many instructions you can run when evaluating the type. Such limitations works really well in practice since useful types takes relatively little to evaluate, and you can put it as a compiler option in the few edge cases where someone needs a huge complicated type that goes above the cap.
[+] [-] rowanG077|5 years ago|reply
[+] [-] abeppu|5 years ago|reply
[+] [-] gjulianm|5 years ago|reply
[+] [-] enricozb|5 years ago|reply
Despite the fact that some of the languages listed here have undecidable type systems, it doesn't feel like many common-purpose languages have purposefully gone down the undecidable route to bring some really cool type-safety.
[+] [-] mhh__|5 years ago|reply
I would, however, like to see termination analysis applied to code more often - e.g. rather like only accepting a pure function in an interface, this function must terminate but might not be pure.
[+] [-] habitue|5 years ago|reply
[1] https://www.idris-lang.org/docs/current/contrib_doc/docs/Dat...
[+] [-] slaymaker1907|5 years ago|reply
[1]: https://commons.apache.org/proper/commons-lang/apidocs/org/a... [2]: https://www.baeldung.com/java-sneaky-throws#:~:text=In%20Jav....
[+] [-] pansa2|5 years ago|reply
But TypeScript is included. Isn’t it an extension to JavaScript in the same way that Mypy is an extension to Python?
Is there a technical difference that justifies one being included and the other not, or is it just a case of popularity?
[+] [-] muglug|5 years ago|reply
Python has no bundled typechecker, and its authors do not insist users use MyPy, Pyre or any other SA tool.
[+] [-] rsrsrs86|5 years ago|reply
[+] [-] lmm|5 years ago|reply
[+] [-] dwhitney|5 years ago|reply
const num: number = [][0]
[+] [-] saurik|5 years ago|reply
[+] [-] panzerklein|5 years ago|reply
[+] [-] smlckz|5 years ago|reply
[1]: http://jsfuck.com
[+] [-] quickthrower2|5 years ago|reply
[+] [-] mastrsushi|5 years ago|reply
Do they mean as opposed to the type check system failing with the wrong data type detected?
[+] [-] yen223|5 years ago|reply
A typechecker that is "sound" will always reject incorrectly-typed programs, but it may reject some correctly-typed programs.
[+] [-] phs|5 years ago|reply
[+] [-] darksaints|5 years ago|reply
[+] [-] adenozine|5 years ago|reply
I hate Scala, but I gotta admit the future of it looks a little promising if they nail the transition
[+] [-] booky2|5 years ago|reply
[+] [-] elwell|5 years ago|reply
[+] [-] unknown|5 years ago|reply
[deleted]
[+] [-] cryptica|5 years ago|reply
Senior recruiter: "How do you feel about TypeScript?"
Candidate: "I like it. It helps ensure that I don't accidentally pass the wrong type of instances to functions... Which is a very big problem for me and the people I usually work with."
Senior recruiter: "Thank you for your time... We'll be in touch..."
... Candidate walks out the door.
Recruiter: "That's a definite no... This candidate is the Neglectful type (pun intended)"
Junior recruiter: "Could have fooled me! Too bad there are no automatic candidate type checkers for us junior recruiters... That would be the greatest thing since adult diapers."
... Both recruiters break into laughter while watching their email inboxes struggle to render the massive, never-ending flow of new resumes.
[+] [-] madeofpalk|5 years ago|reply
[+] [-] clownpenis_fart|5 years ago|reply