4 ms·

This is just rehashing the same tired and fallacious argument that most errors aren't type errors. And it is pure fallacy because different languages have diffe

This is just rehashing the same tired and fallacious argument that most errors aren't type errors. And it is pure fallacy because different languages have different ideas as to what constitutes a type, and therefore have completely different ideas as to what a type error is. If I write `Object.new.foo` in Ruby, I get a NoMethodError. Not a type error, right? But that's the thing, that would be a type error in almost all statically typed languages. And it doesn't even come close to stopping there...there are hundreds of examples of errors that are not Type Errors in your dynamic language that are type errors in some other language. NullPointerException? That's a type error that is entirely prevented by many type systems. If you accidentally multiply your time and distance instead of divide to get your velocity, that would be a Type Error in F# using their units of measure types. If you accidentally pop an empty stack, that might be an EmptyStackException even in many statically typed languages, but would absolutely be a Type Error in a language with dependent types like ATS or Idris. In the end, dynamic typing is just a way to make runtimes slow and building correct programs slower, in exchange for some entirely subjective aesthetic or ergonomic quality. And sure, most type systems in practical languages aren't "complete" enough to eliminate the need for tests. But don't tell me that because you don't eliminate tests that you don't need types. That's bullshit. Statically enforced types eliminate errors, and every check that you defer to runtime is an error waiting to happen. If you're willing to make that tradeoff, by all means do so...but don't lie to me.

deleted 9y ago
[deleted]
alkonaut 9y ago
Also: tests don't prove the absence of errors, only their presence. Static types prove the absence of some errors. Any type snob will tell you that even in supposedly good type systems, without dependent types, all lists are dynamic! Yet most of us that swear by static types don't use dependent types (much). There might be a limit where "more types" don't pay off their added cost relative to the thinking and typing needed and the security gained. Where that limit is depends on the application. Formally verified programs aren't used for many simple web backends - for good reason. Also, type systems aren't equal. There are decent dynamic ones and terrible ones. Same goes for static type systems.
- continuational 9y ago
  As for dependent types, it's probably just that the type systems for them are simply not yet mature enough to be practical for most tasks.
  - seanwilson 9y ago
    If you're using a dependently typed language, you have to write maths proofs to prove properties hold. It's incredibly challenging and not going to be automated any time soon.
  - agentultra 9y ago
    I think that's going to change. It's my completely biased, uninformed opinion that dependently typed systems are much easier to reason about than their counterparts.
evincarofautumn 9y ago
Exactly. Almost any error can be a type error with a sufficiently expressive type system, because a type system is just a way to mechanically prove things about your code. A more expressive type system lets you prove more useful things. Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first. On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :) To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it. On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.
- kronos29296 9y ago
  With things like typescript or mypy in python you fall the other way around with types in dynamic languages. You can do it if you really want (optional but recommended for large projects). So Python and typescript have a nice sweet spot between static and dynamic if you want.
- junke 9y ago
  > ...the cost is that they don’t allow it. Saying they don't allow it is too strong (they allow it, but it might be harder).
  - evincarofautumn 9y ago
    You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”, because its result type can depend on the value of the integer passed in at runtime. You can only prove existential properties (“there are integers for which this function returns an integer”) through testing. That testing can be done before runtime in some languages, e.g., with Perl’s BEGIN/UNITCHECK/CHECK/INIT blocks. But it’s not really the same. In a referentially transparent, statically typed language, if you give me a function of type ∀a. a → a, then I know for a fact that if this function halts, it must be the identity function. The only thing it can do is return its input. The same function in a dynamically typed language could return any value of any type, because its result’s type can depend on both the type and the runtime value of its input, or not depend on its input at all, even if it’s referentially transparent. Even if you supply that type annotation and check it at runtime (“this function returns a value of the same type as its input”), it would only be checking a single code path, and it could still give me any value. That is, a valid implementation would be “return 3”—I wouldn’t get a type error if I only ever called it on integers, but it would still be non-parametric.
junke 9y ago
Yes, everything can be a type error (security, memory management, concurrency (deadlocks), ...). You define properties about the code and you can check them either at runtime, or statically. If I choose to write in OCaml, the memory management is done with a GC, which relies on dynamically typed memory; but I write in Rust, there is no GC but a kind of static analysis for managing ownership; both approaches work. Your fallacy is saying: there is a whole class of errors that can avoided if only we use a different type system, so there is no point in using that type system which defers (some or all) checks at runtime. I can write code that manipulates values which represent types in the language, at runtime. If the types happen to be known or declared during compilation, fine enough, they can be optimized away. Otherwise, they will be checked later (which transparently invokes dynamic dispatch if needed), and I can even use them once they are known to compile the code myself, on a closure; there, along with other values which are then known, they can be taken into account to perform more aggressive optimizations. Why don't all language provide this? As for bugs or errors, if you cannot lower risks (with static guarantees) then you have to improve on fault tolerance. You take other approaches to ensure the system behaves well, even if some parts can fail (e.g. Erlang).
seanwilson 9y ago
> In the end, dynamic typing is just a way to make runtimes slow and building correct programs slower, in exchange for some entirely subjective aesthetic or ergonomic quality. To be honest, I really don't understand what the benefit of dynamic types are supposed to be. People say it's easier and less hassle to get something up and running because you don't need type annotations but this isn't an issue with decent type inference and all you're doing is replacing compile time checks with runtime crashes.
- carlmr 9y ago
  I still feel there's a correlation between Python coding bootcamp survivors and the new wave of people thinking static typing is hard. It makes it easier if you know what you're doing.
  - flavio81 9y ago
    There are also people with 10+ years of using static typing languages like Java or C++, that then go to Python or Lisp or Racket and find out they are more productive with dynamic typing, while writing even more readable code than before.
abetusk 9y ago
I don't claim to be very knowledgeable about this but it seems like you're bringing up a valid point. In the presenters analysis, he looks for very specific types of bugs when making the claim that static typing only addresses 1-5% of bugs. Your claim is, essentially, his type of analysis undercounts the number of bugs a non statically typed language by creating too heavy handed of filter. Do you have any data to back this up or have links to papers that try and do a better job of counting issues that statically typed languages catch?
hyperpallium 9y ago
Insightful +1. But by "types", they really mean the so-called practical languages' types, not the academic definition. Types allow you to prove something about your program - but it takes extra upfront effort to prove something. The trade-off between ease and proof-power has settled on what we have... IDK of course, but I don't think it will change much. And worse, the popularity of static typing is mainly due to performance, followed by documentation, and correctness of proof not really in it. But maybe this story's empirical github evidence on errors will shift it a little. When you're re-coding all the time, the upfront cost isn't amortized over future runs as much as it used to be. Libraries are, but the massive real-world crowd-testing (i.e. usage) catches them... BTW I really like units of measure types, you get dimensional analysis almost for free. You can do it in e.g. java but it's verbose (i.e. it's java). Classes, with arithmetic methods (add, sub, mult etc), You need an ezplicit class for each unit combination (though you can do a little better with generics). And get compile-time type errors when you assign, compare or operate incorrectly.
flavio81 9y ago
> This is just rehashing the same tired and fallacious argument that most errors aren't type errors. And it is pure fallacy because different languages have different ideas as to what constitutes a type, Ok, so you are writing an algorithm for a fast approximation of ATANH using IEEE floating point standard. In type: IEEE floating point number Out type: the same. Tell me how the magical type checking of the excellent programming language you propose will ensure that my calculations are correct.

deleted 9y ago

[deleted]

alkonaut 9y ago

Also: tests don't prove the absence of errors, only their presence. Static types prove the absence of some errors. Any type snob will tell you that even in supposedly good type systems, without dependent types, all lists are dynamic! Yet most of us that swear by static types don't use dependent types (much). There might be a limit where "more types" don't pay off their added cost relative to the thinking and typing needed and the security gained. Where that limit is depends on the application. Formally verified programs aren't used for many simple web backends - for good reason. Also, type systems aren't equal. There are decent dynamic ones and terrible ones. Same goes for static type systems.

continuational 9y ago
As for dependent types, it's probably just that the type systems for them are simply not yet mature enough to be practical for most tasks.
- seanwilson 9y ago
  If you're using a dependently typed language, you have to write maths proofs to prove properties hold. It's incredibly challenging and not going to be automated any time soon.
- agentultra 9y ago
  I think that's going to change. It's my completely biased, uninformed opinion that dependently typed systems are much easier to reason about than their counterparts.

evincarofautumn 9y ago

Exactly. Almost any error can be a type error with a sufficiently expressive type system, because a type system is just a way to mechanically prove things about your code. A more expressive type system lets you prove more useful things. Of course, you can easily do things in a dynamic language that are observably correct, but which are very difficult to prove correct without advanced logic (i.e., an expressive type system). And more advanced type systems typically lose some nice ergonomic properties of simpler type systems, such as clear error messages, type inference, principal types, or decidability. So I can definitely see how someone moving for example from Java to Python would find the latter very liberating at first. On the other hand, you can argue that people shouldn’t be writing code that’s so difficult to prove things about in the first place. :) To my mind, the benefit of static types is that they allow proving properties of your code, but the cost is that they may force you to do so; the benefit of dynamic types is that they don’t force you, but the cost is that they don’t allow it. On balance I think static types are therefore preferable, because you can always fall back to dynamic types (strings/hashes/variants/sums) in a static language, but you can’t “fall forward” to static types in a dynamic language.

kronos29296 9y ago
With things like typescript or mypy in python you fall the other way around with types in dynamic languages. You can do it if you really want (optional but recommended for large projects). So Python and typescript have a nice sweet spot between static and dynamic if you want.
junke 9y ago
> ...the cost is that they don’t allow it. Saying they don't allow it is too strong (they allow it, but it might be harder).
- evincarofautumn 9y ago
  You can’t prove even very simple universal properties of dynamically typed code, such as “when given an integer, this function always returns an integer”, because its result type can depend on the value of the integer passed in at runtime. You can only prove existential properties (“there are integers for which this function returns an integer”) through testing. That testing can be done before runtime in some languages, e.g., with Perl’s BEGIN/UNITCHECK/CHECK/INIT blocks. But it’s not really the same. In a referentially transparent, statically typed language, if you give me a function of type ∀a. a → a, then I know for a fact that if this function halts, it must be the identity function. The only thing it can do is return its input. The same function in a dynamically typed language could return any value of any type, because its result’s type can depend on both the type and the runtime value of its input, or not depend on its input at all, even if it’s referentially transparent. Even if you supply that type annotation and check it at runtime (“this function returns a value of the same type as its input”), it would only be checking a single code path, and it could still give me any value. That is, a valid implementation would be “return 3”—I wouldn’t get a type error if I only ever called it on integers, but it would still be non-parametric.

junke 9y ago

Yes, everything can be a type error (security, memory management, concurrency (deadlocks), ...). You define properties about the code and you can check them either at runtime, or statically. If I choose to write in OCaml, the memory management is done with a GC, which relies on dynamically typed memory; but I write in Rust, there is no GC but a kind of static analysis for managing ownership; both approaches work. Your fallacy is saying: there is a whole class of errors that can avoided if only we use a different type system, so there is no point in using that type system which defers (some or all) checks at runtime. I can write code that manipulates values which represent types in the language, at runtime. If the types happen to be known or declared during compilation, fine enough, they can be optimized away. Otherwise, they will be checked later (which transparently invokes dynamic dispatch if needed), and I can even use them once they are known to compile the code myself, on a closure; there, along with other values which are then known, they can be taken into account to perform more aggressive optimizations. Why don't all language provide this? As for bugs or errors, if you cannot lower risks (with static guarantees) then you have to improve on fault tolerance. You take other approaches to ensure the system behaves well, even if some parts can fail (e.g. Erlang).

seanwilson 9y ago

> In the end, dynamic typing is just a way to make runtimes slow and building correct programs slower, in exchange for some entirely subjective aesthetic or ergonomic quality. To be honest, I really don't understand what the benefit of dynamic types are supposed to be. People say it's easier and less hassle to get something up and running because you don't need type annotations but this isn't an issue with decent type inference and all you're doing is replacing compile time checks with runtime crashes.

carlmr 9y ago
I still feel there's a correlation between Python coding bootcamp survivors and the new wave of people thinking static typing is hard. It makes it easier if you know what you're doing.
- flavio81 9y ago
  There are also people with 10+ years of using static typing languages like Java or C++, that then go to Python or Lisp or Racket and find out they are more productive with dynamic typing, while writing even more readable code than before.

abetusk 9y ago

I don't claim to be very knowledgeable about this but it seems like you're bringing up a valid point. In the presenters analysis, he looks for very specific types of bugs when making the claim that static typing only addresses 1-5% of bugs. Your claim is, essentially, his type of analysis undercounts the number of bugs a non statically typed language by creating too heavy handed of filter. Do you have any data to back this up or have links to papers that try and do a better job of counting issues that statically typed languages catch?

hyperpallium 9y ago

Insightful +1. But by "types", they really mean the so-called practical languages' types, not the academic definition. Types allow you to prove something about your program - but it takes extra upfront effort to prove something. The trade-off between ease and proof-power has settled on what we have... IDK of course, but I don't think it will change much. And worse, the popularity of static typing is mainly due to performance, followed by documentation, and correctness of proof not really in it. But maybe this story's empirical github evidence on errors will shift it a little. When you're re-coding all the time, the upfront cost isn't amortized over future runs as much as it used to be. Libraries are, but the massive real-world crowd-testing (i.e. usage) catches them... BTW I really like units of measure types, you get dimensional analysis almost for free. You can do it in e.g. java but it's verbose (i.e. it's java). Classes, with arithmetic methods (add, sub, mult etc), You need an ezplicit class for each unit combination (though you can do a little better with generics). And get compile-time type errors when you assign, compare or operate incorrectly.

flavio81 9y ago

> This is just rehashing the same tired and fallacious argument that most errors aren't type errors. And it is pure fallacy because different languages have different ideas as to what constitutes a type, Ok, so you are writing an algorithm for a fast approximation of ATANH using IEEE floating point standard. In type: IEEE floating point number Out type: the same. Tell me how the magical type checking of the excellent programming language you propose will ensure that my calculations are correct.