5 ms·

> And if a type system can not guard against run-time errors, what’s the merit of having one? This makes me really question the author's credibility. Clearly

by cle 8y ago

> And if a type system can not guard against run-time errors, what’s the merit of having one? This makes me really question the author's credibility. Clearly the author is pretty confused about static vs. dynamic type systems, and the value and history of type systems in general.

Spivak 8y ago
Why? I think it's very reasonable that a type system should make runtime erorrs impossible. Obviously errors happen but ideally the type system should make you handle them all. For example this should be disallowed by the type system. db_handle h = new DBConnection() * What if the connection arguments are incorrectly formated? * What if the DNS name doesn't resolve? * What if the port isn't open? * What if the password is wrong? If you're going to assign to the handle you have to prove to the compiler that the constructor will return a valid, working handle. Result q = h.sendQuery(...) This should also fail. * What if the connection dropped? * What if your credentials are no longer valid? * What if the query is malformed? x = a / b Prove to the compiler that b is nonzero or that you've handled the case where it is. Elm damn close to this ideal.
- UncleEntity 8y ago
  > If you're going to assign to the handle you have to prove to the compiler that the constructor will return a valid, working handle. I'm trying to imagine how one could prove to the compiler that an event in the far distant future is valid (without the obvious solution of throwing an exception in the constructor but that is at runtime so...)
  - heavenlyblue 8y ago
    Well, an event in a far distant future is always valid if none of the paths leading to that event contain any code that raise an exceptional condition. That’s it.
- cle 8y ago
  One of the early uses of type systems was about performance of memory allocation, which brought massive performance improvements. Folks quickly realized that they could be used to enforce invariants, which they're also really good at. Those benefits are orthogonal to dynamic vs. static type checking. Even with a dynamically typed language, you get massive performance, security, and correctness guarantees vs. an untyped language. There's huge merit in having a type system that provides all these benefits but still doesn't guard against runtime errors. Which brings me to my point: this person is clearly confused about the benefits of type systems, which don't require static typing to add incredible value.

by cle 8y ago

Spivak 8y ago

Why? I think it's very reasonable that a type system should make runtime erorrs impossible. Obviously errors happen but ideally the type system should make you handle them all. For example this should be disallowed by the type system. db_handle h = new DBConnection() * What if the connection arguments are incorrectly formated? * What if the DNS name doesn't resolve? * What if the port isn't open? * What if the password is wrong? If you're going to assign to the handle you have to prove to the compiler that the constructor will return a valid, working handle. Result q = h.sendQuery(...) This should also fail. * What if the connection dropped? * What if your credentials are no longer valid? * What if the query is malformed? x = a / b Prove to the compiler that b is nonzero or that you've handled the case where it is. Elm damn close to this ideal.

UncleEntity 8y ago
> If you're going to assign to the handle you have to prove to the compiler that the constructor will return a valid, working handle. I'm trying to imagine how one could prove to the compiler that an event in the far distant future is valid (without the obvious solution of throwing an exception in the constructor but that is at runtime so...)
- heavenlyblue 8y ago
  Well, an event in a far distant future is always valid if none of the paths leading to that event contain any code that raise an exceptional condition. That’s it.
cle 8y ago
One of the early uses of type systems was about performance of memory allocation, which brought massive performance improvements. Folks quickly realized that they could be used to enforce invariants, which they're also really good at. Those benefits are orthogonal to dynamic vs. static type checking. Even with a dynamically typed language, you get massive performance, security, and correctness guarantees vs. an untyped language. There's huge merit in having a type system that provides all these benefits but still doesn't guard against runtime errors. Which brings me to my point: this person is clearly confused about the benefits of type systems, which don't require static typing to add incredible value.