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 A21BBBC69 for ; Sat, 6 Oct 2007 01:29:50 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJBlBkfAXQImh2dsb2JhbACOOAEBAQgKKQ X-IronPort-AV: E=Sophos;i="4.21,237,1188770400"; d="scan'208";a="3811949" Received: from discorde.inria.fr ([192.93.2.38]) by mail3-smtp-sop.national.inria.fr with ESMTP; 06 Oct 2007 01:29:50 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95NTnNX015735 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Sat, 6 Oct 2007 01:29:50 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJBlBkdA6ba8mGdsb2JhbACOOAEBAQEHBAQTGA X-IronPort-AV: E=Sophos;i="4.21,237,1188770400"; d="scan'208";a="2436850" Received: from nf-out-0910.google.com ([64.233.182.188]) by mail2-smtp-roc.national.inria.fr with ESMTP; 06 Oct 2007 01:29:49 +0200 Received: by nf-out-0910.google.com with SMTP id g13so601729nfb for ; Fri, 05 Oct 2007 16:29:49 -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:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; bh=oyhxoI8Z2vRbNXJem8JRTPU7w5+mw+ENKzIOTM7p/1w=; b=ZvWHA26Jchx5WMpu2/irHB890qwCydvZqAh6gF7brPSS3VWvrC7OPXyo8oXLcckkKL0RufPjRd7kJsmdRDiz+zYbRwiHGeNz7WLJe/16tbL6JdKe4T2uLb4rvVNhlDCgQTLAOs9t+X7ovsg+707R3lQ+aYoQhOhEKgGg1ijhF3w= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=CmhqlY0s7RVEOmdlln+XAOhkQ4b24q3IEKJt3JgfFwuzXKaRoWiDhe82SM6H1chIcVZJrHRrs62pGWjh5I6Lzxtm+IigQiFqI6IDOSrlNjL/zE8Z+q9IrbH7xDbqUeIgEURnvnmCXLXwIrBircIVub18TXh1Bca1k5vI3hNKwxM= Received: by 10.86.93.17 with SMTP id q17mr2855874fgb.1191626988852; Fri, 05 Oct 2007 16:29:48 -0700 (PDT) Received: from ?192.168.0.5? ( [87.88.165.197]) by mx.google.com with ESMTPS id u9sm7003005muf.2007.10.05.16.29.44 (version=SSLv3 cipher=RC4-MD5); Fri, 05 Oct 2007 16:29:45 -0700 (PDT) Message-ID: <4706C8E5.4040908@lix.polytechnique.fr> Date: Sat, 06 Oct 2007 01:29:41 +0200 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.6 (Windows/20070728) MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Depend-type beginner question References: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> <470663E2.2060702@univ-savoie.fr> <5334A8EA-1D74-4BFA-8F7D-5154D441C561@gmail.com> In-Reply-To: <5334A8EA-1D74-4BFA-8F7D-5154D441C561@gmail.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Sender: Arnaud Spiwack X-Miltered: at discorde with ID 4706C8ED.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; lix:01 compile-time:01 decidable:01 ocaml:01 haskell:01 decidable:01 inference:01 coq:01 coq:01 syntax:01 nat:01 forall:01 forall:01 christophe:01 well-formed:01 > > Of course. So languages that claim to have dependant types all delay > the type checking to compile-time or formal proof. I am reassured, I > thought I was missing some big thing... I'm not sure I'm quite getting what you mean here. In any case, dependent types mainly means that there is a bit of computation inside types. This raises quite a lot of issues. It is way preferable, for instance, that type-checking is decidable, which means that one can't put arbitrary computation inside types, moreover, it would be preferable that a type does not read or write into files, that would be rather annoying. In order to get things done, there are a few approachs, languages like OCaml, Haskell, and such, try to build up from decidable inference to richer type systems and see what they can get done, this have the advantages of manipulating fully usable languages; languages like Coq, Agda, Epigram, start with dependent types as highly expressive as possible, and try to retrieve features bit by bit (and thus are not fully usable languages). (I haven't quoted DML and PML because I still haven't quite looked into them, thus I can't really place them :p ). However, to get back to the list example. Let us suppose, in Coq syntax, that we defined lists the following way : Inductive list (A:Type) : nat -> Type := | Nil : forall A, list A 0 | Cons : forall A n, A -> list A n -> list A (S n) These are lists that carry their length. The program : if b then [] else [a] can only be typed as a *dependent* elimination of b, as Christophe said the type is "if b then list A 0 else list A 1". The whole point of dependent types is that this is a perfectly well-formed type. And it can be checked before compiling "if b then [] else [a]" that it actually have type "if b then list A 0 else list A 1". The schyzophrenia of dependent types, is that types depend on previously compiled (and types) expressions, it still is static typing, just weirder (and much more fun if you want my opinion ;) ). Arnaud Spiwack