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".
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.
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.
Sounds overcomplicated. I've seen any number of fancy not-exactly-type-systems and they always end up having crazy edge cases, whereas a plain type system does exactly what you expected (and, crucially, does it in an understandable way) and scales arbitrarily far. Having the type system work the same way in the REPL and the rest of the language is important for that.
I guess then you'd need another mechanism for dealing with re-defining APIs in incompatible ways within the REPL. It's a pretty common use case for REPLs to play around with APIs and temporarily break them.
The best alternative is to keep a map of all of the definitions with broken type checks, and refuse to generate new machine code/bytecode as long as that map is non-empty, and keep using the older definitions until again get back to a sound state of the world.
GHC's REPL supports turning type errors into crashes when the ill-typed expression is used, which lets you test one part of code while another part is broken.
I think you can even extend that to compiled code, for an authentic "it crashed in production" experience.
Slightly off-topic, but say I know Python and JavaScript and I wanted to add a multi-paradigm language with strong typing to my toolbelt. I'm looking for something with a strong functional programming core but with object-oriented facilities as an "escape hatch".
The languages I've been eye-balling are Scala, Kotlin and F# (I'm separately eyeing Elixir, but since it's dynamic, I'd leave it out of this particular discussion)
My main requirements are that it's a "builder's language" with a great ecosystem for web development and growing mainstream adoption. I'm a general-purpose product engineer building apps end-to-end, and I favor general ergonomics and ease of use over other characteristics (performance, functional purity, etc.)
I'm assuming from your comment you've tried both Scala and Kotlin and favor the later - would you bet on it knowing the above?
> Slightly off-topic, but say I know Python and JavaScript and I wanted to add a multi-paradigm language with strong typing to my toolbelt. I'm looking for something with a strong functional programming core but with object-oriented facilities as an "escape hatch".
If you're looking for a language that will let you keep writing Python/Javascript in that language, you'll find it, but you won't learn anything from the experience. You won't appreciate the benefits of those type systems unless you really commit to them. (I actually learnt Standard ML first, and it made me a better Python programmer; I imagine Haskell would have a similar effect). If you're looking for "languages in my toolbelt" you'll end up "knowing" a dozen languages but coding the same way in all of them, which is useful in some ways but ultimately limiting. What's your actual goal here - e.g. are you trying to learn more languages so you can get a better job?
> My main requirements are that it's a "builder's language" with a great ecosystem for web development and growing mainstream adoption. I'm a general-purpose product engineer building apps end-to-end, and I favor general ergonomics and ease of use over other characteristics (performance, functional purity, etc.)
If by "growing" you mean you want a language on the left hand side of the hype cycle, then Kotlin is what you want. If by ease of use you mean easy to write, Kotlin will serve you well - it has that Perl-like feel of it does what you want, unless you want consistency. I pity anyone who has to maintain a Kotlin app in 5 years' time, but it sounds like it'll do what you want it to.
> What's your actual goal here - e.g. are you trying to learn more languages so you can get a better job?
Not as an end by itself, no; I want to learn more languages out of sheer intellectual curiosity, but most of all because I like building things, requirements vary by project, and I believe that it's good to have different tools to tackle them.
I work primarily in JavaScript and Python, but academically I've had rigorous exposure to C, Java and OCaml, and a few other languages to a lesser extent. I appreciate the benefits of dynamic languages but I sometimes miss the confidence and expressiveness of strong types.
My process to learn a language nowadays is to build a project with a large enough scope, solving a real problem (generally, a web app that I or someone very close would use). That way I keep motivation high and get exposed to a non-negligible surface area of the language and tools involved.
That's why I ask for advice on what to learn next - because I make a somewhat sizeable investment and I don't have the time to repeat the process that many times over the course of a year. Over the long run, I may have time to try all the things listed (and more!) but even then the question of sequencing (which one first?) is interesting to me... I'm young and healthy but I may not be alive in six months time.
> If by "growing" you mean you want a language on the left hand side of the hype cycle
Not necessarily growing as in the left side of the hype cycle, but in that it will likely continue having a vibrant ecosystem in 5-10 years time.
> Kotlin will serve you well - it has that Perl-like feel of it does what you want, unless you want consistency. I pity anyone who has to maintain a Kotlin app in 5 years' time, but it sounds like it'll do what you want it to.
Maintanability would be something I would certainly look for in a strongly typed language!
> Not as an end by itself, no; I want to learn more languages out of sheer intellectual curiosity, but most of all because I like building things, requirements vary by project, and I believe that it's good to have different tools to tackle them.
> I work primarily in JavaScript and Python, but academically I've had rigorous exposure to C, Java and OCaml, and a few other languages to a lesser extent. I appreciate the benefits of dynamic languages but I sometimes miss the confidence and expressiveness of strong types.
If you've actually made serious use of OCaml then I wouldn't bother with any of the languages on your list - they're very much the same paradigms as OCaml (similar to how I wouldn't advise someone to learn both Ruby and Python - it's not that there aren't differences between them, but those differences aren't mind-expanding if you see what I mean). If you're talking about "a multi-paradigm language with strong typing to my toolbelt" then isn't OCaml already that? So I'd say Elixir is a better bet from that perspective - I'm no fan of the language, but it does something that none of the other languages you've talked about does. (Well, there is an actor implementation for Scala, but IME it's in an awkward tension with the rest of the language - kind of like the OCaml object system in that respect).
> Not necessarily growing as in the left side of the hype cycle, but in that it will likely continue having a vibrant ecosystem in 5-10 years time.
Scala is not growing fast, but it's mature and stable in a way that Kotlin isn't yet; I genuinely have more confidence in Scala being usable in 5-10 years' time, though that may be my biases showing. I'd say the same thing but to a lesser extent with F# - the whole .net ecosystem is kind of a parallel world from the big contiguous dev community, and the move to .net core is a big disruption at a time when F# is always going to be a lower priority than C#. (Of course the JVM looked equally rocky for a while, but it feels like the community has coalesced smoothly around AdoptOpenJDK now).
I also predominantly use python and JavaScript professionally, but have written a lot of Haskell, and a bit of go, rust and others.
I love haskell and GHC but it's not a builder's language. That's not to say it can't be used in production, the language is very powerful, easy to refactor, performs well and is hard to make mistakes in. Some of the tooling like QuickCheck, STM and lenses are decades beyond other ecosystems whereas simple things like logging are hard and debuggers/autoformatters/IDE tooling are less polished than their counterparts in mainstream language. I have both Haskell and Django web applications in production and it pains me to say that python is a lot more convenient and easier to iterate on.
Finally, in answer to your question I would recommend rust. It is a rising star with a decent type-system derived from ML languages. I would also characterise the language and it's ecosystem as being focused on building production software. As an added bonus it integrates well with python and JavaScript applications, and is a useful tool to have for optimising expensive algorithms.
Kotlin's a good bet with your requirements. You could also consider C# (not as new and cool, but still adding more features, and particularly well-designed language) and Rust (admittedly a little harder to use, but excellent multi-paradigm support and a strong web ecosystem).
Kotlin has lots of type anomalies if you peruse the official discussion fora. For example, you can write a pure Kotlin program, which compiles without (type) warning/error, that throws an NPE without using casting.
Overall I prefer Kotlin to Scala as I really disliked Scala's implicits.
But I'm not convinced that Kotlin's type system is that much simpler than Scala's when you think of the interactions between various features like smart casting.
It certainly doesn't seem to compile any faster - I have a 2020 quad-core i7 laptop and at best I'm seeing is compile times in the range of a few hundred lines of code per second - and I suspect this is due to type inference rather than byte code generation. Both Kotlin and Scala represent a significant regression in this regard for me.
But Scala is, according to that list, just as undecidable and unsound as TypeScript. Are the places where you can't trust your types just more esoteric there?
It's practical to restrict yourself to a sound subset of Scala (the soundness issue they mention applies to a specific usage pattern that you can ban with a linter), and the issue is outright fixed in Scala 3.
The undecidability is real but you at least get what you're paying for - a certain amount of type-level programming is practical and useful in Scala. I'm not sure it's the right tradeoff but it's on (or at least close to) the Pareto frontier in a way that many languages aren't.
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'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.
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 :)
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.
> Or the converse “your type system is basically a very limited test suite.”
the converse doesn't hold. You can write new code that will benefit from the guarantees of existing types. But you'd have to write new tests if you didn't have types.
Not necessarily. If you add new code to the user signup (let's say some additional checks on the shape of their username) and the integration test for the happy path of a user signup still passes, the new code is absolutely covered by existing tests (though probably not completely, there are probably edge cases not covered).
The tests/types correspondence still holds: if you write new code, you will often also need to alter the types to correctly describe the changed domain. In the username example above, after adding username validation it would be a good idea to have a dedicated `Username` type that can only contain valid usernames instead of just stuffing everything into `String`. If you count extra time writing and refactoring tests after adding new code, you should also count the extra time writing and refactoring additional types after adding new code.
I think that’s where our experience with type systems could be used to improve our testing methodology and technology. Having the ability to reuse tests in client modules would effectively fix that gap (eg by generating fakes for the original modules from its tests).
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.
Rust made me realise the truth in this. Using a sound type system wisely removes a whole class of things that can go wrong.
It can be exhausting to use if you never learned how to use it, but if you got the hang of it, you can program more freely because reasoning about what is going wrong becomes easier.
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".
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".
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.
> 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.
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.
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.
Thanks, I don’t think I learned the about these concepts in college; granted, I dropped out because I am ADHD to the max. I usually adopt or adapt what I observe in others code, my old code, or idea from other fields entirely. I like to adapt and improve techniques I see and fit them best into my projects.
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.
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.
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.
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.
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.
When you have a hammer everything looks like a nail. A language theorist trying to fix issues will of course look at changing the language first, doesn't mean he is right.
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.
That is your opinion though, my opinion is that type systems stricter than C# detracts rather than adds and most agree with me. People who like to discuss language theory don't, of course, since the major reasons to discuss language theory is that the popular languages don't have the features you like or that you want to specifically solve software engineering problems in the language level rather than the code level.
It's not possible to solve problems at the code level. That would require every single developer writing in that language to account for all the holes in the type systems. That's completely unrealistic. And can be seen to be disastrous in practice. I mean just walk through some python code. There are almost no None or manual type checks. These are just bombs waiting to explode.
The problem with type systems like C# and Java are that they are too strict. Look at the polymorphism mess in those languages. The entire reason people hate static typing is because of the shittiness of precisely those two languages. That's the reason we need better type systems.
Each restriction at the language level adds a cost. The cost of having simple nullable types like you do in Java or C# is worth it. The cost of trying to formalize away null errors isn't. That is what I think. Just because you can do something doesn't mean that you should, so just because you can ensure no errors of class X happens at a language level doesn't mean that enforcing that at a language level is the best solution.
> It's not possible to solve problems at the code level. That would require every single developer writing in that language to account for all the holes in the type systems.
I'm not sure what you mean with this. Of course you can fix this at a code level. Not for the entire world of course, but you can do it in the code you write.
So? People build huge programs in typed languages as well. Whether people do something one way says nothing about how that approach compares to others.
> The cost of not having null is that all initialization and generic code gets much harder to write and work with
Could you provide examples of how lack of a null value makes these so much harder?
> the benefit is that once in a blue moon you get a hard to debug null pointer error
This is like saying that the only drawback to not having smart pointers in C++ is that once in a blue moon you get a hard to debug segfault. Sure, segfaults may be more common when working with raw pointers, but there are also substantial drawbacks in terms of mental overhead due to potential uncertainties about ownership/lifetimes.
In that vein, NPE/NREs are not the only drawback to a type system with null; the additional state space means mental overhead for the programmer and an increased risk of mistakes.
In addition, introducing universal nullability into a type system entails performance penalties. Null increases the state space of a given type, so if a type uses all of its bits (e.g., int) you need to introduce indirections (java.lang.Integer) or increase the size of the type (C# Nullable<int>/int?) to shoehorn in a null value.
> 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.
I'm not sure what you're trying to get at here. This seems to be a criticism of generics/similar mechanisms, but you seem to be fine with C#/similar type systems, which has generics and makes use of them?
What's especially confusing is that type systems with generics and null are precisely equivalent to type systems with generics without null, as all instances of nullable types can be replaced with Option<T>/Optional<T>/Nullable<T>/etc. (with appropriate sugar for other operations, of course). So I'm a little lost as to what the problem is.
> 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?
Soundness gives an important benefit: Performance, for a compiler capable of utilising the type information properly. It can omit run-time checks, and unbox primitives etc.
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.
Type annotations in recent 3.x releases though have made Python a much better language, and in practice the Jetbrains- (Pycharm-)-bundled type-checkers work very well. I'm much more comfortable recently working with larger codebases in Python and don't miss the C++/Java type constraints now.
Python has type annotations but no type checking. The type checker you use for Python may have different soundness/decidability versus other type checkers.
There's only one (official) TypeScript type checker, which works in only one way, and introduces both type annotations as well as syntax which compiles to JavaScript that's executed at runtime (enums, decorators).
It's not a difference in marketing. Types anotations are part of Python, but not of JavaScript. CPython will happily run a program with type anotations, V8 will fail to parse Typescript.
You could draw similarities with using Typescript to check JSDoc comments and MyPy to check Python 2.7 comments, but that's again because type hints are neither part of Python 2.7, nor JavaScript.
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).
While not a dependently-typed language, the Rust compiler can do this here for arrays. Arrays in Rust have the length as part of their type, which is compile-time constant, and if you're indexing with another compile-time constant the compiler will check it. So for a line:
let number: i32 = [][0];
The compiler knows the array is 0-length, therefore the index is out of bounds, and emits this error:
error: this operation will panic at runtime
--> src/main.rs:2:23
|
2 | let number: i32 = [][0];
| ^^^^^ index out of bounds: the length is 0 but the index is 0
|
= note: `#[deny(unconditional_panic)]` on by default
Of course, it's trivial to defeat by converting the array to a slice first, then you get a runtime error.
As an aside, am I the only one who got Four Candles'd by that title?
That seems like a pretty insane default. Do you happen to know what the thinking is? While I'm fortunate enough to have never needed to spend significant time working in JS and its spawn, I've heard a lot of good things from people I respect about TS and its incremental typing approach, so I'm starting from the baseline assumption that this is a reasonable choice.
There seem to have been a few options that are disabled by default and emit additional errors, that slowly get turned on by default in later versions. Perhaps this is one of them.
Despite the theoretical decidability of rank-2 type inference their actual implementations in GHC are the same IIRC (so rank-2 types are not fully inferrable by GHC). I think the difference is really just one of historicity and backwards compatibility at this point. They resolve to the same underlying mechanism.
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.
If a surgeon needed the help of a computer to make sure that he/she didn't confuse your heart for your kidney, would you trust that surgeon to do an operation on you?
How does this metaphor make literally any sense? In what way is type checking similar to making sure you do not kill a person because you can't tell the difference between two organs that look completely different and are in completely different parts of the body?
Here's a metaphor that makes exactly as much sense:
"Construction workers should wear hard hats."
"If surgeons needed to wear bulletproof vests to perform surgery, that would be silly!"
Protective equipment is typically used to protect people, not products.
1. Tests detect errors at runtime. Typing is completely redundant when you have even half-decent tests.
2. Comments, good variable and function names provides documentation too.
3. Not really. TypeScript is not faster than JavaScript for example. Even in certain cases where they are faster (e.g. comparing C/C++ with JavaScript), the max speedup is typically less than 40% in the absolute best use cases.. For the average case (typical program) the speedup is typically insignificant (like 5%, 10%...). Also, static types don't stop people from writing inefficient algorithms.
On the other hand, statically typed languages with a build step slow down the develop/test iteration speed. In the case of TypeScript, transpilers add complexity to the project in many ways including compatibility issues (since now you have to worry about not just Node.js or Browser version but also TypeScript version and the different permutations)... Source mapping doesn't work right in certain environments. The output often looks mangled and is hard to debug in a constrained remote environment. Takes more time to setup. Adds many unnecessary dependencies to your project. Makes your software harder to integrate by third-parties since your schema is more rigid and might not correspond with their own type system. They encourage developers to define complex function signatures with complex interfaces and encourage passing instance references instead of simple copy-by-value primitives.. The drawbacks are significant and I could keep listing them all day.
I mean we're not surgeons, we just make over-complicated wordpress themes.
I like static typing because sometimes those systems are complicated (for better or worse), and you want to understand the wake of a certain change. Or, it's just another form of documentation. How is it disagreeable that these are good things, or only relevent for the less experienced?
It's very relevant. In fact I would argue that type systems only address the simplest possible errors and do absolutely nothing about the most complex, time-consuming errors such as those related to unpredictable state mutations caused by multiple events being processed in parallel or having different parts of the code operate on the same instances.
In fact, I would argue that static typing encourages developers to define more complex function interfaces which creates stronger coupling between components in the code and this leads to instances being passed around/shared between more different files and this is more likely to lead to unpredictable mutations of those instances' state. It makes it easier for developers to neglect good separation of concerns.
Dynamic languages make it more difficult to keep track of complex instances between different functions and files so they encourage developers to pass more primitive 'pass by value' arguments; this results in looser coupling between the components.
Dynamic languages encourage more modular, more interchangeable code. This is why the most popular package managers of all time are based on dynamic languages like JavaScript (npm) or Ruby (RubyGems) and not on statically typed languages; it's not a coincidence.
statically typed languages with dependent types solve this problem of “static types not catching off-by-ones”, although I question the premise of these being the most common software bugs. Perhaps in a CS class these are the most prevalent?
Furthermore,
> Dynamic languages encourage more modular, more interchangeable code.
Have you ever used an ML or another typed language with an actual module system? It makes these dynamic languages look duct-taped in comparison.
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.