5 ms·

What to know before debating type systems

55 points by brooksbp 17y ago

ohwaitnvm 17y ago
I was debating type systems with a fellow student the other day, and there seemed to be a sort of disconnect in the meanings of the different labels we applied to one another's preferences and arguments. This article definitely helped me see more of the other side of the debate (Mine being that of a hardcore Rubyist amd his of Java) and understand the disconnect we were having in discussion. A worthwhile read for sure.
moe 17y ago
Informative, balanced and very well written.
ubernostrum 17y ago
Unfortunately, the author seems to be on the verge of falling into one of the fallacies he rightly points out: assuming that one of the main purposes of unit testing is to act as a surrogate for static analysis. I've seen code written in dynamically-typed languages which tries to do this, and such code pretty much universally falls into the category of "using dynamically-typed languages poorly" (particularly since pretty much every popular dynamically-typed language has lint tools which will catch the sorts of things paranoid static-typing aficionados try to test for). What unit tests are good at, and what they should be used for, is verifying behavior and integration, something that static type systems notably still aren't particularly good at (and likely will never be good enough at for practical purposes -- I believe quite firmly that there's a diminishing-returns effect from ever-more-powerful type systems). In general, though, I like to think of static type systems existing in relation to their programming languages in much the same way that metalanguages exist in relation to object languages in logic: the type system is essentially a separate language in which you can express and then verify statements about the program, just as a metalanguage allows you to express and verify statements about its object language. This carries with it, of course, various implications for the limits of type systems (particularly since metalanguages are notoriously prone to infinite regress -- eventually you need a metametalanguage to make statements about the metalanguage, then a metametametalanguage and so on); I'm fairly certain that any sufficiently powerful type system would need to end up being a Turing-complete programming model in its own right, and since I've already got one of those (I'm writing my program in it) I generally pass on that and just write the unit tests :)
- camccann 17y ago
  I'm fairly certain that any sufficiently powerful type system would need to end up being a Turing-complete programming model in its own right, and since I've already got one of those (I'm writing my program in it) I generally pass on that and just write the unit tests :) Programming language designers are way ahead of you on that one! If memory serves me, C++ templates and type inference in Haskell and ML are all Turing complete. Then again, in a world where XML transforms and typesetting are Turing complete, this isn't too shocking, I guess...
  - kingkilr 17y ago
    C++ templates are turning complete.
- silentbicycle 17y ago
  The flip side of this, I think, is that you may get 90% of the overall benefit of static typing from just checking boundaries between modules and other fundamental static analysis, not the really far out stuff that makes for cutting-edge research papers. While it can do some really impressive things after that, there may be diminishing returns. I'm not a type system expert by any means, and I didn't really see what the point of static typing was until I learned OCaml, but I wonder if there's a practical middle ground here. Perhaps dynamic typing with optional inferred types or declarations.
  - kscaldef 17y ago
    OCaml and Haskell seem to strike a pretty good middle ground to me. Powerful, but generally inferred static types. Haskell is a bit more concise, so I think it can be more appealing to the dynamic language crowd. The major objection people to have to HM-style type systems seems to boil down to "the compiler is forcing me to fix my bugs before it will run my code", which seems a bit silly. It seems doubly silly when it comes from people who advocate TDD or other variations on tests-first.
    - silentbicycle 17y ago
modelic3 17y ago
Really nice read, quite easygoing.
gruseom 17y ago
I agree that it's a good article. Its primary point, that "type" doesn't mean the same thing in "statically typed" and "dynamically typed", is well put. The model he presents of static typing taking a proof-based approach to correctness while dynamic typing takes a test-based approach is also interesting. It's quite wrong, though, to say that the modern unit testing school (i.e. xUnit and TDD) is a creature of the dynamically typed world. It is very much a creature of the Java world. It's true that the original xUnit was Smalltalk's, but that was a pale foreshadowing of Junit. And all the examples from Beck's TDD book were in Java. The most zealous unit-testers may be Rubyists, but their numbers are surely dwarfed by the number of people programming in that style in Java and .NET. I did so in C# for years myself. Edit: he also is far too dismissive of the importance of performance. (Alex Payne's talk about choosing Scala is a nice counterexample since it was posted yesterday). I'm beginning to think the piece is less insightful than it first appears.
- gnaritas 17y ago
  > And all the examples from Beck's TDD book were in Java. One has to make a living. > but their numbers are surely dwarfed by the number of people programming in that style in Java and .NET. Doubtful. To quote Kent himself, "Even allowing for my marketing and sales mistakes, the data suggests that there are at most a few thousand Java programmers actively practicing TDD." Which is why he stopped developing jUnitMax http://www.threeriversinstitute.org/blog/?p=291 http://www.threeriversinstitute.org/blog/?p=291 Java just doesn't have a TDD culture, nor does C# really.
  - gruseom 17y ago
    Your two points are contradictory. It's true that I'm guessing at the numbers. (Who isn't? The post you reference doesn't include any data.) But that doesn't affect the point that the OP is obviously wrong to say "the whole unit testing movement basically came out of dynamically typed languages".
    - silentbicycle 17y ago
      The points aren't necessarily contradictory. There are probably tons of programmers who buy books about various fashionable methodologies but don't continue using them in the long run. Writing the examples in Java would make sense as a lingua franca, even if he didn't believe that TDD would be adopted by the Java community.
aufreak 17y ago
The author says that simply typed lambda calculus proves that programs terminate. That sounds to me like saying "simply typed lambda calculus is not Turing-complete". Disclaimer: I know basics of lambda calculus but don't exactly know what the "simply typed" one is.
- camccann 17y ago
  You are correct, it's not. In the simply-typed lambda calculus, generally recursive constructs (such as fixed-point combinators like our friend Y) do not have valid types and are not legal. Wikipedia has a nice article on it: http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus
blasdel 17y ago
Something I've always thought would make this classic article better is a good old s/typed/type-checked/g Both static and dynamic type-checking can be easily implemented for most programs in nearly every language. Plenty of statically type-checked language implementations build in support for RTTI and runtime casts (dynamic type checks galore!). Plenty of language implementations that do pervasive dynamic type-checks have modules for accessing the AST (upon which you can perform static type-checks!). It's not always easy to add sound static type-checking, for sure. In some language implementations it's impossible to implement dynamic type-checks that make any sense without major greenspunning (eg. Haskell and type erasure). But your language's native type system is not your program's destiny!
fauigerzigerk 17y ago
It's a good article but he creates a new fallacy himself, which is that performance becomes less important over time. It only becomes less important for the exact same things we did in the past or for equally (computationally) simple things. But faster machines can be used to do things we couldn't do in the past, and my own opinion is that these are the interesting things. So I think, generally, the importance of performance doesn't change much over time.
- camccann 17y ago
  I agree with you about the "interesting things", but those aren't the majority of things by a good margin. The overwhelming majority of code written today is likely limited primarily by I/O, such as waiting on user input, network speed, disk speed, &c. Also, most slower languages these days are explicitly designed with the ability to call into code written in a faster language, which means that with some profiling and a few dozen lines of C many applications can get 90+% of the speed of a fast language while still being written almost entirely in the trendy interpreted language of your choice. Which reminds me, how many people in "the real world" actually profile their programs? I bet a lot of performance gains could be found that way in any language.
  - silentbicycle 17y ago
    > Which reminds me, how many people in "the real world" actually profile their programs? I bet a lot of performance gains could be found that way in any language. Not enough, I'd say. Particularly since just scrutinizing the first few things a profiler catches can make a tremendous difference. For example, in an hour of profiling and tuning a project of mine, I fixed two hotspots that each led to an independent 20x speedup. 400x total. Half the runtime is just disk IO now.
  - fauigerzigerk 17y ago
    The reason why the interpreted language + C = 90% speed equation has never quite worked out for me is that much of the speed advantage of compiled languages comes from lower memory consumption. Python's __slots__, collections.namedtuple, array and struct modules do help a lot to reduce memory consumption. Sadly, it's not nearly good enough to write significant parts of my code in Python (which I would love to do)
lsd5you 17y ago
Dynamically typed languages are automobiles and statically typed are bicyles?? Not exactly a neutral comparison and hypocracy in light of his complaints against the strong vs. weak labels. Isn't it fair to say statically typed languages are still faster but are generally heavier and less agile. So surely the inverse is a much better analogy. Or is it that dynamic are more modern? In which case may I propose: statically typed languages are automobiles and dynamically typed languages are segways! (I kid).
- mgreenbe 17y ago
  Dynamically typed languages are automobiles and statically typed are bicyles?? Not exactly a neutral comparison and hypocracy in light of his complaints against the strong vs. weak labels. Good thing he didn't make it. Please read the article next time. Here's the relevant quote: [Obsessively tracking type information in dynamic languages] prevents a programmer from realizing the benefits of dynamic typing. It's like buying a new car, but refusing to drive any faster than a bicycle. The car is horrible; you can't get up the mountain trails, and it requires gasoline on top of everything else. Indeed, a car is a pretty lousy excuse for a bicycle! Similarly, dynamically typed languages are pretty lousy excuses for statically typed languages. The point the author is making is that some programmers may have been frustrated by dynamic languages because they didn't allow their programs to fail, i.e., with runtime type errors. I disagree with the author's point---I've never heard of anyone having that problem---but you've woefully misunderstood what the author says.
  - lsd5you 17y ago
    I don't want to be argumentative - its only a light hearted comment - but i did of course read the article. I just interpreted something differently to yourself. I read it again, and the analogy is still there. Car is to dynamic typing as bicycle is to ... anyway ... you can play down its significance or ambiguity, but i'd need convincing that its not there at all.
    - mgreenbe 17y ago
azgolfer 17y ago
IMO Gilad Bracha is the best guy to listen to on types http://wwhttp://www.se-radio.net/podcast/2009-07/episode-140-newspeak-and-pluggable-types-gilad-brachaw.se-radio.net/podcast/2009-07/episode-140-newspeak-and-pluggable-types-gilad-bracha http://wwhttp://www.se-radio.net/podcast/2009-07/episode-140...

55 points by brooksbp 17y ago

I was debating type systems with a fellow student the other day, and there seemed to be a sort of disconnect in the meanings of the different labels we applied to one another's preferences and arguments. This article definitely helped me see more of the other side of the debate (Mine being that of a hardcore Rubyist amd his of Java) and understand the disconnect we were having in discussion. A worthwhile read for sure.

moe 17y ago

Informative, balanced and very well written.

ubernostrum 17y ago

Unfortunately, the author seems to be on the verge of falling into one of the fallacies he rightly points out: assuming that one of the main purposes of unit testing is to act as a surrogate for static analysis. I've seen code written in dynamically-typed languages which tries to do this, and such code pretty much universally falls into the category of "using dynamically-typed languages poorly" (particularly since pretty much every popular dynamically-typed language has lint tools which will catch the sorts of things paranoid static-typing aficionados try to test for). What unit tests are good at, and what they should be used for, is verifying behavior and integration, something that static type systems notably still aren't particularly good at (and likely will never be good enough at for practical purposes -- I believe quite firmly that there's a diminishing-returns effect from ever-more-powerful type systems). In general, though, I like to think of static type systems existing in relation to their programming languages in much the same way that metalanguages exist in relation to object languages in logic: the type system is essentially a separate language in which you can express and then verify statements about the program, just as a metalanguage allows you to express and verify statements about its object language. This carries with it, of course, various implications for the limits of type systems (particularly since metalanguages are notoriously prone to infinite regress -- eventually you need a metametalanguage to make statements about the metalanguage, then a metametametalanguage and so on); I'm fairly certain that any sufficiently powerful type system would need to end up being a Turing-complete programming model in its own right, and since I've already got one of those (I'm writing my program in it) I generally pass on that and just write the unit tests :)

camccann 17y ago
I'm fairly certain that any sufficiently powerful type system would need to end up being a Turing-complete programming model in its own right, and since I've already got one of those (I'm writing my program in it) I generally pass on that and just write the unit tests :) Programming language designers are way ahead of you on that one! If memory serves me, C++ templates and type inference in Haskell and ML are all Turing complete. Then again, in a world where XML transforms and typesetting are Turing complete, this isn't too shocking, I guess...
- kingkilr 17y ago
  C++ templates are turning complete.
silentbicycle 17y ago
The flip side of this, I think, is that you may get 90% of the overall benefit of static typing from just checking boundaries between modules and other fundamental static analysis, not the really far out stuff that makes for cutting-edge research papers. While it can do some really impressive things after that, there may be diminishing returns. I'm not a type system expert by any means, and I didn't really see what the point of static typing was until I learned OCaml, but I wonder if there's a practical middle ground here. Perhaps dynamic typing with optional inferred types or declarations.
- kscaldef 17y ago
  OCaml and Haskell seem to strike a pretty good middle ground to me. Powerful, but generally inferred static types. Haskell is a bit more concise, so I think it can be more appealing to the dynamic language crowd. The major objection people to have to HM-style type systems seems to boil down to "the compiler is forcing me to fix my bugs before it will run my code", which seems a bit silly. It seems doubly silly when it comes from people who advocate TDD or other variations on tests-first.
  - silentbicycle 17y ago

modelic3 17y ago

Really nice read, quite easygoing.

gruseom 17y ago

I agree that it's a good article. Its primary point, that "type" doesn't mean the same thing in "statically typed" and "dynamically typed", is well put. The model he presents of static typing taking a proof-based approach to correctness while dynamic typing takes a test-based approach is also interesting. It's quite wrong, though, to say that the modern unit testing school (i.e. xUnit and TDD) is a creature of the dynamically typed world. It is very much a creature of the Java world. It's true that the original xUnit was Smalltalk's, but that was a pale foreshadowing of Junit. And all the examples from Beck's TDD book were in Java. The most zealous unit-testers may be Rubyists, but their numbers are surely dwarfed by the number of people programming in that style in Java and .NET. I did so in C# for years myself. Edit: he also is far too dismissive of the importance of performance. (Alex Payne's talk about choosing Scala is a nice counterexample since it was posted yesterday). I'm beginning to think the piece is less insightful than it first appears.

gnaritas 17y ago
> And all the examples from Beck's TDD book were in Java. One has to make a living. > but their numbers are surely dwarfed by the number of people programming in that style in Java and .NET. Doubtful. To quote Kent himself, "Even allowing for my marketing and sales mistakes, the data suggests that there are at most a few thousand Java programmers actively practicing TDD." Which is why he stopped developing jUnitMax http://www.threeriversinstitute.org/blog/?p=291 http://www.threeriversinstitute.org/blog/?p=291 Java just doesn't have a TDD culture, nor does C# really.
- gruseom 17y ago
  Your two points are contradictory. It's true that I'm guessing at the numbers. (Who isn't? The post you reference doesn't include any data.) But that doesn't affect the point that the OP is obviously wrong to say "the whole unit testing movement basically came out of dynamically typed languages".
  - silentbicycle 17y ago
    The points aren't necessarily contradictory. There are probably tons of programmers who buy books about various fashionable methodologies but don't continue using them in the long run. Writing the examples in Java would make sense as a lingua franca, even if he didn't believe that TDD would be adopted by the Java community.

aufreak 17y ago

The author says that simply typed lambda calculus proves that programs terminate. That sounds to me like saying "simply typed lambda calculus is not Turing-complete". Disclaimer: I know basics of lambda calculus but don't exactly know what the "simply typed" one is.

camccann 17y ago
You are correct, it's not. In the simply-typed lambda calculus, generally recursive constructs (such as fixed-point combinators like our friend Y) do not have valid types and are not legal. Wikipedia has a nice article on it: http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus http://en.wikipedia.org/wiki/Simply_typed_lambda_calculus

blasdel 17y ago

Something I've always thought would make this classic article better is a good old s/typed/type-checked/g Both static and dynamic type-checking can be easily implemented for most programs in nearly every language. Plenty of statically type-checked language implementations build in support for RTTI and runtime casts (dynamic type checks galore!). Plenty of language implementations that do pervasive dynamic type-checks have modules for accessing the AST (upon which you can perform static type-checks!). It's not always easy to add sound static type-checking, for sure. In some language implementations it's impossible to implement dynamic type-checks that make any sense without major greenspunning (eg. Haskell and type erasure). But your language's native type system is not your program's destiny!

fauigerzigerk 17y ago

It's a good article but he creates a new fallacy himself, which is that performance becomes less important over time. It only becomes less important for the exact same things we did in the past or for equally (computationally) simple things. But faster machines can be used to do things we couldn't do in the past, and my own opinion is that these are the interesting things. So I think, generally, the importance of performance doesn't change much over time.

camccann 17y ago
I agree with you about the "interesting things", but those aren't the majority of things by a good margin. The overwhelming majority of code written today is likely limited primarily by I/O, such as waiting on user input, network speed, disk speed, &c. Also, most slower languages these days are explicitly designed with the ability to call into code written in a faster language, which means that with some profiling and a few dozen lines of C many applications can get 90+% of the speed of a fast language while still being written almost entirely in the trendy interpreted language of your choice. Which reminds me, how many people in "the real world" actually profile their programs? I bet a lot of performance gains could be found that way in any language.
- silentbicycle 17y ago
  > Which reminds me, how many people in "the real world" actually profile their programs? I bet a lot of performance gains could be found that way in any language. Not enough, I'd say. Particularly since just scrutinizing the first few things a profiler catches can make a tremendous difference. For example, in an hour of profiling and tuning a project of mine, I fixed two hotspots that each led to an independent 20x speedup. 400x total. Half the runtime is just disk IO now.
- fauigerzigerk 17y ago
  The reason why the interpreted language + C = 90% speed equation has never quite worked out for me is that much of the speed advantage of compiled languages comes from lower memory consumption. Python's __slots__, collections.namedtuple, array and struct modules do help a lot to reduce memory consumption. Sadly, it's not nearly good enough to write significant parts of my code in Python (which I would love to do)

lsd5you 17y ago

Dynamically typed languages are automobiles and statically typed are bicyles?? Not exactly a neutral comparison and hypocracy in light of his complaints against the strong vs. weak labels. Isn't it fair to say statically typed languages are still faster but are generally heavier and less agile. So surely the inverse is a much better analogy. Or is it that dynamic are more modern? In which case may I propose: statically typed languages are automobiles and dynamically typed languages are segways! (I kid).

mgreenbe 17y ago
Dynamically typed languages are automobiles and statically typed are bicyles?? Not exactly a neutral comparison and hypocracy in light of his complaints against the strong vs. weak labels. Good thing he didn't make it. Please read the article next time. Here's the relevant quote: [Obsessively tracking type information in dynamic languages] prevents a programmer from realizing the benefits of dynamic typing. It's like buying a new car, but refusing to drive any faster than a bicycle. The car is horrible; you can't get up the mountain trails, and it requires gasoline on top of everything else. Indeed, a car is a pretty lousy excuse for a bicycle! Similarly, dynamically typed languages are pretty lousy excuses for statically typed languages. The point the author is making is that some programmers may have been frustrated by dynamic languages because they didn't allow their programs to fail, i.e., with runtime type errors. I disagree with the author's point---I've never heard of anyone having that problem---but you've woefully misunderstood what the author says.
- lsd5you 17y ago
  I don't want to be argumentative - its only a light hearted comment - but i did of course read the article. I just interpreted something differently to yourself. I read it again, and the analogy is still there. Car is to dynamic typing as bicycle is to ... anyway ... you can play down its significance or ambiguity, but i'd need convincing that its not there at all.
  - mgreenbe 17y ago

azgolfer 17y ago

IMO Gilad Bracha is the best guy to listen to on types http://wwhttp://www.se-radio.net/podcast/2009-07/episode-140-newspeak-and-pluggable-types-gilad-brachaw.se-radio.net/podcast/2009-07/episode-140-newspeak-and-pluggable-types-gilad-bracha http://wwhttp://www.se-radio.net/podcast/2009-07/episode-140...