[Haskell-cafe] Re: Problems with strictness analysis?

[wren ng thornton]

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