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 28771BC69 for ; Fri, 5 Oct 2007 18:34:27 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJQEBkfAXQInh2dsb2JhbACOOQIBCAop X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="3803445" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 18:34:26 +0200 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95GYQeY004059 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 18:34:26 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAMwEBkdA6ba5kGdsb2JhbACOOQIBAQcEBBMRBw X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="2195796" Received: from nf-out-0910.google.com ([64.233.182.185]) by mail1-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2007 18:34:26 +0200 Received: by nf-out-0910.google.com with SMTP id g13so522422nfb for ; Fri, 05 Oct 2007 09:34:25 -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=yx4j+cmOGGovjiOG3kujrs2Vs7odJeIxV30cNHLod9w=; b=B+EhshN3yNkF33KnFXfmX+qNZVqKK/5fOtw3OZ3tyOU3nB3OUvq3zn62K0dNmHB6MKOtBOpYDwuWZRinCOmKyURLxX2gm0xELxYmbULkMtdGtb7+KUvMLJFDDWR6Tz1GW/TJCgyVG/QOzyMjeUBBjHXzCNsMX9ZXQwj7096IwcU= 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=c2omHtNtX1xV/R5QLJS4dvLmdu+s65RWarsnBy22Re8jYpsxjdo0sljljBgwnGg1keJU/B5AVfwVtykcH5jZr1V3l8rrrcK7C1zlPGtpC+8hKBHqwfEBzJlBIRhjP3YLM/iIGx6f+dqaRElrxdRD5Smd+1Nk4Eij2CCbu7IS2Bc= Received: by 10.86.84.5 with SMTP id h5mr2614648fgb.1191602065467; Fri, 05 Oct 2007 09:34:25 -0700 (PDT) Received: from ?192.168.0.10? ( [82.229.199.66]) by mx.google.com with ESMTPS id u9sm1816933muf.2007.10.05.09.34.23 (version=TLSv1/SSLv3 cipher=OTHER); Fri, 05 Oct 2007 09:34:24 -0700 (PDT) In-Reply-To: <470663E2.2060702@univ-savoie.fr> References: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> <470663E2.2060702@univ-savoie.fr> Mime-Version: 1.0 (Apple Message framework v752.2) Content-Type: text/plain; charset=ISO-8859-1; delsp=yes; format=flowed Message-Id: <5334A8EA-1D74-4BFA-8F7D-5154D441C561@gmail.com> Cc: caml-list@inria.fr Content-Transfer-Encoding: quoted-printable From: Vincent Aravantinos Subject: Re: [Caml-list] Depend-type beginner question Date: Fri, 5 Oct 2007 18:34:20 +0200 To: Christophe Raffalli X-Mailer: Apple Mail (2.752.2) X-Miltered: at concorde with ID 47066792.001 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; christophe:01 raffalli:01 undecidable:01 compile-time:01 equality:01 compile:01 caml-list:01 proofs:01 checking:02 languages:03 typed:04 complex:05 types:05 types:05 problem:05 Le 5 oct. 07 =E0 18:18, Christophe Raffalli a =E9crit : > Vincent Aravantinos a =E9crit : >> I can't get how the following could ever be typed at compile time: >> >>> if ... then [] else [a] >> > > if b then [] else [a] has type list(if b then 0 else 1) > where is the problem ? > > if b then 0 else 1 may or may not be simplified if you know b. > > The problem is that equality over such complex types in undecidable =20= > and you have > to provide proofs ... Of course. So languages that claim to have dependant types all delay =20 the type checking to compile-time or formal proof. I am reassured, I =20 thought I was missing some big thing... Thanks a lot to all, Vincent=