Unsoundness is essential

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

On Wed, 2007-10-03 at 22:39 +0200, Christophe Raffalli wrote:

> So the story is by saying (wrongly) that it is too heavy to anottate
> arrow types with exceptions,
> making the arrow type a ternary type construct, ML is missing a lot ...

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.

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

I want an unsound type system! It much better than the useless
but 'sound' type system of Python, in which the type inference
engine decides all values have type Object and proves
in vacuuo that all programs are type-safe, only to do the 
dependent type checks at run time anyhow -- a cheat known
as dynamic typing.

It is better to admit from the start that type systems
can and MUST be unsound, and allow programmers to write
known correct programs with expressive typing which no type 
system could type check, than to turn programmers off by 
rejecting their valid code.

The cost is some invalid code will be accepted, but there
is no help for it: the type system has to be unsound
or it is of no practical use at all (Ok, I exaggerate,
predicate calculus is complete and useful .. algebraic
typing is the equivalent).

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. Later, some programs may
be properly rejected early instead of late when some
smart type theorist extends the capabilities of the compiler,
or the programmer learns how to re-express the typing so
the existing algorithms catch more faults.

Languages like Ocaml make significant advances in type checking
capability, but users and theorists incorrectly laugh at the weak
and unsound type system of C. In fact, the idea of C is the right
one. We know the type system is unsound. It is essential. It is the
very reason C lives on. Newer compilers have better error detection,
in the meantime C doesn't stop you writing your code. C does this
right: you can use a cast to override the type checks OR you can
simply exploit the unsoundness directly. The latter is preferable
because later versions of the compiler may be smart enough to
catch real errors which the casts would always defeat.

It's time to turn type theory on its head. Forget about whether
the typing is sound, give me EXPRESSION first and worry about
checking second. Accept Goedel: the unsoundness is *essential*
and thus must not be an excuse for failure to express. Let me
write:

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

and I may catch a bug using the human brain, or later
the compiler may be improved and catch more bugs automatically.
The fact it will never catch all these bugs is irrelevant 
because unsoundness is an essential requirement of 
expressive type systems. 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



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