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=1.0 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 078E4BC69 for ; Thu, 4 Oct 2007 17:31:30 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAGSjBEfAXQInemdsb2JhbACOOAEBCQo X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="3756369" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 04 Oct 2007 17:31:29 +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 l94FVTkM002207 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Thu, 4 Oct 2007 17:31:29 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAE6kBEdA6aLokGdsb2JhbACOOAEBAgcEBCIH X-IronPort-AV: E=Sophos;i="4.21,230,1188770400"; d="scan'208";a="2381868" Received: from nz-out-0506.google.com ([64.233.162.232]) by mail2-smtp-roc.national.inria.fr with ESMTP; 04 Oct 2007 17:31:28 +0200 Received: by nz-out-0506.google.com with SMTP id z3so183231nzf for ; Thu, 04 Oct 2007 08:31:28 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; bh=itM5VWoip11O19YrPGiDhhF1jpTvsrBxp2VohBfnYkI=; b=ubmDGDXKlagPJTf+vuwTsImqVW8f84DDpGGKQnA4m2hF1VdtZjk3FlSilhyJ2HF1g+2Hi25sn85YN3AORZ1V2uteQouJ33oUVDqVgeL5yCUGMrmLf0SAuVi++rtnvCT0AAMYGAhEhP6bQQ28sQde2NdSi4WPCjVkJGg+BnVLWK4= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references; b=nNKSBIXpVcfd0K5Jg+0yQg7pUd4bA9Z6GFREg6ek7Ty+mV+9AYNJsYQjcWBWPn2V5YSlYoR3Lgrm0CBSXTsuqIQ230KaMgHEGh1duKccCANEo3q8WRUyRXGo9NtHu3FtmQD2K3OFbZJokHyujsVDPtBn5ikWHnd/ID9h1RxiXC0= Received: by 10.65.121.9 with SMTP id y9mr13101268qbm.1191511874822; Thu, 04 Oct 2007 08:31:14 -0700 (PDT) Received: by 10.65.38.11 with HTTP; Thu, 4 Oct 2007 08:31:14 -0700 (PDT) Message-ID: <4a708d20710040831i292ac809kee8e0d091409c81d@mail.gmail.com> Date: Thu, 4 Oct 2007 17:31:14 +0200 From: "Lukasz Stafiniak" To: skaller Subject: Re: [Caml-list] Unsoundness is essential Cc: caml-list@inria.fr In-Reply-To: <1191451810.7218.86.camel@rosella.wigram> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <20071003083529.40DA2A99F@Adric.metnet.fnmoc.navy.mil> <4703FDEF.7030900@univ-savoie.fr> <1191451810.7218.86.camel@rosella.wigram> X-Miltered: at concorde with ID 47050751.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lukasz:01 inference:01 type-safe:01 sourceforge:01 wrote:01 typing:01 caml-list:01 python:03 dynamic:03 dependent:04 theorists:04 unsound:07 useless:07 bold:91 correct:08 A "sound program refuter" will not reject correct programs. On 10/4/07, skaller wrote: > > To be bold I propose type theorists have got it totally wrong. > > 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.