On 15-Jun-1998, Peter White <peter@galois> wrote:
>
> On June 15, Fergus Henderson writes
>
> > As noted earlier, things like heap overflow, and stack overflow
> > are different from other kinds of exceptions. They can't be modelled
> > using the domain-theoretic semantics. Rather, they reflect the failure
> > of the operational semantics to accurately reflect the domain-theoretic
> > semantics. Thus the treatment of these exceptions may need to be
> > different to the treatment of ordinary exceptions.
>
> One of the advertisements of Haskell is that you can reason
> about your program, by performing mathematical proofs about
> the program. Haskell has gone a long way to incorporating IO
> and stateful computations in such a way that you still get
> referential transparency, and you can still reason about programs.
> If the operational semantics fails to reflect, the domain-theoretic
> semantics, then it would appear that the ability to reason about
> the programs dissappears.
This is not the case here. The reason is that although the operational
semantics are not complete w.r.t. the denotational (domain-theoretic)
semantics, they are sound. That is, you can't use the denotational semantics
to prove that your program won't get a heap overflow; but you can use them
to prove that if your program doesn't get a resource failure like that,
then it will compute the right answer.
If you want to reason about resource limits, then you need to use
an operational semantics, not the denotational semantics.
> I think it is a requirement upon a
> Haskell implementation to preserve the independence of threads
> by "localizing" the resources to the threads, such that each thread
> can predict by itself, independently of any other thread, whether
> its resources will be sufficient.
I don't think this is desirable in the general case.
I think it would be useful to *allow* threads to reserve
resources, but often it is difficult to predict in advance
exactly how much each thread will use, and frequently it
is better to deal with resource failures when they arise.
--
Fergus Henderson <[EMAIL PROTECTED]> | "I have always known that the pursuit
WWW: <http://www.cs.mu.oz.au/~fjh> | of excellence is a lethal habit"
PGP: finger [EMAIL PROTECTED] | -- the last words of T. S. Garp.
