3 ms·
If you're hoping to catch a specification error, don't use a type like `Integer -> Integer`, which doesn't capture the specification except in a most general se
by dons 14y ago
If you're hoping to catch a specification error, don't use a type like `Integer -> Integer`, which doesn't capture the specification except in a most general sense.
Just as you should write good tests, that actually test for useful properties, so you should write good types -- and get useful proofs back from the compiler as a result.
- kingkilr 14y agoI wasn't trying to catch the error of "program author is a moron who doesn't know the difference between Fibonacci and factorial". Were I trying to catch that error I would have been aware of it, and then much less likely to write the bug in the first place. This is a truism that is well accepted by testing proponents: which tests you write are incredibly important, and you need to write your tests first in order to avoid a curve fitting problem (so to speak). Any non-trivial test would have shown my function to be very broken, what type would you have used to represent that so it wouldn't compile?
- dons 14y agoNumerical algorithms suffer from a paucity of types. So either you enrich your numerical type hierarchy, or you prove an implementation matches a model, e.g. for fibonacci http://stackoverflow.com/a/8434107/83805 http://stackoverflow.com/a/8434107/83805
- kingkilr 14y agoI don't have a response to that, other than to say, now you know why I decided to write compilers instead of pursue a graduate degree in computer science.
- swah 14y agoVery elegant way to show a point...
- Symmetry 14y agoThe point about a static type system not catching all errors is well taken[1], but if a programmer has mixed up factorial and Fibonacci I would expect that their tests would reflect this as well as their code. This is more the sort of thing you should rely on code reviews to spot. [1] Isn't the old joke in Haskell "If your program compiles it probably does something someone would find useful, but not necessarily the useful thing you want"