3 ms·
When 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
by Zalastax 8y ago
When 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!