Re: and then... (a curiosity)

[stefan-lucks@see-the.signature]

On Thu, 4 Sep 2008, Dmitry A. Kazakov wrote:

> There is absolutely no reason to sacrifice purity for impurity.

Fine! ;-)

> >    If A is false, the expression is false, whatever B does. 
> >    If A raises an exception, of if A is true and B raises an exception, 
> >    the exception is propagated.
> 
>    1 /\ T = T (it works!)
> 
> As you see the theory works fine, even if you don't like it.
> 
> Anyway now I see what you want. That is (more or less formally):
> 
> Boolean'Base is Belnap logical values. All Boolean expressions are
> evaluated in Boolean'Base, as it is already done for numeric types. Nothing
> drastically new. (Compare also how Float overflow is converted to IEEE
> Infinity.) Like universal numbers, Boolean'Base may have no variables
> declared.

> > (*) Funny problem: *Which* exception should be propagated? 
> 
> This is not funny. This one kills the idea, unless you forcefully convert
> all exceptions into Constraint_Error, when a non-Boolean value is converted
> to Boolean.

If I would actually propose something like that, I would probably propose 
to raise Program_Error if the exceptions aren't all the same. 

> But the main problem is that this is not what people want. They do lazy
> evaluation in order to control side effects (and exception is considered
> rather as a side effect). 

Well, exceptions are treated like side effects, but they actually are 
something different. 

E.g., pure functions are free from "real" side effects, but they can still 
raise an exception. Even if you employ the SPARK verifier, you can be sure 
that no Constraint_Error occurs, but you still don't know about 
Storage_Error.




-- 
------ Stefan Lucks   --  Bauhaus-University Weimar  --   Germany  ------
               Stefan dot Lucks at uni minus weimar dot de
------  I  love  the  taste  of  Cryptanalysis  in  the  morning!  ------