Re: [Caml-list] Unsoundness is essential

[skaller <skaller@users.sourceforge.net>]

On Thu, 2007-10-04 at 23:07 +0200, rossberg@ps.uni-sb.de wrote:
> skaller wrote:
> >
> >> Exceptions are /trapped/ errors.
> >
> > I chose not to accept that definition. I use instead
> > "trapped at compile time", meaning "in advance of running
> > the program".
> 
> As a definition for what?

What trapped means.

> > Otherwise you could say dynamically typed languages were
> > strongly typed and sound.
> 
> In fact, technically, they are. People have used the term "unityped" for it.

That isn't what I meant at all. Python is statically unityped, but
dynamically it has integers, reals, strings, etc. Type errors
in Python are not 'trapped' .. they're impossible.

> > C/C++ does this right: if a program is 'ill-formed' then
> > a diagnostic must be issued. Throwing an exception silently
> > is NOT allowed. [C/C++ doesn't mandate diagnostics always because
> > some are too hard to detect]
> 
> This paragraph sounds like a contradiction in itself.

Yes, but it isn't. If the specification was to throw
a catchable exception, then that would be a requirement
on implementation which would permit programmers to divide
by zero deliberately. In that case, a divide by zero error
is impossible to detect because it can't be distinguished
from the legitimate division by zero for the purpose
of raising an exception.

> More importantly, an OCaml program performing div 0 isn't "ill-formed", it
> has a perfectly well-defined, safe semantics (in precisely the same way as
> adding a string in Python). See the library docs.

I didn't claim otherwise: I claim it is a very bad idea
to permit a program to do obvious bullshit like divide by zero
(for integers I mean).

Note I'm NOT saying Ocaml *implementation* shouldn't raise an exception,
just that the language specification should not require it do so.
The difference is in one case the operation is semantically well defined
and thus definitely not detectable as an error, whereas in the other
it is not defined, and so is unequivocably an error.

Oh well this was fun but I'm off interstate without a computer for
a week.. hope my Airbus doesn't divide any empty lists by zero ..

-- 
John Skaller <skaller at users dot sf dot net>
Felix, successor to C++: http://felix.sf.net