The argument seems to rely on the cost of static typing, which is stated in the following four points that I challenge:
It requires more upfront investment in thinking about the correct types.
I don’t buy this argument at all. If you don’t think about correct types in a dynamic languages, you will run into trouble during testing (and production, when your tests aren’t perfect). You really have to get your types right in a dynamic language too. Arguably, with a statically typed language, you have to think less because compiler will catch your error. I think that’s the whole point of statically typed languages (performance concerns aside).
It increases compile times and thus the change-compile-test-repeat cycle.
I’d have to see some proof to show that static typing plays a significant role in compile time. I’ll buy that you can make a very complicated (perhaps turing complete) type system and that would have a big impact. But there are statically typed languages that compile really fast, and most of the compile time is probably not spent on types. I’d argue that it is likely for the compiler to catch your error with types faster than you could compile, run, and test to find the same error with no types.
It makes for a steeper learning curve.
That may or may not be true. Sure, a type system can be very complicated. It doesn’t have to be. On the other hand, a dynamic language will still have types, which you need to learn and understand. Then, instead of learning to annotate the types in code, you learn to figure out type errors at run time. Is that so much easier?
Either way, I don’t believe type systems are an insurmountable barrier. And I think some people give the learning curve way too much weight. Maybe they are working on throwaway software on a constantly changing faddy tech stack, in a place with high employee turnover. It’ll matter more. I suppose there’s a niche for that kind of software. But I’m more into tech that is designed for software that is developed, used, and maintained for years if not decades. A little bit of extra learning up front is no big deal and the professionals working on it will reap the benefits ever after.
And more often than we like to admit, the error messages a compiler will give us will decline in usefulness as the power of a type system increases.
That might be the case with the current crop of languages with clever type system, though I don’t know if it’s inherent. Do static type system need to be so powerful (read: complicated) however? A simpler system can get you just as much type safety, at the expense of some repetition in code.
–
I think there are dimnishing returns, but not due to the cost of static typing as such, but rather due to the fact that types just don’t catch all errors. Once the low hanging fruit is out, there’ll be proportionally more and more logic errors and other problems that aren’t generally prevented with types. Or you could catch these with extensive type annotation, but the likelihood of preventing a real problem becomes small compared to the amount of annotation required. And then there’s the usual question: who checks the proof?
There have been some famous bugs that resulted from systems using different units. So if these numeric quantities were properly typed, these bugs would have been prevented. However, what if we change the scenario a little, and suppose we’re measuring fuel or pressure, in the right units. But we read the wrong quantity – spent fuel instead of stored fuel, or exterior pressure instead of interior pressure? Sure you can add more types to prevent such misuse, but it gets more and more verbose, and then you’re moving closer and closer to re-expressing (and thus enforcing) the program logic in the language of the type system; we could consider that to be a language of its own.
Now you have two programs, and one can prevent bugs in the other, but both could still be buggy. And the other program starts to grow because you start needing explicit conversions to enable the code to actually perform a computation on internal-pressure-in-pascal. Of course you are subverting the type system when you say you really want to convert internal-pressure-in-pascal to just pressure-in-pascal or whatever. Bugs ahoy?
A simpler system can get you just as much type safety, at the expense of some repetition in code.
I agree with most of the rest of your comment, but this part is untrue. Stronger type systems do allow you to enforce more powerful laws at compile time. At one end of the curve we have a type system like C’s, which barely buys you anything, and then at the other end we have full dependent types where you can prove arbitrary invariants about your code (this function always terminates, this value is always even, etc.) that you cannot prove in a weaker type system. In between is a huge spectrum of safety checking power.
The C type system can actually be quite powerful if you wrap basic types in one element structs. struct meter { int v; } and struct foot { int v; } can’t be added by mistake, but can still be worked with using one line inline functions with no performance penalty. It’s just work (which nobody likes).
I would not describe that as “quite powerful” at all. That’s one of the most basic things a type system can give you.
You can’t really prove any interesting properties until you at least have proper polymorphism. Java doesn’t, for example, because every object can be inspected at runtime in certain ways. In a sensible type system, there are no properties of objects except those which are explicitly stated in the type of the object.
In such a type system, you can prove interesting properties like that a data structure does not “depend” in any way on the objects in contains. For example, if you could implement a function
fmap :: (a -> b) -> f a -> f b
Which “mapped over” the contents of your object with some function, this would prove that your object never inspects its contents and therefore its structure does not depend on the values of its contents (because this function is universally quantified over ‘b’, and therefore you could map every ‘a’ to a constructed type which cannot be inspected in any way).
You can prove all sorts of useful properties like this (often without even realize you’re doing it) once you have proper quantification in your type system. One of the coolest quantification-based proofs I know of is that Haskell’s ST monad is extrinsically pure.
As you add more power to your type system (up to full dependent types, linear types, etc.) you can prove more and more useful things.
In mathematics the system Z of integers and the system R of reals are different. The number 3 has different properties depending on system context - for example 3x = 1 has a solution in the second context.
I don’t buy this argument at all. If you don’t think about correct types in a dynamic languages, you will run into trouble during testing (and production, when your tests aren’t perfect). You really have to get your types right in a dynamic language too. Arguably, with a statically typed language, you have to think less because compiler will catch your error. I think that’s the whole point of statically typed languages (performance concerns aside).
That’s a good point and one that took me a long time to learn: if a concept cannot be expressed in a language, it doesn’t magically disappear and absolve the programmer from thinking about it. Types are one example as you mention; similarly, in many discussions about Rust, some people mention that the borrow checker is an impediment to writing code. It’s true that some programs are rejected by the compiler, but lifetime and ownership are also concerns in C programs as well. The main differences are that in Rust you have rules and language constructs to talk about those concerns while in C it’s left to documentation and convention.
I don’t buy this argument at all. If you don’t think about correct types in a dynamic languages, you will run into trouble during testing (and production, when your tests aren’t perfect). You really have to get your types right in a dynamic language too. Arguably, with a statically typed language, you have to think less because compiler will catch your error.
It’s true that you have to get the types right in a dynamic language, but the appeal of dynamic languages isn’t that you don’t have to think about types. It’s that you don’t have to think about the shape of types. For example:
def make_horror_array(depth: int):
arr = []
deepest_arr = arr
for i in range(depth):
deepest_arr.append([])
deepest_arr = deepest_arr[0]
deepest_arr.append(depth)
return arr
What type should that return? Contrived, but it’s not the gnarliest type problem I’ve run into. Sometimes it’s nice to have a language where I can give up on getting the types right and rely on tests and contracts to check it.
It’s that you don’t have to think about the shape of types.
How do you use a value without thinking about it’s type or shape?
In your example, you can’t just blindly apply numerical operation to first element of that horror array since it might be another array. So, if you wanted to get to the value inside of those nested arrays, you’d need to think about how you would “strip” them off, wouldn’t you? And wouldn’t it mean that layers of nesting have some special meaning for us?
we can write a Haskell version that distinguishes between a value nested in a “layer” and a value by itself:
λ> :{
λ> data Nested a = Value a | Layer (Nested a)
λ>
λ> -- just for presentation purposes
λ> instance Show a => Show (Nested a) where
λ> show (Value a) = "[" ++ show a ++ "]"
λ> show (Layer a) = "[" ++ show a ++ "]"
λ> :}
λ>
λ> mkHorror n = foldr (.) id (replicate n Layer) $ Value n
λ> :type mkHorror
mkHorror :: Int -> Nested Int
λ>
λ> mkHorror 0
[0]
λ> mkHorror 1
[[1]]
λ> mkHorror 5
[[[[[[5]]]]]]
λ> mkHorror 10
[[[[[[[[[[[10]]]]]]]]]]]
and if we don’t need layers anymore, we can get value out pretty easily:
λ> :{
λ> fromNested :: Nested a -> a
λ> fromNested (Value a) = a
λ> fromNested (Layer a) = fromNested a
λ> :}
λ>
λ> fromNested (mkHorror 0)
0
λ> fromNested (mkHorror 5)
5
This is because type theory is confused about what programs do - which is operate on bit sequences (or, these days, byte sequences). These sequences may be representations of mathematical objects or representations of things that are not mathematical objects, but they remain representations, not actual ideal mathematical objects.
The type system can be fine but the rules you define with the types could be flawed. Thus, you can still write flawed programs that the type system can’t prevent because the types were defined incorrectly.
It requires more upfront investment in thinking about the correct types.
I don’t buy this argument at all. If you don’t think about correct types in a dynamic languages, you will run into trouble during testing (and production, when your tests aren’t perfect).
One thing I am learning from working with inexperienced developers is that even thinking about which container type you are using is a challenge. Should your function return a Seq? An Array? An Iterator? A Generator? And what if your new library returns a Generator and the old one returned an Iterator and now you have to rewrite all your declarations for seemingly no reason at all? Some kind of “most general type” restriction/requirement/tool would help with this…
This is one of the things I think Go does really well (in spite of having a generally quite weak type system) - thanks to implicit interfaces, you can just return the concrete type you’re using and the caller will automatically pick up that it ‘fits’.
I’m unclear what you mean. Many languages offer two solutions. You can declare the variable IEnumerable or whatever as appropriate. Or you declare the variable as “whatever type the initializer has”.
I think one reason this whole debate irks me is the unspoken belief that programming languages need to feed the
beast of productivity, which always demands results faster and cheaper. (He does mention different domains in the article.) Any language that presents any sort of negative feedback on correctness of code is seen as a hindrance.
I’m not arguing for poor developer UX, I’m arguing that the “throw code at the wall and keep what sticks” mentality is stupid and not the way to build a system.
Ummm, I’m old and crotchety, and one of my cats is sick, so take this with pinch of salt.
“SRE, Go Programmer, Mathematician.”
I beg of you, Software Engineers, Computer Scientists or anyone in the field, pleeeease don’t self-identify with one language. It breaks my heart. There are vast tracts of land to explore!
As far as the post though, it’s weird though, although I enjoy programming in loosely typed or dynamically typed languages occasionally, I’ve generally had just as much, if not more productivity in statically typed environments. Especially in these days of editors that fully understand the AST and type flow.
So, as far as increasing compile times… I don’t even need to compile very often these days - well not until I can already see that the thing compiles - the tools are that good.
Even without the fancy editors though, seeing really strong concrete types explicitly in the code is a wonderful form of documentation that is really beneficial to others that have to maintain things years down the line. Personally I only begrudgingly accepted auto’s and var’s in the last five years although I do have to concede they do make refactoring more convenient and save key presses.
All in all, it seems like he is really torn up and like he’s trying to convince himself or his boss one way or the other. I kind of feel for the guy actually :/
I beg of you, Software Engineers, Computer Scientists or anyone in the field, pleeeease don’t self-identify with one language. It breaks my heart. There are vast tracts of land to explore!
I’m still trying to convince our hiring people that advertising for “ruby programmer” or “Javascript programmer” is like advertising for “hammer user” instead of “carpenter”
So, as far as increasing compile times… I don’t even need to compile very often these days - well not until I can already see that the thing compiles - the tools are that good.
I think this is a fascinating point. Strongly typed languages, especially those that separate side effects, don’t really need to be fully compiled to reason about, at least in byte-sized pieces.
“The value of static typing is subjective” might be a better name for this article. Implying that static typing has diminishing returns is counter to the argument of the post.
How is it counter? It’s how the author is able to believe that Go has the Goldilocks amount of type checking. If benefits didn’t diminish they’d have to agree that generic containers are important.
The thesis of the post is that the value of static typing is subjective. And there are some graphs that the author believes are universal. But there is not reason to think one’s subjective value of static typing requires the benefits diminish or match those graphs.
“Correct code velocity” is not a function of “number of keypresses” nor is it “number of times I have to change what I wrote to convince the type system to attempt it”. It’s a mix of many more things as well:
How long it takes you to figure out existing code; who calls this? When? What kind of data does it expect?
How loosely or tightly coupled individual modules are
How similar modules will be when they’re doing similar things
Just how similar the execution will be at runtime versus the code you’re looking at; if there’s macros, you need to be able to expand them via tooling or in your head. If the module structures are manipulated dynamically, like with AOP or some other sort of runtime metaprogramming, you can spend hours trying to track down where things are going wrong, let alone why.
Understanding what symbols are available in any given scope, and what they might be…
I could go on forever. Not only do these things affect performance in both speed and quality, but they affect each other as well. It’s a giant combinatorial problem space, and this sort of inch-deep over-simplification doesn’t really add anything.
Edit to add: Both the size of your codebase, and your choice of type system can vastly change the values on each of these dimensional axes as well.
The argument seems to rely on the cost of static typing, which is stated in the following four points that I challenge:
I don’t buy this argument at all. If you don’t think about correct types in a dynamic languages, you will run into trouble during testing (and production, when your tests aren’t perfect). You really have to get your types right in a dynamic language too. Arguably, with a statically typed language, you have to think less because compiler will catch your error. I think that’s the whole point of statically typed languages (performance concerns aside).
I’d have to see some proof to show that static typing plays a significant role in compile time. I’ll buy that you can make a very complicated (perhaps turing complete) type system and that would have a big impact. But there are statically typed languages that compile really fast, and most of the compile time is probably not spent on types. I’d argue that it is likely for the compiler to catch your error with types faster than you could compile, run, and test to find the same error with no types.
That may or may not be true. Sure, a type system can be very complicated. It doesn’t have to be. On the other hand, a dynamic language will still have types, which you need to learn and understand. Then, instead of learning to annotate the types in code, you learn to figure out type errors at run time. Is that so much easier?
Either way, I don’t believe type systems are an insurmountable barrier. And I think some people give the learning curve way too much weight. Maybe they are working on throwaway software on a constantly changing faddy tech stack, in a place with high employee turnover. It’ll matter more. I suppose there’s a niche for that kind of software. But I’m more into tech that is designed for software that is developed, used, and maintained for years if not decades. A little bit of extra learning up front is no big deal and the professionals working on it will reap the benefits ever after.
That might be the case with the current crop of languages with clever type system, though I don’t know if it’s inherent. Do static type system need to be so powerful (read: complicated) however? A simpler system can get you just as much type safety, at the expense of some repetition in code.
–
I think there are dimnishing returns, but not due to the cost of static typing as such, but rather due to the fact that types just don’t catch all errors. Once the low hanging fruit is out, there’ll be proportionally more and more logic errors and other problems that aren’t generally prevented with types. Or you could catch these with extensive type annotation, but the likelihood of preventing a real problem becomes small compared to the amount of annotation required. And then there’s the usual question: who checks the proof?
There have been some famous bugs that resulted from systems using different units. So if these numeric quantities were properly typed, these bugs would have been prevented. However, what if we change the scenario a little, and suppose we’re measuring fuel or pressure, in the right units. But we read the wrong quantity – spent fuel instead of stored fuel, or exterior pressure instead of interior pressure? Sure you can add more types to prevent such misuse, but it gets more and more verbose, and then you’re moving closer and closer to re-expressing (and thus enforcing) the program logic in the language of the type system; we could consider that to be a language of its own.
Now you have two programs, and one can prevent bugs in the other, but both could still be buggy. And the other program starts to grow because you start needing explicit conversions to enable the code to actually perform a computation on internal-pressure-in-pascal. Of course you are subverting the type system when you say you really want to convert internal-pressure-in-pascal to just pressure-in-pascal or whatever. Bugs ahoy?
I agree with most of the rest of your comment, but this part is untrue. Stronger type systems do allow you to enforce more powerful laws at compile time. At one end of the curve we have a type system like C’s, which barely buys you anything, and then at the other end we have full dependent types where you can prove arbitrary invariants about your code (this function always terminates, this value is always even, etc.) that you cannot prove in a weaker type system. In between is a huge spectrum of safety checking power.
The C type system can actually be quite powerful if you wrap basic types in one element structs. struct meter { int v; } and struct foot { int v; } can’t be added by mistake, but can still be worked with using one line inline functions with no performance penalty. It’s just work (which nobody likes).
I would not describe that as “quite powerful” at all. That’s one of the most basic things a type system can give you.
You can’t really prove any interesting properties until you at least have proper polymorphism. Java doesn’t, for example, because every object can be inspected at runtime in certain ways. In a sensible type system, there are no properties of objects except those which are explicitly stated in the type of the object.
In such a type system, you can prove interesting properties like that a data structure does not “depend” in any way on the objects in contains. For example, if you could implement a function
Which “mapped over” the contents of your object with some function, this would prove that your object never inspects its contents and therefore its structure does not depend on the values of its contents (because this function is universally quantified over ‘b’, and therefore you could map every ‘a’ to a constructed type which cannot be inspected in any way).
You can prove all sorts of useful properties like this (often without even realize you’re doing it) once you have proper quantification in your type system. One of the coolest quantification-based proofs I know of is that Haskell’s ST monad is extrinsically pure.
As you add more power to your type system (up to full dependent types, linear types, etc.) you can prove more and more useful things.
As long as you like all your types disjoint, sure. But I’ll pass.
So what’s wrong with disjoint types?
It doesn’t you have rationals and floats that are both numbers for example.
In Ocaml ints and floats are different types and operators like (+) only apply to ints, one has to use (+.) for floats. It’s not a problem IME.
I think automatic type conversion of ints to reals was the original sin of FORTRAN.
In mathematics the system Z of integers and the system R of reals are different. The number 3 has different properties depending on system context - for example 3x = 1 has a solution in the second context.
But it lacks a keyword connection to category theory.
That’s a good point and one that took me a long time to learn: if a concept cannot be expressed in a language, it doesn’t magically disappear and absolve the programmer from thinking about it. Types are one example as you mention; similarly, in many discussions about Rust, some people mention that the borrow checker is an impediment to writing code. It’s true that some programs are rejected by the compiler, but lifetime and ownership are also concerns in C programs as well. The main differences are that in Rust you have rules and language constructs to talk about those concerns while in C it’s left to documentation and convention.
OCaml is a good example of this.
It’s true that you have to get the types right in a dynamic language, but the appeal of dynamic languages isn’t that you don’t have to think about types. It’s that you don’t have to think about the shape of types. For example:
What type should that return? Contrived, but it’s not the gnarliest type problem I’ve run into. Sometimes it’s nice to have a language where I can give up on getting the types right and rely on tests and contracts to check it.
How do you use a value without thinking about it’s type or shape?
In your example, you can’t just blindly apply numerical operation to first element of that horror array since it might be another array. So, if you wanted to get to the value inside of those nested arrays, you’d need to think about how you would “strip” them off, wouldn’t you? And wouldn’t it mean that layers of nesting have some special meaning for us?
Taking your implementation as reference:
we can write a Haskell version that distinguishes between a value nested in a “layer” and a value by itself:
and if we don’t need layers anymore, we can get value out pretty easily:
Assuming it’s correct, it should return whatever the type inference engine chooses for you :)
This is because type theory is confused about what programs do - which is operate on bit sequences (or, these days, byte sequences). These sequences may be representations of mathematical objects or representations of things that are not mathematical objects, but they remain representations, not actual ideal mathematical objects.
Aren’t a lot of type systems proven type-correct nowadays?
The type system can be fine but the rules you define with the types could be flawed. Thus, you can still write flawed programs that the type system can’t prevent because the types were defined incorrectly.
Can you give an example? I’m not sure exactly what breed of incorrect types you’re referring to.
One thing I am learning from working with inexperienced developers is that even thinking about which container type you are using is a challenge. Should your function return a
Seq? AnArray? AnIterator? AGenerator? And what if your new library returns aGeneratorand the old one returned anIteratorand now you have to rewrite all your declarations for seemingly no reason at all? Some kind of “most general type” restriction/requirement/tool would help with this…This is one of the things I think Go does really well (in spite of having a generally quite weak type system) - thanks to implicit interfaces, you can just return the concrete type you’re using and the caller will automatically pick up that it ‘fits’.
This sort of works – but even with that system, it’s easy to declare one’s types too tightly.
It depends in part on how granular the collection library’s interfaces are (ditto for numeric tower, effects tracking, monad wizard tool).
I’m unclear what you mean. Many languages offer two solutions. You can declare the variable IEnumerable or whatever as appropriate. Or you declare the variable as “whatever type the initializer has”.
When in doubt, use the inference!
It is sometimes easy to choose wrong.
IterablevsIteratorvsEnumerableI think one reason this whole debate irks me is the unspoken belief that programming languages need to feed the beast of productivity, which always demands results faster and cheaper. (He does mention different domains in the article.) Any language that presents any sort of negative feedback on correctness of code is seen as a hindrance.
I’m not arguing for poor developer UX, I’m arguing that the “throw code at the wall and keep what sticks” mentality is stupid and not the way to build a system.
Ummm, I’m old and crotchety, and one of my cats is sick, so take this with pinch of salt.
“SRE, Go Programmer, Mathematician.”
I beg of you, Software Engineers, Computer Scientists or anyone in the field, pleeeease don’t self-identify with one language. It breaks my heart. There are vast tracts of land to explore!
As far as the post though, it’s weird though, although I enjoy programming in loosely typed or dynamically typed languages occasionally, I’ve generally had just as much, if not more productivity in statically typed environments. Especially in these days of editors that fully understand the AST and type flow.
So, as far as increasing compile times… I don’t even need to compile very often these days - well not until I can already see that the thing compiles - the tools are that good.
Even without the fancy editors though, seeing really strong concrete types explicitly in the code is a wonderful form of documentation that is really beneficial to others that have to maintain things years down the line. Personally I only begrudgingly accepted auto’s and var’s in the last five years although I do have to concede they do make refactoring more convenient and save key presses.
All in all, it seems like he is really torn up and like he’s trying to convince himself or his boss one way or the other. I kind of feel for the guy actually :/
I’m still trying to convince our hiring people that advertising for “ruby programmer” or “Javascript programmer” is like advertising for “hammer user” instead of “carpenter”
I think this is a fascinating point. Strongly typed languages, especially those that separate side effects, don’t really need to be fully compiled to reason about, at least in byte-sized pieces.
“The value of static typing is subjective” might be a better name for this article. Implying that static typing has diminishing returns is counter to the argument of the post.
How is it counter? It’s how the author is able to believe that Go has the Goldilocks amount of type checking. If benefits didn’t diminish they’d have to agree that generic containers are important.
The thesis of the post is that the value of static typing is subjective. And there are some graphs that the author believes are universal. But there is not reason to think one’s subjective value of static typing requires the benefits diminish or match those graphs.
“Correct code velocity” is not a function of “number of keypresses” nor is it “number of times I have to change what I wrote to convince the type system to attempt it”. It’s a mix of many more things as well:
I could go on forever. Not only do these things affect performance in both speed and quality, but they affect each other as well. It’s a giant combinatorial problem space, and this sort of inch-deep over-simplification doesn’t really add anything.
Edit to add: Both the size of your codebase, and your choice of type system can vastly change the values on each of these dimensional axes as well.