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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by yquem.inria.fr (Postfix) with ESMTP id 2D370BC69 for ; Fri, 5 Oct 2007 18:52:02 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAMsIBkfAXQInh2dsb2JhbACOOQIBCAop X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="2429088" Received: from concorde.inria.fr ([192.93.2.39]) by mail2-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2007 18:52:02 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95Gq1NF005459 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 18:52:01 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAANoHBkdA6aaxkGdsb2JhbACOOQIBAQcEBhERBQ X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="3804063" Received: from py-out-1112.google.com ([64.233.166.177]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 18:52:00 +0200 Received: by py-out-1112.google.com with SMTP id u52so1069201pyb for ; Fri, 05 Oct 2007 09:51:59 -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=QS1regLheN46DGys+0iWd5iwnaShYfv7Pdx6oQgkrXA=; b=INturqNB40/L1d5kmb6BxMS3GV1aRirX0eeM7ewhm+cZ4mnGbAL+t1StcHkzRMlT1zrCuDqWDpzDdRiP5cN41r9gPlTCTBPXghocpLkJBUEPX06+HqsAEQQmJz3xji444xRIEMj+CfzJyPpdW1g6wNBc07BkaU88DLdhuIIPj3E= 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=d/JwVonB/qI54BdoFoDCuDtrzLIGk9Vb/FqbPl6Eh8/FmfcmsVdQV+Ximjid/E239c7HOqZkmTx6FciQIMoZUJF4rjS2wmiltJcgka+9B1+BfoC5zcR59K49F3ROZKEFr/f+7mqBsQslMSJ0UF4D1FT7rTC17ICzcW7/n+aXbAM= Received: by 10.65.150.18 with SMTP id c18mr16813345qbo.1191603118850; Fri, 05 Oct 2007 09:51:58 -0700 (PDT) Received: by 10.65.38.11 with HTTP; Fri, 5 Oct 2007 09:51:58 -0700 (PDT) Message-ID: <4a708d20710050951h55bfca3cs4935fbab48ab146a@mail.gmail.com> Date: Fri, 5 Oct 2007 18:51:58 +0200 From: "Lukasz Stafiniak" To: "Vincent Aravantinos" Subject: Re: [Caml-list] Depend-type beginner question Cc: "Christopher L Conway" , "Gurus Ocaml" In-Reply-To: MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable Content-Disposition: inline References: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> X-Miltered: at concorde with ID 47066BB1.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lukasz:01 ocaml:01 existential:01 iirc:01 integers:01 existential:01 wrote:01 compile:01 compile:01 caml-list:01 dependency:01 linear:02 implemented:02 seems:03 typed:04 On 10/5/07, Vincent Aravantinos wrote: > > Le 5 oct. 07 =E0 17:41, Christopher L Conway a =E9crit : > > > > 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 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 > variable -> n-list ? If this is it, it seems to me that you won't be > able to gain much information. > DML (or its successor ATS) is not really a dependently typed language IIRC. It is a polymorphically typed language which can express _some_ dependency of types on values using e.g. singleton types. The upside is that it can limit what can be expressed to a logic manageable at compile time. The downside is that you are limited to, e.g., linear inequalities over integers, and this forces you to lose information e.g. by using existential quantification.