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 56504BC69 for ; Fri, 5 Oct 2007 17:32:47 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAJf2BUfAXQInh2dsb2JhbACOOQIBCAop X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="3801274" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 05 Oct 2007 17:32:46 +0200 Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id l95FWk1M000490 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 5 Oct 2007 17:32:46 +0200 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAM71BUdA6ba4mGdsb2JhbACOOQIBAQcCBhMY X-IronPort-AV: E=Sophos;i="4.21,236,1188770400"; d="scan'208";a="2426437" Received: from nf-out-0910.google.com ([64.233.182.184]) by mail2-smtp-roc.national.inria.fr with ESMTP; 05 Oct 2007 17:32:46 +0200 Received: by nf-out-0910.google.com with SMTP id g13so508175nfb for ; Fri, 05 Oct 2007 08:32:45 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:mime-version:content-transfer-encoding:message-id:content-type:to:from:subject:date:x-mailer; bh=7cg3UO2maS0qRfuTbOB7wOtqDWq30anTHLf7W45/zGM=; b=q8JLswjCST/3Kt4QL08VsHBCGUQ2Gk77FwjltKx3E9wpiArlRzpNPX+SmFO3wePsef1VChpx053Dee/KEQ0NWG/vRcR+hkwY4i/2Zzmz/c+q2K6yIm5OKguXl/atHqVAh8lLBaOZBS7Wv/U0D1+builo2bDLSFouPAWs+dmI/Ac= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:mime-version:content-transfer-encoding:message-id:content-type:to:from:subject:date:x-mailer; b=UGFLM7eW6eM+yHa1VrRNfATd14NwsmPbCx4cKVizRsv28YQpRmwM7qEdknSreJL9RG9n6U98Dn/UsNpRtWZQuGmKRQM3pwaQLhooDlkqzVJUz/R42Au/u+S5kGRmwqwZHYWWb8c/N0SQqwcj8Ur589b4O5ylQe0WIfgcixFzsDU= Received: by 10.86.80.5 with SMTP id d5mr2558642fgb.1191598364786; Fri, 05 Oct 2007 08:32:44 -0700 (PDT) Received: from ?192.168.0.10? ( [82.229.199.66]) by mx.google.com with ESMTPS id w5sm6061876mue.2007.10.05.08.32.42 (version=TLSv1/SSLv3 cipher=OTHER); Fri, 05 Oct 2007 08:32:43 -0700 (PDT) Mime-Version: 1.0 (Apple Message framework v752.2) Content-Transfer-Encoding: 7bit Message-Id: <2EF33DCA-1E28-4F10-AEAB-F3258E976CA7@gmail.com> Content-Type: text/plain; charset=US-ASCII; delsp=yes; format=flowed To: Gurus Ocaml From: Vincent Aravantinos Subject: Depend-type beginner question Date: Fri, 5 Oct 2007 17:32:40 +0200 X-Mailer: Apple Mail (2.752.2) X-Miltered: at concorde with ID 4706591E.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; ocaml:01 undecidable:01 computation:01 arithmetic:01 precisely:01 implemented:02 checking:02 guess:04 types:05 vincent:07 vincent:07 dependant:07 actually:10 beginner:12 question:13 Hi, 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 ? Would something like http://okmij.org/ftp/Computation/lightweight- dependent-typing.html be implementable ? Thanx, Vincent