5 ms·

Types aren't just for catching type errors, they're also a way of defining and enforcing at least parts of the programming contract. Most type systems are poor

Types aren't just for catching type errors, they're also a way of defining and enforcing at least parts of the programming contract. Most type systems are poor at this, but it still goes beyond just catching runtime type errors. The time you save from writing a dynamic program is time not spent on defining that contract. You will eventually be paying for that when the first major refactor comes - if it comes, that is. You will pay for it with extra test coverage, if that's in the budget. Or you will pay for it by re-writing everything. Those may all be worthwhile tradeoffs, but in the long run, I think static types win out.

staticassertion 8y ago
> Types aren't just for catching type errors, they're also a way of defining and enforcing at least parts of the programming contract. I don't disagree. To be clear, I'm a type safety zealot. > You will eventually be paying for that when the first major refactor comes - if it comes, that is. This is fine but not relevant. Erlang, for example, just assumes you'll fuck up the refactor. Actors are isolated interfaces and you can not share state - so a failure in one actor can not impact other actors directly. It's fine to say that static types are better but if you read about Erlang you may find the approach very compelling - Erlang's managed to provide the basis for extremely reliable systems, without types. And as I said, it is not either or. You can build power supervisory structures and statically type your code if you like, but no languages really do it, so you have to reach outside of the language (like using a distributed queue/ microservice approach).
- hota_mazi 8y ago
  > It's fine to say that static types are better but if you read about Erlang you may find the approach very compelling - Erlang's managed to provide the basis for extremely reliable systems, without types. I have yet to see some convincing proof of that, besides that Ericsson router from 20 years ago that ended up being rewritten in C++. Also, even if it is true like you say that > Erlang's managed to provide the basis for extremely reliable systems, without types. This still doesn't prove that there are no languages that can do a better job at it than Erlang. 99.99% of extremely reliable software today runs on non Erlang: C, C++, Java, you name it. Finally, in my experience, writing supervisors in Erlang is just as painful, and if not harder, than writing resilient code based on exceptions in Java or C++.
  - qaq 8y ago
    "I have yet to see some convincing proof of that, besides that Ericsson router from 20 years ago that ended up being rewritten in C++." Control plane for 80% of mobile in the world is Erlang. Core critical infra @ Goldman is Erlang. Control plane for 90% of internet routers is Erlang.
    - hota_mazi 8y ago
      That's neither proof, nor convincing. Just claims. Do you have any statements from these companies that they do indeed do that? I'm not talking about claims from Erlang web sites, but actual companies using Erlang confirming your claims.
  - staticassertion 8y ago
    I'm not advocating for Erlang over type safety. I personally prefer a type based approach. They are also not incompatible. That said, > I have yet to see some convincing proof of that There is no proof, but I can point you to research. pdf warnings: https://jimgray.azurewebsites.net/papers/tandemtr85.7_whydocomputersstop.pdf https://jimgray.azurewebsites.net/papers/tandemtr85.7_whydoc... This paper is fundamental to reliability, and describes two primitives for building reliable systems - transactions, and the "persistent process" (spoilers: it's an actor). And here's Joe Armstrong's thesis. The first 3 chapters are quite relevant and will point you to further research http://erlang.org/download/armstrong_thesis_2003.pdf http://erlang.org/download/armstrong_thesis_2003.pdf > besides that Ericsson router from 20 years ago that ended up being rewritten in C++. This is missing some important information. Erlang is still used at the control plane/ orchestration layer, for exactly the reasons I've described. > This still doesn't prove that there are no languages that can do a better job at it than Erlang. Didn't say otherwise. > 99.99% of extremely reliable software today runs on non Erlang: C, C++, Java, you name it. Sure, but who cares about Erlang? The real money's in isolated persistent processes aka actors, and I bet most reliable software is built on those, whether language provided or not. See AWS's cell based architecture, which is just the actor model with discipline attached. Or all of microservice architecture. > Finally, in my experience, writing supervisors in Erlang is just as painful, and if not harder, than writing resilient code based on exceptions in Java or C++. That's ok.
dragonwriter 8y ago
> Types aren't just for catching type errors, Yes they are. > they're also a way of defining and enforcing at least parts of the programming contract. Violation of those parts of the contract are type errors. (And all proper type errors—those that aren't artifacts of the type system and it's incorrect use or impedance mismatch with the project—are violations of the programming contract. > The time you save from writing a dynamic program is time not spent on defining that contract. No, you can still define the contract when using a dynamic language, and still often save time compared to a real static language. In the ideal case, sure, a static language would add no additional overhead to this, but that's an unattainable ideal.
- bunderbunder 8y ago
  I think you're maybe overly focused on the "compile time type checker" bit of static typing. The contract definition bit is secondary, but useful. It's also at least somewhat separable from the type checking. The best example I can think of is to compare the duck typing that is common in many dynamic languages with the formal interfaces that are more popular in static languages. With duck typing, you basically look for a method with a particular name in an object, and then, having found it, simply assume that that method is going to implement the semantics you expect. That works surprisingly often, but it is a bit rough-and-ready for many people's tastes. With formal interfaces, you have a clearer indication from the type's author that they're consciously planning on implementing a specific set of semantics. They could still be doing it wrong, of course, but it's at least trying to be more meticulous about things. I also think it's worth pointing out that static typing can be useful as a performance thing. Pushing all those type checks into run-time does have costs. There's the extra branch instructions involved in doing all those type checks at run time, and there's the extra memory consumption involved in carrying around that type information at run time. (It's also true that this aspect is very much a continuum, especially with regards to the performance considerations: Many dynamic languages have JIT compilers that can statically analyze the code and treat it as if it were statically typed at run time, and any ostensibly static language that allows downcasting or reflection supplies those features by carrying type information and allowing for type checks at run time.)

staticassertion 8y ago

> Types aren't just for catching type errors, they're also a way of defining and enforcing at least parts of the programming contract. I don't disagree. To be clear, I'm a type safety zealot. > You will eventually be paying for that when the first major refactor comes - if it comes, that is. This is fine but not relevant. Erlang, for example, just assumes you'll fuck up the refactor. Actors are isolated interfaces and you can not share state - so a failure in one actor can not impact other actors directly. It's fine to say that static types are better but if you read about Erlang you may find the approach very compelling - Erlang's managed to provide the basis for extremely reliable systems, without types. And as I said, it is not either or. You can build power supervisory structures and statically type your code if you like, but no languages really do it, so you have to reach outside of the language (like using a distributed queue/ microservice approach).

hota_mazi 8y ago
> It's fine to say that static types are better but if you read about Erlang you may find the approach very compelling - Erlang's managed to provide the basis for extremely reliable systems, without types. I have yet to see some convincing proof of that, besides that Ericsson router from 20 years ago that ended up being rewritten in C++. Also, even if it is true like you say that > Erlang's managed to provide the basis for extremely reliable systems, without types. This still doesn't prove that there are no languages that can do a better job at it than Erlang. 99.99% of extremely reliable software today runs on non Erlang: C, C++, Java, you name it. Finally, in my experience, writing supervisors in Erlang is just as painful, and if not harder, than writing resilient code based on exceptions in Java or C++.
- qaq 8y ago
  "I have yet to see some convincing proof of that, besides that Ericsson router from 20 years ago that ended up being rewritten in C++." Control plane for 80% of mobile in the world is Erlang. Core critical infra @ Goldman is Erlang. Control plane for 90% of internet routers is Erlang.
  - hota_mazi 8y ago
    That's neither proof, nor convincing. Just claims. Do you have any statements from these companies that they do indeed do that? I'm not talking about claims from Erlang web sites, but actual companies using Erlang confirming your claims.
- staticassertion 8y ago
  I'm not advocating for Erlang over type safety. I personally prefer a type based approach. They are also not incompatible. That said, > I have yet to see some convincing proof of that There is no proof, but I can point you to research. pdf warnings: https://jimgray.azurewebsites.net/papers/tandemtr85.7_whydocomputersstop.pdf https://jimgray.azurewebsites.net/papers/tandemtr85.7_whydoc... This paper is fundamental to reliability, and describes two primitives for building reliable systems - transactions, and the "persistent process" (spoilers: it's an actor). And here's Joe Armstrong's thesis. The first 3 chapters are quite relevant and will point you to further research http://erlang.org/download/armstrong_thesis_2003.pdf http://erlang.org/download/armstrong_thesis_2003.pdf > besides that Ericsson router from 20 years ago that ended up being rewritten in C++. This is missing some important information. Erlang is still used at the control plane/ orchestration layer, for exactly the reasons I've described. > This still doesn't prove that there are no languages that can do a better job at it than Erlang. Didn't say otherwise. > 99.99% of extremely reliable software today runs on non Erlang: C, C++, Java, you name it. Sure, but who cares about Erlang? The real money's in isolated persistent processes aka actors, and I bet most reliable software is built on those, whether language provided or not. See AWS's cell based architecture, which is just the actor model with discipline attached. Or all of microservice architecture. > Finally, in my experience, writing supervisors in Erlang is just as painful, and if not harder, than writing resilient code based on exceptions in Java or C++. That's ok.

dragonwriter 8y ago

> Types aren't just for catching type errors, Yes they are. > they're also a way of defining and enforcing at least parts of the programming contract. Violation of those parts of the contract are type errors. (And all proper type errors—those that aren't artifacts of the type system and it's incorrect use or impedance mismatch with the project—are violations of the programming contract. > The time you save from writing a dynamic program is time not spent on defining that contract. No, you can still define the contract when using a dynamic language, and still often save time compared to a real static language. In the ideal case, sure, a static language would add no additional overhead to this, but that's an unattainable ideal.

bunderbunder 8y ago
I think you're maybe overly focused on the "compile time type checker" bit of static typing. The contract definition bit is secondary, but useful. It's also at least somewhat separable from the type checking. The best example I can think of is to compare the duck typing that is common in many dynamic languages with the formal interfaces that are more popular in static languages. With duck typing, you basically look for a method with a particular name in an object, and then, having found it, simply assume that that method is going to implement the semantics you expect. That works surprisingly often, but it is a bit rough-and-ready for many people's tastes. With formal interfaces, you have a clearer indication from the type's author that they're consciously planning on implementing a specific set of semantics. They could still be doing it wrong, of course, but it's at least trying to be more meticulous about things. I also think it's worth pointing out that static typing can be useful as a performance thing. Pushing all those type checks into run-time does have costs. There's the extra branch instructions involved in doing all those type checks at run time, and there's the extra memory consumption involved in carrying around that type information at run time. (It's also true that this aspect is very much a continuum, especially with regards to the performance considerations: Many dynamic languages have JIT compilers that can statically analyze the code and treat it as if it were statically typed at run time, and any ostensibly static language that allows downcasting or reflection supplies those features by carrying type information and allowing for type checks at run time.)