> 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.
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".