Re: [Caml-list] Unsoundness is essential

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

On Thu, 2007-10-04 at 19:56 +0200, rossberg@ps.uni-sb.de wrote:
> skaller wrote:
> >
> > All advanced programming languages have unsound type systems
> > of necessity. Some falsely claim soundness by denying the
> > expression of certain type information (eg array bounds
> > or the type of integers excluding zero).
> 
> No. Soundness is the absence of /untrapped/ errors. 

Fair ..

> 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".

Otherwise you could say dynamically typed languages were
strongly typed and sound.

I'm not saying that it is a bad thing to emit code to
generate diagnostics at run time, if you can't prove
safety at compile time .. I AM saying that doing that
means the type system is unsound, because by type system
I mean "static type checking".

The point is that static checks are hopefully rigorous:
what ever properties they ensure they ensure them 
for certain, once and for all time.

Whereas dynamic checks prove only, in some cases,
that there is a bug and thus you have to actually
test the program with good coverage, and even then
you learn little UNLESS there is a bug :)

Also note, specified exceptions are not suitable traps:
this is a conformance issue and not really related,
but it is worth noting that if a catchable exception
is specified, the condition that caused it to be raised
isn't necessarily an error:

	try:
		x = "Bad" +42
	except:
		print "Python WILL print this"

This code is perfectly well defined and contains no
errors, not even a type error. Adding a string to an integer
raises TypeError in Python, and this is mandatory, so this
behaviour is well defined and can be used as a programming
technique (and it is!), there is no 'trapped' error here.

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]



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