Re: [Caml-list] Unsoundness is essential

[Brian Hurt <bhurt@spnz.org>]

On Thu, 4 Oct 2007, skaller wrote:

> On Wed, 2007-10-03 at 19:28 -0400, Joshua D. Guttman wrote:
>> skaller <skaller@users.sourceforge.net> writes:
>>
>>>   Goedel's theorem says that any type system strong enough
>>>   to describe integer programming is necessarily unsound.
>>
>> Are you sure that's what it *says*?  I thought I remembered
>> it stated differently.
>
> I paraphrased it, deliberately, in effect claiming an analogous
> situation holds with type systems.
>

I'm not sure that's correct- I thought it was that any type system 
sufficiently expressive enough (to encode integer programming) could not 
be gaurenteed to be able to be determined in the general case- that the 
type checking algorithm could not be gaurenteed to halt, in other words, 
and the computing equivelent of Godel's theorem is the halting problem.

The dividing line, as I understand it, is non-primitive recursion.  So 
Ocaml's type system, which is not Turing complete, is gaurenteed to 
terminate eventually (it may have regretable big-O behavior, including an 
nasty non-polynomial cost algorithm for unification, but it will complete 
if you let it run long enough, which may be decades...).  Haskell's type 
system, by comparison, is Turing complete, so it's not gaurenteed to ever 
halt/terminate in the general case.  One advantage Haskell has over Ocaml 
is that Haskell has a Turing complete type system- on the other hand, one 
advantage Ocaml has over Haskell is that Ocaml doesn't have a Turing 
complete type system... :-)

I am not an expert, tho.

Brian