From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 96349BC69 for ; Thu, 4 Oct 2007 04:19:57 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADbqA0fAXQInemdsb2JhbACOOAEBCQo X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2350906" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 04:19:57 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l942Jucg001992 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 04:19:57 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAADbqA0fYi40EnWdsb2JhbACOOAEBAgsN X-IronPort-AV: E=Sophos;i="4.21,226,1188770400"; d="scan'208";a="2350905" Received: from mail-out4.nyct.net (HELO bsd4.nyct.net) ([216.139.141.4]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 04:19:56 +0200 Received: from [192.168.42.2] (adsl-216-139-154-52.nyct.net [216.139.154.52]) by bsd4.nyct.net (8.13.4/8.13.4) with ESMTP id l942Jri4050608; Wed, 3 Oct 2007 22:19:55 -0400 (EDT) (envelope-from bhurt@spnz.org) Date: Wed, 3 Oct 2007 22:35:57 -0400 (EDT) From: Brian Hurt X-X-Sender: bhurt@localhost To: skaller Cc: "Joshua D. Guttman" , caml-list@inria.fr Subject: Re: [Caml-list] Unsoundness is essential In-Reply-To: <1191462724.7542.76.camel@rosella.wigram> Message-ID: References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> <1191462724.7542.76.camel@rosella.wigram> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII; format=flowed X-Miltered: at concorde with ID 47044DCC.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; recursion:01 ocaml's:01 unification:01 haskell's:01 haskell:01 ocaml:01 haskell:01 ocaml:01 2007,:98 sourceforge:01 wrote:01 wrote:01 encode:01 integer:01 integer:01 On Thu, 4 Oct 2007, skaller wrote: > On Wed, 2007-10-03 at 19:28 -0400, Joshua D. Guttman wrote: >> skaller 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