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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 2E89EBC6C for ; Fri, 5 Oct 2007 17:41:12 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAK73BUfAXQImh2dsb2JhbACOOQIBCAop X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="2193434" Received: from discorde.inria.fr ([192.93.2.38]) by mail1-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2007 17:41:12 +0200 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95FfBDH020951 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 17:41:11 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAK73BUdC+VLklmdsb2JhbACOOQIBAQcEBhERBw X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="3801583" Received: from wx-out-0506.google.com ([66.249.82.228]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 17:41:10 +0200 Received: by wx-out-0506.google.com with SMTP id h28so562494wxd for ; Fri, 05 Oct 2007 08:41:09 -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:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; bh=XjKlWcH17nMQ+jJyAYJJgDrBSs/s4gITd5LhCqKbgF0=; b=ZRRp6x5CvfJD/mL7/5t8iAdrJRg016NDNzwZt57if787+ELYdjT8TWSdrIBQDY/s0uD+GDsz16uoz1hZtKdqfqJ+TNBQdfAuk239F6ZVSGCa53fu3amdmGixM9HNP9CaKeekO2NqmyzYVZHpOcqM/BAG+BN2toQ+27r6JXEvsGY= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:sender:to:subject:cc:in-reply-to:mime-version:content-type:content-transfer-encoding:content-disposition:references:x-google-sender-auth; b=H6kD5MrISSfve281jIYBxEhQmrkMEqC5VEonuu971VchhMmt8nk2VPwZz8FY/eENqwWYMu5/un9UQgP6ML1uDRB4Bo6un/lLXnM7qc07j25eC/MUyE0uUcjHr+JlrlYNcLxGj3zMlAO+LKdDjSgTO/Hct9hiIIZQQqdV0cNf/CY= Received: by 10.78.170.6 with SMTP id s6mr8807011hue.1191598868231; Fri, 05 Oct 2007 08:41:08 -0700 (PDT) Received: by 10.78.156.10 with HTTP; Fri, 5 Oct 2007 08:41:08 -0700 (PDT) Message-ID: <4a051d930710050841t7de7dfa3qf695ee271b38bcb7@mail.gmail.com> Date: Fri, 5 Oct 2007 11:41:08 -0400 From: "Christopher L Conway" Sender: christopherleeconway@gmail.com To: "Vincent Aravantinos" Subject: Re: [Caml-list] Depend-type beginner question Cc: "Gurus Ocaml" In-Reply-To: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Content-Disposition: inline References: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> X-Google-Sender-Auth: 28e84b962625898f X-Miltered: at discorde with ID 47065B17.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 undecidable:01 ocaml:01 decidability:01 hurdles:98 wrote:01 caml-list:01 arithmetic:01 precisely:01 implemented:02 implemented:02 checking:02 dependent:04 guess:04 types:05 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 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)... Regards, Chris