Hacker News Reader

Comment by toomanydoubts | Hacker News Reader

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

View on HN

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

Reply on news.ycombinator.com