Re: [Caml-list] Unsoundness is essential

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

On Thu, 2007-10-04 at 10:56 +0200, Arnaud Spiwack wrote:
> Hi everybody,

> Still there is something peculiar in the interpretation of Gödel 
> theorem, since if we are in a classical logical system (where ~~A (not 
> not A)  and A are equivalent). If neither A nor ~A are provable, then 
> both can be "the real one". By that I mean that both can be chosen as 
> true, without impacting the consistency of the system (quick proof 
> sketch : A -> ~A is equivalent to A -> (A -> False) which is equivalent 
> to A&A -> False wich is equivalent to ~A).
> 
> A conclusion I can draw from that is that we don't care about what is 
> true, we care about what is provable, since it is at least welle 
> defined,

This is my point. Theorists have this all wrong.
I'm a programmer. I do NOT really care if my program is provably
correct. Sure, it would be nice to have such a proof, but the
lack of one will not stop me writing the program!

What I care about is that the program works.

Now, suppose I code some types in my program, and the
type system cannot prove I have respected them. Incompleteness
ensures this can happen (given a sufficiently powerful
type system). Pragmatics indicates this is also possible:
the proof may indeed be constructible but take too long
to construct to be practical.

Should it accept or reject the program? My claim is that
it should accept the program. It should only reject programs
which can be proven incorrect.

Now, I want you to hold on before disputing that claim,
because there is more to the reasoning to come.

The purpose of typing is to assist in showing a program 
is incorrect. We know for sure that in principle and practice
there will be well typed incorrect programs, so there
is no issue of proving all programs correct.

The question is, should we strengthen the type systems
we use to be more descriptive? There is a problem doing this.
If we make the type system descriptive enough, there is a 
possibility we will be able to reject more programs --
this is good! But it is also likely that we will lose
the ability to prove the typing is correct. What should
we do?

If we reject the program, the programmer will be annoyed,
if we accept it, the type system is unsound, because
in accepting it, we risk accepting programs which are
not well typed, and therefore not correct.

Now, please observe that with a stronger type system,
we are going to reject more programs. That is the point.
But we are ALSO going to be unable to decide the well typedness
of many programs, for either incompleteness or pragmatic
reasons.

It simply isn't feasible to reject these programs simply
because a proof of well-typedness cannot be constructed:
and there is no possibility of disputing this claim
because it is what programming languages like Ocaml do
right now: they generate run time checks precisely because
they cannot ensure correctness.

It's already a known fact that today, we cannot ensure
certain things like array bounds and zero division
statically.

So the question is, whether array length and non-zero
integers should be expressible in the type systems 
today.

And my answer is YES PLEASE. A type system with that
expression MUST BE UNSOUND.

I hope this argument is not too hard to follow:
if you make the type system expressive enough, right now,
then it MUST BE UNSOUND because we cannot have the type
system rejecting the many correct programs I can and do
write where I (think I) know I'm never going to divide
by zero, simply because the type system cannot prove
my belief.

There is no issue that the powerful type system must
be unsound. That is not the question or the claim.

The question is: should compiler writers introduce
powerful enough type systems that can express things
like non-zero integers or array index correctness,
KNOWING FOR SURE THAT TO DO SO MANDATES UNSOUNDNESS.

There's no question such powerful type systems have
to be unsound, at least today. That isn't in dispute!

The question is whether we should introduce such rich
and expressible notations anyhow!

My claim is YES WE SHOULD. Because Arnaud is quite wrong
in his belief that 'what we should care about is provability'.
That is what theoreticians care about, but it is NOT the domain
in which programmers operate (unless they're type systems programmers
of course! :)

[PS: of course I do *care* about provability, but I'm not
willing to give up programming just because I can't prove
everything I code is correct]

So finally I will give an example: I cannot write this:

	hd : 'a non-empty-list -> 'a
	divide: int * non-zero-int -> int

in Ocaml at the moment. Should I be able to??

If you say YES, you will note the Ocaml type system would 
become unsound. Ocaml simply cannot prove in all cases that an 
integer value is non-zero, nor that a list is non-empty.

We do not reject programs that apply 'hd' just because of this.
Heck: hd and divide ARE PART OF THE CORE LIBRARY!!!!

My point is: NOTHING IS LOST BY MAKING THE TYPE SYSTEM UNSOUND
WITH THIS EXTENSION. Indeed in SOME cases Ocaml may indeed
be able to prove wrong typing, so we GAIN something from 
the point of view of machine verification. And the human
programmer gains something too, because they too may find
errors, even ones the type system cannot, and it could easily
make the program semantics easier to understand, if the
interface type annotations were richer.

So my belief is that theoreticians are doing the programming
industry a DISSERVICE by insisting on sound typing, because
in so doing they're greatly limiting the expressiveness of 
the type system.

There is no benefit in it. That is the point. A proof of
well-typedness is NOT a proof of correctness in the first
place. I do not care that the type system cannot prove
well typedness because that is not its job: its job is
to prove a program INCORRECT by proving wrong typing.

Making the type system unsound by extending the expressiveness
can be done without failing to reject programs which are
currently rejected. Take Ocaml and add non-zero integers,
and allow it to accept programs where the non-zeroness
cannot be proven, and we are no worse off than now, where
the same fact applies: Ocaml ALREADY allows such programs.

Much as we'd like to be able to guarantee that a program using
non-zero integer type is well typed, it is better to let such
a program pass, than to compromise the expressiveness of
the type system JUST BECAUSE THEORETICIANS ARE SO CONFUSED
ABOUT WHAT THE PURPOSE OF THE TYPE SYSTEM IS THAT THEY REFUSE
TO ALLOW AN UNSOUND ONE (of course I'm definitely not meaning
to be offensive here!)

If you think a type system has to be sound, you do not understand
that the purpose is to catch errors early, and if not diagnose them
late, and we wish to catch as many as possible. We are therefore
COMPELLED to introduce a richer type system, and there is no doubt
such a system, at least today if not always, cannot be sound.

BTW: I am not asking for 'non-zero-int' and 'non-empty-list' as
actual features for Ocaml. There is still a real issue how to make
the extensions to the type system in a general enough way.
For example:

	int \ {0}

looks better because subtraction is a fairly general operator,
but there may be other more useful annotations.

There certainly exist languages where the 'checking' system 
is 'unsound'.

For example Eiffel and Felix both allow pre and post conditions on
functions, and both generate run time checks, which are witness
to unsoundness.

It is merely pride of theoreticians that they claim a precondition
is not type information. There is NO DOUBT in my mind a precondition
is precisely a restriction on the set of input values to a function,
and is definitely type information.

Ocaml does not let you notate this**, although you can write an assert,
but in Felix it is plain it is intended as type information:

	fun divide(x: int where x!=0): ...

even though this is not encoded in the type signature because I do not
know what to do with it. In Felix the typing is unsound, because
it generates the non-zero test at run time.

** of course Ocaml DOES let you notate this now we have private
types we can enforce the constraint in the constructor of a record,
however this semi-abstract type is nominally typed, and not
quite the same as a structural annotation like int \ {0}
which is anonymously typed. However this enforcement is clearly
an unsoundness of typing because the constraint isn't enforced
at compile time. So this is a perfect example of a GOOD
extension of the kind I desire which already introduces an
unsoundness. The key point of the idea is in fact to clearly
and pointedly restrict the unsoundness to the constructor.
Using this, plus smartness of the type system, we may be able to:

	a) reject some programs which are clearly incorrect
	b) optimise away the check in other programs which
		are clearly correct
	c) accept a program where the type system cannot decide
		and generate runtime check as witness to the
		unsoundness

This is GOOD. There should be more of it! The lack of soundness
is not a problem -- it's ESSENTIAL to rejecting even more incorrect
programs because there's no way to eliminate the unsoundness
without eliminating the very expressiveness which allows more
programs to be type checked and thus more to be rejected.
What's more, it leads to better performance too.

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