From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id F04F0BC48 for ; Wed, 27 Apr 2005 22:55:34 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j3RKtY8N028094 for ; Wed, 27 Apr 2005 22:55:34 +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 WAA09890 for ; Wed, 27 Apr 2005 22:55:34 +0200 (MET DST) Received: from mail21.sea5.speakeasy.net (mail21.sea5.speakeasy.net [69.17.117.23]) by nez-perce.inria.fr (8.13.0/8.13.0) with ESMTP id j3RKtPgP024114 (version=TLSv1/SSLv3 cipher=DHE-RSA-AES256-SHA bits=256 verify=NO) for ; Wed, 27 Apr 2005 22:55:32 +0200 Received: (qmail 32472 invoked from network); 27 Apr 2005 20:55:24 -0000 Received: from shell1.sea5.speakeasy.net ([69.17.116.2]) (envelope-sender ) by mail21.sea5.speakeasy.net (qmail-ldap-1.03) with AES256-SHA encrypted SMTP for ; 27 Apr 2005 20:55:24 -0000 Date: Wed, 27 Apr 2005 13:55:24 -0700 (PDT) From: brogoff X-X-Sender: brogoff@shell1.sea5.speakeasy.net To: caml-list@inria.fr Subject: Re: [Caml-list] type-checking difficulties in recursive functions In-Reply-To: <001b01c54b65$b28bbe90$14b2a8c0@wiko> Message-ID: References: <001b01c54b65$b28bbe90$14b2a8c0@wiko> MIME-Version: 1.0 Content-Type: TEXT/PLAIN; charset=US-ASCII X-Miltered: at concorde with ID 426FFC46.001 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at nez-perce with ID 426FFC3D.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; caml-list:01 recursive:01 rossberg: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: On Wed, 27 Apr 2005, Andreas Rossberg wrote: > 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": It's also possible (and slightly nicer IMO) to use the experimental recursive module facility to encode polymorphic recursion in OCaml. There are some restrictions, but they're not horrible. Speaking of modules, for a while, there was talk of some notion of mixin modules to address the problems (and more) being addressed by the recursive module feature. Anyone in the know care to comment on what happened with that? -- Brian