But is it the same problem, really? Static typing eliminates a whole class of issues that dynamic typed languages don't. Of course you can still have logical bugs, but it's definitely not the same thing. I don't know how to put it better, but you should try writing haskell sometime and you'll see what I mean.

And static languages introduce a whole class of issues that dynamic languages don't have to deal with. You have to learn a separate metalanguage just for the types that isn't expressive enough to do things that are easy in a dynamic language, and even if it were, you'd still have to write everything twice: once in the real language, and once again in the type language. And then you still have to test, don't pretend you don't. If tests are both necessary and sufficient, then why bother with the type language? The static typing is not worth the cost.

>you'd still have to write everything twice: once in the real language, and once again in the type language

Hmm, no I don't? Actually, 99% percent of the time I'm writing haskell, I can just write it like it's a dynamically typed language and the compiler/lsp will just say "Hey, I can see this is an int/string/list/whatever, want me to annotate that for you"?

Hindley–Milner type systems are way way too powerful and I can count on my fingers how many times the compiler was confused when inferring types and I had to manually annotate it.

And yes, of course I have to test the logic of my code. What I don't have to test is that my code behaves when given wrong-type values and that all the code calls functions with values of the correct type, because the compiler is doing that for me.

I haven't worked with Haskell enough to fully object to this, so any complaints I could come up with would be second hand, so I'll abstain. I don't feel fluent in Haskell yet, but my impressions so far were mostly not negative.

I'm mostly complaining about static typing in the style of Mypy/Pyright and Java (and half of Scala, the other half is like Haskell). You know, the static typing one is likely to encounter in industry. But even Hindley-Milner isn't as expressive as fully dependent types like Agda or Idris. If you're going to use static typing at all, why not go all the way?

Scala is going to get "full" dependent types at some point. It's work in progress for a long time already (and it's actually quite close by now).

Besides that your argumentation makes no sens anyway whatsoever:

Fully dependent languages are undecidable by type inference alone. So you're forced "to write everything twice" especially in such a powerful language. But that's actually the whole point of it! Like you duplicate large chunks of your code when writing tests to verify your code in a dynamic language that exact same "duplication" in code when using proper static types is what actually helps to avoid casual errors. But the difference is of course that in the later case the machine can verify that both parts match up (which it can't in case of usual tests!).

On a side note: Why have you such strong opinions about typed languages if you didn't had much used a proper one at all as you say? Of course a type system like that of Java or C/C++ is a huge PITA, but that says nothing at all about static typing in general. Actually quite the contrary as Java's type system is especially painful (and therefore you need to cast your way through the whole time, which is not what static types are for in the first place). But you make general statements about static typing here the whole time. That doesn't seem justified imho.

> "full" dependent types

From the quotation marks, I surmise that you're wondering what a non-full dependent type system could possibly mean. I added that qualifier because Python, in fact, had one, last I checked, with its `Literal` type (https://peps.python.org/pep-0586/#rejected-or-out-of-scope-i...), which is "a very simplified dependent type system", according to the PEP, but "True dependent types" are out of scope, at least for now.

> From the quotation marks, I surmise that you're wondering what a non-full dependent type system could possibly mean.

That wasn't the point. Scala has a few variants of dependent types but that features are constantly diminished as not being "full" (or sometimes even "real") dependent types. I don't buy that as dependent types aren't defined as being like dependent types in say CoC (the Calculus of Constructions). For example Singleton types match also the definition of dependent types when derived from literals; even such types are still weaker than the usual "full" dependent types à la CoC.

Regarding Python: Python has only one type, the "almighty-python-runtime-type", as it's a "dynamic" (unityped) language. Therefore it does not make much sense to talk about "types" in Python at all…

https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

So why not static with the ability to ignore hinting or similar? C# does this.

I think function definitions should be statically defined, but the actual body of a function could easily stay largely dynamic.

I do think that's helpful compared to the strict alternative, but much of the up-front cost is still there. You still write most things twice, and the static type checker still slows you down when prototyping. You'd still be tempted to write bad code to work around the insufficiently-expressive type language, rather than write it in the most natural way, and only give up when it's too hard.

You can also approach this from the other direction: why not start with a dynamic language for the rapid prototyping and gradually introduce typing as the code stabilizes? Python and Typescript do this.

> You'd still be tempted to write bad code to work around the insufficiently-expressive type language, rather than write it in the most natural way. […]

Could you provide any evidence for the claims that one needs "workarounds" and can't write code "in the most natural" way in a statically typed language?

> You can also approach this from the other direction: why not start with a dynamic language for the rapid prototyping and gradually introduce typing as the code stabilizes? Python and Typescript do this.

Which obviously does not work, which is the whole point of this submission and discussion thread…