From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by yquem.inria.fr (Postfix) with ESMTP id 633E4BC48 for ; Wed, 27 Apr 2005 22:13:25 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j3RKDOOk019384 for ; Wed, 27 Apr 2005 22:13:25 +0200 Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id WAA08993 for ; Wed, 27 Apr 2005 22:13:24 +0200 (MET DST) Received: from smtp05.web.de (smtp05.web.de [217.72.192.209]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j3RKDOG2019381 (version=TLSv1/SSLv3 cipher=EDH-RSA-DES-CBC3-SHA bits=168 verify=NO) for ; Wed, 27 Apr 2005 22:13:24 +0200 Received: from [217.235.112.5] (helo=wiko) by smtp05.web.de with smtp (WEB.DE 4.105 #275) id 1DQsuQ-0003AE-00; Wed, 27 Apr 2005 22:13:23 +0200 Message-ID: <001b01c54b65$b28bbe90$14b2a8c0@wiko> From: "Andreas Rossberg" To: , "Mike Hamburg" References: Subject: Re: [Caml-list] type-checking difficulties in recursive functions Date: Wed, 27 Apr 2005 22:13:44 +0200 MIME-Version: 1.0 Content-Type: text/plain; charset="iso-8859-1" Content-Transfer-Encoding: 7bit X-Priority: 3 X-MSMail-Priority: Normal X-Mailer: Microsoft Outlook Express 6.00.2800.1437 X-MimeOLE: Produced By Microsoft MimeOLE V6.00.2800.1441 Sender: AndreasRossberg@web.de X-Sender: AndreasRossberg@web.de X-Miltered: at nez-perce with ID 426FF264.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 426FF264.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; rossberg:01 caml-list:01 recursive:01 rec:01 foo:01 foo:01 val:01 bool:01 bool:01 recursive:01 checker:01 recursion:01 inference:01 recursion:01 undecidable:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: Mike Hamburg wrote: > > let rec foo p x = > if p then x > else > let something = foo false "Hello" > in x;; > val foo : bool -> string -> string = > > Now, foo is actually safe as a function from bool -> 'a -> 'a, but the > recursive declaration doesn't generalize and so the checker doesn't > realize this. With magic, I can get the right type relatively safely What you want is "polymorphic recursion". Unfortunately, type inference for polymorphic recursion is undecidable in general. Haskell allows polymorphic recursion if you annotate the type, so that it doesn't have to be inferred. In OCaml, this is not possible directly, but you can achieve the same effect by going through a record and using the more recent feature of polymorphic record fields, plus OCaml's let rec "language extension": type foo_rec = {foo : 'a.bool->'a->'a} let rec foo_rec = {foo = fun p x -> if p then x else let _ = foo_rec.foo false "" in x} let foo = foo_rec.foo Not particularly nice, but does what you want. Hope this helps, - Andreas