3 ms·

There is plenty of work in PL that covers why type theory is useful. Check out the classic paper by Philip Wadler called "Theorems for free" that covers some of

There is plenty of work in PL that covers why type theory is useful. Check out the classic paper by Philip Wadler called "Theorems for free" that covers some of the terrific benefits of parametric polymorphism. There has also been a good amount of discussion generated by organizations such as Jane Street concerning the benefits of static typing and type inference in practice. Notably, the free documentation (that is completely coupled with the code) that you get when you design software that takes advantage of the type system.

seanmcdirmid 11y ago
Wadler's work is great, I've seen his talk on this many times (where he has the lambda shirt on), but it doesn't really cover "why it is useful" just "why it is inevitable". Really, how would you scientifically show that parametric polymorphism is "useful?" "Useful" isn't a very empirical property, it isn't something you can reliably measure. In a scientific paper, you can't just say something like: > When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. without justification! You have a citation, or perhaps it is something just accepted universally (which it isn't, of course). At the very least, you have to weaken the statement a bit...like: > When it comes to maintaining and evolving these systems, the lack of explicit static typing is probably a bottleneck. You can't talk in absolutes without evidence. But you know, the benefits of static typing are clear via anecdotal experience, we only really argue about whether or not the benefits balance out the disadvantages of static typing (and how those disadvantages can be mitigated, and if that is enough...). Again, in arguing about this we are firmly in the area of design and not science.
- iheartmemcache 11y ago
  With regards to definitive benefit that's backed up by scientific study (rather than just anecdote)-- the UK's Ministry of Defense commissioned a study (IV&V) on the error rate of long-lived code comparing C code bases (static but not too strict) vs Ada (static and fairly strict). They presented their findings Ada-Europe 2001. There was about a 1 to 10 error ratio. They subset the Ada code into formally verified by SPARK code, and the error rate -- I kid you not -- dropped another order of magnitude. I'd assert based on that study static typing is definitively more reliable when your problem domain is set in stone [the operational semantics of flight, stock markets, power plants]. Of course that doesn't extend to any 'exploratory' computing where your domain isn't strictly (pardon the pun) defined. RE: Parametric polymorphism being "useful" - a pedant like me would claim for it to be of use, one has to demonstrate one clear instance of PP being of use - trivial or not - after which PP gains the attribute "useful" ;)
  - kazinator 11y ago
    Based on that study I would assert that tight static typing is more reliable than static typing that is full of holes. It doesn't speak to strong dynamic versus strong static at all. Speaking of holes, of course dynamic typing can have holes also: if an interpreter or compiler misses a type check, the consequences are that the wrong operation is applied to an object. The result is corruption, crashing. The correctness and completeness of a type scheme is orthogonal to static versus dynamic.
  - seanmcdirmid 11y ago
    This UK study is an anecdotal data point. It is not a controlled study, it is just comparing project A to project B that differ, among other thing in the languages they were written in (and probably much more!). It doesn't tell us very much for sure, but again adds to the anecdotes that can shape our judgement. Of course, useful has a low bar, but it also has a magnitude (X is useful if it is used, it might not be very useful though). Incidentally, stock markets have been big on Lisp and Smalltalk, two languages not known for static typing. It turns out that language X is always used in the stock market, where X is the latest hot language (Scala, Haskell, Clojure...).
kazinator 11y ago
Are these advanced theorem proving benefits obtainable with static typing alone, or does everything also have to be effect free ("purely funtional")?
- sgeisenh 11y ago
  Formally, everything has to be effect free; furthermore, everything has to be strict (the potential for any value to be "bottom" breaks things). You can apply the same intuition and things mostly work, but there can be a few surprises. These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.

seanmcdirmid 11y ago

Wadler's work is great, I've seen his talk on this many times (where he has the lambda shirt on), but it doesn't really cover "why it is useful" just "why it is inevitable". Really, how would you scientifically show that parametric polymorphism is "useful?" "Useful" isn't a very empirical property, it isn't something you can reliably measure. In a scientific paper, you can't just say something like: > When it comes to maintaining and evolving these systems, the lack of explicit static typing becomes a bottleneck. without justification! You have a citation, or perhaps it is something just accepted universally (which it isn't, of course). At the very least, you have to weaken the statement a bit...like: > When it comes to maintaining and evolving these systems, the lack of explicit static typing is probably a bottleneck. You can't talk in absolutes without evidence. But you know, the benefits of static typing are clear via anecdotal experience, we only really argue about whether or not the benefits balance out the disadvantages of static typing (and how those disadvantages can be mitigated, and if that is enough...). Again, in arguing about this we are firmly in the area of design and not science.

iheartmemcache 11y ago
With regards to definitive benefit that's backed up by scientific study (rather than just anecdote)-- the UK's Ministry of Defense commissioned a study (IV&V) on the error rate of long-lived code comparing C code bases (static but not too strict) vs Ada (static and fairly strict). They presented their findings Ada-Europe 2001. There was about a 1 to 10 error ratio. They subset the Ada code into formally verified by SPARK code, and the error rate -- I kid you not -- dropped another order of magnitude. I'd assert based on that study static typing is definitively more reliable when your problem domain is set in stone [the operational semantics of flight, stock markets, power plants]. Of course that doesn't extend to any 'exploratory' computing where your domain isn't strictly (pardon the pun) defined. RE: Parametric polymorphism being "useful" - a pedant like me would claim for it to be of use, one has to demonstrate one clear instance of PP being of use - trivial or not - after which PP gains the attribute "useful" ;)
- kazinator 11y ago
  Based on that study I would assert that tight static typing is more reliable than static typing that is full of holes. It doesn't speak to strong dynamic versus strong static at all. Speaking of holes, of course dynamic typing can have holes also: if an interpreter or compiler misses a type check, the consequences are that the wrong operation is applied to an object. The result is corruption, crashing. The correctness and completeness of a type scheme is orthogonal to static versus dynamic.
- seanmcdirmid 11y ago
  This UK study is an anecdotal data point. It is not a controlled study, it is just comparing project A to project B that differ, among other thing in the languages they were written in (and probably much more!). It doesn't tell us very much for sure, but again adds to the anecdotes that can shape our judgement. Of course, useful has a low bar, but it also has a magnitude (X is useful if it is used, it might not be very useful though). Incidentally, stock markets have been big on Lisp and Smalltalk, two languages not known for static typing. It turns out that language X is always used in the stock market, where X is the latest hot language (Scala, Haskell, Clojure...).

kazinator 11y ago

Are these advanced theorem proving benefits obtainable with static typing alone, or does everything also have to be effect free ("purely funtional")?

sgeisenh 11y ago
Formally, everything has to be effect free; furthermore, everything has to be strict (the potential for any value to be "bottom" breaks things). You can apply the same intuition and things mostly work, but there can be a few surprises. These theorems are a huge part of the "if it compiles it must be correct" feeling that functional programming often provides.