Re: [Caml-list] Unsoundness is essential

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

On Wed, 2007-10-03 at 19:13 -0400, Jacques Carette wrote:
> skaller wrote:
> > To be bold I propose type theorists have got it totally wrong.
> >
> > Goedel's theorem says that any type system strong enough to
> > describe integer programming is necessarily unsound.
> >   
> No, that's wrong.  Any *complete* type system that strong is unsound.  
> It says nothing about incomplete systems.

You're right, I have assumed a complete system cannot describe
the integer programming. Is that not so?

> > I want an unsound type system! 
> No you don't, you want an incomplete one.  You want one where the type 
> system will tell you when you are obviously wrong, and will ask you for 
> a proof when it's not sure.  If you insist on unsound, then when the 
> type system doesn't know, it might let things through anyways, and then 
> all bets are off.  I don't want that.

Ah, but that is what I *am* arguing for. The 'reasoning' is simply
that 'the programmer knows best' -- when the type system doesn't.
The evidence is: programming languages with dynamic or unsound
typing eg Python, C, are vastly more popular than those with 
strong typing.

Now, my (quite disputable) claim is that the reason for that 
is that the strong typing people prefer to reject correct 
programs than accept ones which cannot be proven correct, 
but this belief is *demonstrably* fallacious.

As I demonstrated with simple examples, the type system ALREADY
lets incorrectly typed programs through. This fact is hidden
by theoretical mumbo-jumbo. It's time the theorists woke up.
Leaving out (int-{0}) as a type simply because it would make
the type system unsound does not enhance the reliability of
the program: either way, without the annotation and a sound type
system or with the annotation and an unsound system, it is possible
to have a division by 0.

The difference is that the unsound system can be improved,
and the human brain can do type-checking too. So the unsound
system is better because it subsumes the sound one.
Nothing is lost in the unsound system. NEITHER system 
guarantees correctness, and the unsound system still
rejects at least the same set of incorrect programs,
but possibly more.

Ocaml type system is ALREADY unsound: any division by zero
or array bounds check exception provides that conclusively.

Type systems will NEVER be able to prove all programs are
correct. Requiring type safety, i.e. soundness, is simply
an obstacle, not an aid. Correctness and type-safety from
soundness aren't the same thing. It is better to put
more information in the type system, to be more expressive
and declarative and accept unsoundness, than to be limited
in one's declarative description of executable code, so
that in fact the typing is WRONG, in which case the soundness
of the type system is of no use in proving correctness!

I am arguing in favour of a much richer and more expressive
type system, EVEN IF it is not known how to prove type-correctness,
and indeed EVEN IF it CAN be proven that there exist cases
which are undecidable!
 
> Again, I disagree.  It's much better to do most type checks statically, 
> and then to residualize some type checks to run-time if you absolutely 
> must.

I don't see how I disagree with that. Indeed, that is very much
my point! You check what can be checked early, but unless the
compiler can PROVE that the code is incorrect, it should not
reject it. Unsoundness doesn't imply incorrectness.

Any failure caught at runtime by a 'residualised' check
proves the type system is unsound.

So actually you agree with my point. If indeed the type
system were sound there would necessarily not be any need
to generate any such run time checks.

[Note: this does not mean run time type information isn't
required, eg constructor indices, array bounds, etc:
run time type calculations subsume mere type-checks]

> > In particular, the ability to write proper type annotations
> > such as
> >
> > 	divide: int * (int - {0}) -> int
> >
> > and fail to reject programs which violate the typing is an
> > essential and useful feature. 
> I would rather say that what should be done is that run-time type checks 
> should be residualized into the program, so that no unsound program 
> would be allowed to run to completion, an assertion would be triggered 
> first.

I told you: you're agreeing with my claim. However it is slightly
confused: a program can be correct or not, it cannot be unsound.
It is the type system which can be sound or not.

So I am going to assume you mean: a program with suspicious typing
for which a type-safety proof cannot be found at compile time
should have a run time check to ensure the fault consequent
of the unsoundness is caught and diagnosed ASAP at run time.

I don't dispute the ability to generate such checks is useful,
however I raise these issues:

1. What if you cannot generate the checks?
2. Just because the checks pass doesn't mean the program is correct

> > In fact, the idea of C is the right one. 
> When I was forced to write a C program (after enjoying Ocaml so much), 
> and even with
> gcc -W -Wall -Werror -pedantic something.c
> I got a clean compile which, when run, core dumped, I was seriously 
> unhappy. 

And I got a Not_found error in my Ocaml program recently which took
three days to locate. I don't see any qualitative difference.

There is a difference of 'degree' which confusingly is a quality
issue: better diagnostics, earlier detection, etc. But the bottom
line is an uncaught exception in Ocaml and a null pointer dereference
in C both cause an abnormal termination symptomatic of an incorrect
program (not necessarily due to a typing error).

> > Stop CHEATING by refusing to allow
> > me to write types you can't check -- because this forces
> > ME as the programmer to cheat on the type annotations:
> >
> > 	divide: int * int -> int
> > 	hd : 'a list -> 'a
> >   
> Here we agree.  Both of those types are 'cheating'. 

Yes, but your solution might look like this:

	divide: int * (int \ {0}) -> int

with static check on int, and residualised check for a zero
divisor .. and for hd, similar... 

Hey, Ocaml does those checks NOW! SO what's the difference??

The difference is that the system with 

	(int \ {0})

is unsound, but more expressive. My argument is simply that
this is BETTER. Not allowing this has no real utility other
than to allow theorists to argue the type system is sound.
It has no benefits, and many downsides.

Perhaps you see a problem where some typing notation is so hard
it cannot even be checked at run time? This can surely happen.

My answer is: SO WHAT? The programmer is going to code the algorithm
ANYHOW. They will either use CHEAT types, in which case the type
safety provides no benefit OR, MUCH WORSE .. they're go off and
write the program in Python or C instead.


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