4 ms·
One reason is that more general types mean you can write fewer functions, and so the function that you do write is more likely to be correct. The function `int
by endgame 8y ago
One reason is that more general types mean you can write fewer functions, and so the function that you do write is more likely to be correct.
The function `intMap :: (Int -> Int) -> [Int] -> [Int]` can do all sorts of crazy things that are not map. The function `map :: (a -> b) -> [a] -> [b]` can do far fewer crazy things, and just from looking at the type you can say that any `b` in the result list _must_ have come from applying the function to some `a` in the input list.
- gmfawcett 8y ago> you can say that any `b` in the result list _must_ have come from applying the function to some `a` in the input list. Morally correct... but consider the function `\f xs -> [undefined]`, which can be typed as `(a -> b) -> [a] -> [b]`. (Obviously it could be given other types as well.)
- Zalastax 8y agoWhen discussing Haskell and theorems about its types it's common to simply ignore non-termination; if we don't ignore non-termination there's basically nothing we can say about Haskell programs at all. Interested readers should check out Agda and Theorems for free!
- gmfawcett 8y agoFair enough. On reflection, `\f xs -> []` is a better example of the point I was trying to make.
- Zalastax 8y agoYeah that's a better one (which I think is discussed (or a similar one) in Theorems for free!), but the wording of OP weasels itself out of that being a problem. > any `b` in the result list _must_ have come from applying the function to some `a` in the input list. Since there exists no a in [], the quoted statement holds! I find that really beautiful :)
- gmfawcett 8y agoThat is indeed a weaselly but accurate statement. :) I'll have to give Theorems for Free a read, thanks for the suggestion!