There is an advanced type system that is becoming more and more mainstream, it's Typescript. E.g: https://www.typescriptlang.org/docs/handbook/advanced-types.... (conditional types for example)

Also c++20 with concepts will push the boundaries of what is possible.

But what I'm really looking for and doesn't exist except maybe through libraries, is runtime Dependant types.

What would runtime dependent types be? As I understand, they are a tool for statically proving properties of some code. What use are they at runtime? For code that came up as a result of the working system? I believe properties of generated programs can also be proven statically. For user-provided code? Why not just run the compiler/interpreter on it?

In practice, the overwhelming majority of tests I see in dynamic languages are just checking things that get statically checked in a language with a good algebraic type system (e.g. Typescript, Rust, Haskell, etc.)

The Rust type system made me understand why you want to have one.

It boils down to beeing able to catch as many bugs as possible in compile time and a good type system allows you to move whole classes of rules into that space.

So when you try to use that variable wirh the wrong type in the wrong place it will notify you before deployment. This can be extremely reassuring and allows you to code more freely because it makes it harder to break things accidentally in a bad way.

I like it in principle, but it can also be really annoying and fussy. A lot of the time with Rust (perhaps because I'm no good, but still) I find myself fiddling around with some inane difference between two types I don't really care about (for instance, whether a function pointer is boxed or not). It gets so distracting that I often do the bulk of the work with the linter switched off, just so I can actually think about what I'm doing without having to go down a rabbit hole just so an option is turned into a result in some bit of the code I'm probably going to delete anyway.

I think a combination of the explicitness about performance implications, the focus on safety, and the whole lifetime thing leads to Rust being, if not specifically complicated to write, at least extremely fiddly. Which is great if you're in some kind of hot spot where you need all that control and safety. But when you're just trying to add two strings together to make some random error message, it's actually really annoying having the language purposefully complicate things just so you realize there's going to be an allocation. It leads to a really weird distribution of effort, where I spend about half the time on important stuff, and the other half on things that are so trivial and irrelevant to both performance and user experience that I'd be totally happy if they were just all dumped on the heap and cast through void pointers.

I think you probably are just not there yet, Rust defintly has a steep learning curve to it, especially if you are used to other paradigms or patterns than those used in the language.

I remember fighting the compiler because I tried to write what I thought of as “beautiful” abstractions, that were basically inspired by my object oriented Python use. Everything and the interaction between everything was a incredibly hard challenge. Until at one point I just gave up and said: “Okay Rust, scrap beautiful code, I’ll just do it your way” and then things started instantly to fall into place.

I am not saying that this is where you are at, but it was like that for me. Do I still struggle with types? Sometimes, but rarely and then it is mostly a mix between lack of focus, lazyness and a mistake somewhere else.

I think python is a great example of what I'm talking about, though. I'm not a Python programmer - I've never written anything over a hundred lines in Python, nor sat down to really learn it. However, every time I do something in Python, I'm impressed by how smoothly what I expect to happen actually happens.

With Rust, where I've put in a chunk of effort to learn, where I've read books, and have written a substantial amount of code, I'm constantly going back to the documentation to do simple things. The main offender is my inability to remember what traits are implemented by what types. I mean, off the top of your head, is '.binary_search()' a method on &[T] or Vec<T>? Or both? I literally can't remember right now.

> Dependent types are totally academic/enthusiast concern at this point, Haskell is still very much niche, and only Rust might cut it as having a slightly more complex type system and being actually used...

They're also sneaking into the gradually typed languages. Typescript and python both support literal types, which are a (very) weak form of dependent types. C++ templates also support a different weak form of dependent types (ints), that is used to, among other things, support typechecked matrix operations in eigen.

Dependently typed languages are one example, but there are popular languages with modern type systems and various degrees of popularity. The ML-family comes to mind. Rust is one gaining traction as well.

Keep in mind Python was considered niche 10 years ago.

I'd say Python was niche closer to 20 years ago. According to http://pypl.github.io/PYPL.html in 2009 Python was about as popular as C# is now, which is my recollection.