[Haskell-cafe] Automatic file closing after readFile

[Duncan Coutts]

On Sun, 2007-10-21 at 17:15 -0400, Albert Y. C. Lai wrote:
> Magnus Therning wrote:
> > I'll certainly try to look into all of that.  However, I suspect your
> > suggestion doesn't scale very well.  On my original code it's easy, it
> > was less than 10 lines, but how do I know where to start looking if it's
> > a program of 100 lines, or 1000 lines?  The problem could occur in an
> > updated library that I just use... Well you get the idea :-)
> 
> A library function is supposed to tell you its time usage, memory usage, 
> file usage, ... generally resource usage, as part of its specification.
> 
> A 100-line program is not supposed to be a monolith. It is supposed to 
> be a combination of 10 functions (or 10 parts; I'll call them functions 
> anyway), 10 lines each. Each function is supposed to come with its 
> specification too, which again tells you its resource usage.
> 
> To reason about the 100-line program, you only need to reason about 10 
> lines of specifications.

I'm not sure what semantics we would use to reason about resource use in
specifications like this. Our standard semantics abstract over space,
time and sharing properties of our programs.

For a lazy language, resource specifications of functions do not compose
in a simple way. For example we might naively say that [1..m] uses m
time and space and that take n takes at most n time and space but then
take n [1..m] does not take the sum of these two time/space
specifications. In more complex examples the connection is even less
obvious.

One more accurate way to look at resource use is to say that we only
consider time and space to reduce to WHNF and then ask that question
when we apply various evaluation functions to the expression. Different
evaluation functions would force various parts of the value. Then when
we plug an expression into different contexts we see what kind of
evaluation function that context is and use that in our question about
the resource use to evaluate the expression. Still, that only gives you
total resource use, not maximum resource use at any point during
evaluation which is important for space.

Summary: it's not so simple.

Duncan