Re: [Caml-list] Unsoundness is essential

[Jacques Carette <carette@mcmaster.ca>]

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.

My position is that looking for decision procedures everywhere is what 
is blocking real progress.  People doing dependent types have gotten 
over most of that.

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

> 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.
>   
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. This is roughly what my Master's student Gordon Uszkay did for a 
"scientific computation" language, using CHRs.  Unfortunately, his work 
was already way too ambitious as it was, so all he succeeded in doing is 
an implementation [that works], but no formal proofs.

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


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

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

Jacques