[Haskell-cafe] Re: Problems with strictness analysis?
wren ng thornton
wren at freegeek.org
Thu Nov 6 01:57:15 EST 2008
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. 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 and
Phil Wadler have certainly done very similar work.
More information about the Haskell-Cafe