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 mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 42F04BC69 for ; Fri, 5 Oct 2007 17:53:09 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAH/6BUdA6ba9i2dsb2JhbACOOQIBCAQEExEF X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="17343340" Received: from discorde.inria.fr ([192.93.2.38]) by mail4-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 17:53:09 +0200 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95Fr8YL021586 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 17:53:08 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAH/6BUdA6ba9i2dsb2JhbACOOQIBCAQEExEF X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="17343338" Received: from nf-out-0910.google.com ([64.233.182.189]) by mail4-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 17:53:07 +0200 Received: by nf-out-0910.google.com with SMTP id g13so512812nfb for ; Fri, 05 Oct 2007 08:53:07 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:from:subject:date:to:x-mailer; bh=L7EkAlvnfIXAYStgOhyjgjW1Vy1QFD2ppBc/b+LGBaU=; b=k1H/sWog7JtkBapSD2LouGCMYNEztsiF05eD2PsQaFPI+APAVC4NnB2bnMPggEARBGiEwBSDJPeI5ldATiI43aUolzLlFY/ROJsFybhvDYeDzkn+tt0XLlZdmb3f/SQ0OCl11myBdevjXGaYr1P1tL6mX3rBb7vrN9CaWsYHzcM= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:in-reply-to:references:mime-version:content-type:message-id:cc:content-transfer-encoding:from:subject:date:to:x-mailer; b=SrBa0lBZJXX3AuUfuBmy/As8Q8/gmubxmbpY+dYVelcUc9N0qUd0/1r0/IdmkkEPSGfrbIR8L9cbc/inwYDKCn7I3HMRHqgGbQa+hp5pCddxX7w/gtuCVSFkUWRyWYgDA+qnjcQLEHMCNlALsWEvHFcSzICmAosPCSkK9h2kcf8= Received: by 10.86.54.3 with SMTP id c3mr2572960fga.1191599587436; Fri, 05 Oct 2007 08:53:07 -0700 (PDT) Received: from ?192.168.0.10? ( [82.229.199.66]) by mx.google.com with ESMTPS id w7sm6100322mue.2007.10.05.08.53.05 (version=TLSv1/SSLv3 cipher=OTHER); Fri, 05 Oct 2007 08:53:06 -0700 (PDT) In-Reply-To: <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> References: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Message-Id: Cc: "Gurus Ocaml" Content-Transfer-Encoding: quoted-printable From: Vincent Aravantinos Subject: Re: [Caml-list] Depend-type beginner question Date: Fri, 5 Oct 2007 17:53:03 +0200 To: "Christopher L Conway" X-Mailer: Apple Mail (2.752.2) X-Miltered: at discorde with ID 47065DE4.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 undecidable:01 ocaml:01 decidability:01 existential:01 hurdles:98 wrote:01 compile:01 caml-list:01 arithmetic:01 precisely:01 implemented:02 implemented:02 checking:02 seems:03 Le 5 oct. 07 =E0 17:41, Christopher L Conway a =E9crit : > On 10/5/07, Vincent Aravantinos wrote: >> why actually dependant types cannot be implemented in ocaml ? Is the >> type checking undecidable ? Or is it for other reason (e.g. >> arithmetic) ? I guess it's both. But could someone develop =20 >> precisely ? > > It's not that dependent types can't be implemented in OCaml, just that > they haven't. See, e.g., http://www.cs.bu.edu/~hwxi/DML/DML.html > > I suspect the OCaml development team is not inclined to add "sexier" > types to the core language, though I can't say if there are any > specific technical hurdles preventing it (certainly, decidability is > an issue)... I can't get how the following could ever be typed at compile time: > if ... then [] else [a] Is this a 0-list or a 1-list ? do they just put an existential =20 variable -> n-list ? If this is it, it seems to me that you won't be =20 able to gain much information. ?? V.=