From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: 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 C62B8BBAF for ; Wed, 17 Feb 2010 20:41:27 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AhUCAN/Ue0vRVdzfkGdsb2JhbACTNodECBUBAQEBCQkMBxMDILAEhHWIcgEBAwWEWASMBg X-IronPort-AV: E=Sophos;i="4.49,493,1262559600"; d="scan'208";a="44981777" Received: from mail-fx0-f223.google.com ([209.85.220.223]) by mail3-smtp-sop.national.inria.fr with ESMTP; 17 Feb 2010 20:41:27 +0100 Received: by fxm23 with SMTP id 23so6823911fxm.22 for ; Wed, 17 Feb 2010 11:41:27 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:mime-version:sender:reply-to:received :in-reply-to:references:from:date:x-google-sender-auth:message-id :subject:to:content-type:content-transfer-encoding; bh=v8wD2UCYm+42fm62yALVySGvZHpNmAxnujmMSd8XvgA=; b=rrux1FI+rWo3ZSNvznetV4wodDDuK3FKbFtGMc8u/JZ5dzYNTN4WpXRtuJfLljplgh qjFAIIJkN/aJU/ioQkTzV6+3mAC590ASHCs71LQz+t+WRaFurUl1TcdmuA88Uu5Es1g6 uHTWDyRn5OsZ3X/50Q1GiSvp+xlKAZO3AJYlo= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=mime-version:sender:reply-to:in-reply-to:references:from:date :x-google-sender-auth:message-id:subject:to:content-type :content-transfer-encoding; b=MOjCcWNVyq/LRC29Y6PAVUJRIYnpar+2JO4coT3/Z3JgCpbS3+xSct+lVd4t1WNQur 6NNVT9eX9t/Xmqwd6JzF1MJav6HFO9pFzhgckGl2zzWsyrfFW1UaWOvF4SvB3mylSuPq pAFHjOFHUog5+q849JT7rYsdHdkD3lJT6tOEo= MIME-Version: 1.0 Sender: cppcrazy@gmail.com Reply-To: boris@yakobowski.org Received: by 10.204.26.148 with SMTP id e20mr3686346bkc.25.1266435687162; Wed, 17 Feb 2010 11:41:27 -0800 (PST) In-Reply-To: <20100217163424.GA38458@tenebreuse> References: <20100217163424.GA38458@tenebreuse> From: Boris Yakobowski Date: Wed, 17 Feb 2010 20:41:07 +0100 X-Google-Sender-Auth: 7c078b1e9d5061a8 Message-ID: <76c7f53f1002171141y68374f94u11d0ac807ccfee89@mail.gmail.com> Subject: Re: [Caml-list] type generalization of recursive calls To: =?ISO-8859-1?Q?St=E9phane_Gimenez?= , The Caml Mailing List Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable X-Spam: no; 0.00; yakobowski:01 yakobowski:01 recursive:01 gimenez:01 gimenez:01 recursive:01 coq:01 syntactical:01 ocaml:01 annotations:01 polymorphism:01 checker:01 inference:01 undecidable:01 recursion:01 Hi Gim, On Wed, Feb 17, 2010 at 5:34 PM, St=E9phane Gimenez wrote: > Questions: > =A0- Is it theoreticaly safe to generalize recursive calls ? Yes. And this is done in explicitly-typed languages, such as in Coq. > =A0- Is there a syntactical trick to use generalized recursive calls ? Not in the current Ocaml, as type annotations cannot be used to introduce type polymorphism. However, see below. > =A0- Could such a generalization be added to the type checker ? > =A0 =A0 =A0- Performance issues ? > =A0 =A0 =A0- More obfusctated type checking errors ? Unfotunately, it is worse than that : type inference is undecidable in the presence of polymorphic recursion. See e.g. http://citeseerx.ist.psu.edu/viewdoc/summary?doi=3D10.1.1.42.3091 > In a related disscution I found, one asked about generalization > between mutualy recursive definitions (same problem). No answers, but > maybe I just lack pointers. If I'm not mistaken, you can encode all cases of polymorphic recursion using mutual monomorphic recursion. For your example, this would give let rec map f =3D function | E -> E | D (t1, t2) -> D (map f t1, map f t2) | O a -> O (f a) | I tt -> I (map2 (map f) tt) and map2 x =3D map x Here, map is always called with type ('a -> 'b) -> 'a t -> 'b t inside its own body (and is instantiated only inside map2). Thus this second problem is even harder than polymorphic recursion. Finally, starting from Ocaml 3.13, you can simply write let rec map : 'a 'b. ('a -> 'b) -> 'a t -> 'b t =3D fun f -> function | E -> E | D (t1, t2) -> D (map f t1, map f t2) | O a -> O (f a) | I tt -> I (map (map f) tt) Hope this helps, --=20 Boris