3 ms·

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

by gilch 4y ago

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?

still_grokking 4y ago
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.
- gilch 4y ago
  > "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-ideas 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.
  - still_grokking 4y ago
    > 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-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...

by gilch 4y ago

still_grokking 4y ago

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.

gilch 4y ago
> "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-ideas 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.
- still_grokking 4y ago
  > 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-languages-are-static-languages/ https://existentialtype.wordpress.com/2011/03/19/dynamic-lan...