Luke Palmer wrote:
The example being discussed in this thread is a good one:
sum [1..10^8] + length [1..10^8]
With Haskell's semantics, we know we can write this as:
let xs = [1..10^8] in sum xs + length xs
But it causes a change in memory *complexity*, so in some sense these two sentences are not equal. What is the theory in which we can observe this fact? Is it possible to give a simple denotational semantics which captures it?
There's actually been a good deal of work on trying to mathematize this sort of issue, under the name of linear logic[1]. The problem with classical equational reasoning is that it doesn't capture the notion of "resources" or the "sharing" thereof. The two expressions are not the same because the first has two [1..10^8] resources it can use up, whereas the later only has one. Depending on the balance between sharing temporal work vs minimizing memory overhead, sometimes it's okay to add sharing and other times it's okay to remove it, but in general both options are not available at once. It's pretty easy to capture issues of economy with LL, though making a rewriting system takes a bit more framework. I'm not sure to what extent LL has been explored as a semantic model for programs, but Clean[2] and Phil Wadler[3] have certainly done very similar work. [1] http://en.wikipedia.org/wiki/Linear_logic [2] http://www.st.cs.ru.nl/Onderzoek/Publicaties/publicaties.html [3] http://homepages.inf.ed.ac.uk/wadler/topics/linear-logic.html -- Live well, ~wren