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=0.9 required=5.0 tests=AWL,SPF_NEUTRAL autolearn=disabled version=3.1.3 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id 58CC2BC69 for ; Fri, 23 Nov 2007 14:38:08 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAAExmRkfRVYTzkmdsb2JhbACPNAEBAQEHBAQTFg X-IronPort-AV: E=Sophos;i="4.21,456,1188770400"; d="scan'208";a="19608123" Received: from an-out-0708.google.com ([209.85.132.243]) by mail4-smtp-sop.national.inria.fr with ESMTP; 23 Nov 2007 14:38:07 +0100 Received: by an-out-0708.google.com with SMTP id b15so667731ana for ; Fri, 23 Nov 2007 05:38:06 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=beta; h=domainkey-signature:received:received:message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; bh=DKuTA9kHO7jbUekxrHJ7gTgZOaFvspxbwrLxXslAbvI=; b=r8Pjv+hY3KHjYVpnIsNZjYtn3ofu3bpPLijfWVUrb1RL6k+njkdlDmxNXth/2phjb7B3x+FEopxABIs1153VY6BU81PJD5kUlZxeKQMEbxdNjbWPUtRaLQ/hTfId7cxG0dldfOaJseRJCfMEnkARiKv6nDVDs3opUUUEXnTcQGA= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=beta; h=received:message-id:date:from:user-agent:mime-version:to:cc:subject:references:in-reply-to:content-type:content-transfer-encoding:sender; b=soxoP7fjT+UnMuqCBiViwLpO13rj46Cr3QvkRhM5gMtU/+ewPXp+y3yM/J3a1kP7ywS9TYY+TE8Ko1x7qkxizaaN007Ass7ehD3gGIA7HccuGOZJexPE2sv+T7xy2tbYfBVwYtXE0BaTnPUZPX58u8FDVqcYGHlEK9JyrVEbIPk= Received: by 10.101.71.16 with SMTP id y16mr14019826ank.1195825086849; Fri, 23 Nov 2007 05:38:06 -0800 (PST) Received: from ?192.168.0.7? ( [87.88.165.197]) by mx.google.com with ESMTPS id k5sm1962294nfd.2007.11.23.05.38.04 (version=SSLv3 cipher=RC4-MD5); Fri, 23 Nov 2007 05:38:05 -0800 (PST) Message-ID: <4746D7BA.6060508@lix.polytechnique.fr> Date: Fri, 23 Nov 2007 14:38:02 +0100 From: Arnaud Spiwack User-Agent: Thunderbird 2.0.0.9 (Windows/20071031) MIME-Version: 1.0 To: Alain Frisch Cc: Jonathan T Bryant , caml-list@yquem.inria.fr Subject: Re: [Caml-list] Type issue References: <2921298.1195790493072.JavaMail.jtbryant@valdosta.edu> <47469A02.6010503@frisch.fr> In-Reply-To: <47469A02.6010503@frisch.fr> Content-Type: text/plain; charset=UTF-8; format=flowed Content-Transfer-Encoding: 8bit Sender: Arnaud Spiwack X-Spam: no; 0.00; lix:01 frisch:01 bool:01 bool:01 val:01 recursion:01 recursive:01 occurences:01 recursive:01 val:01 semantics:01 hen:98 polymorphic:01 wrote:01 arnaud:01 Alain Frisch a écrit : > Jonathan T Bryant wrote: >> List, >> >> I don't understand the following typing: >> >> # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;; >> type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a >> >> # let rec f t = match t with >> Cond (c,t,e) -> if f c then f t else f e >> | Value x -> x >> ;; >> val f : bool t -> bool = > > The type system does not infer polymorphic recursion: the type of a > recursive function cannot be more general than any of its occurences > within its body. > > You can get around this limitation in various ways. E.g., with > recursive modules: My personal favorite, without modules : # type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a;; let f_gen branch next t = match t with Cond (c,t,e) -> if branch c then next t else next e | Value x -> x ;; let rec f_deep t = f_gen f_deep f_deep t;; let rec f t = f_gen f_deep f t;; type 'a t = Cond of bool t * 'a t * 'a t | Value of 'a val f_gen : (bool t -> bool) -> ('a t -> 'a) -> 'a t -> 'a = val f_deep : bool t -> bool = val f : 'a t -> 'a = The pattern is rather generic (here we can do a bit better by replacing "next" by a recursive call to f_gen actually) : - you first write a generic version of your function where "recursive calls" are taken as arguments - you write a certain number of type-specialized function which are intended to be used as initial "recursive calls". They are themselves really recursive - you write your final function by using the type-specialized ones as "recursive calls" Notice that the use of "recursive calls" in the above is justified since all these functions have precisely the same semantics (and almost the same behaviour once compiled). But if someone has a better vocabulary to describe this practice, I'd gladly adopt it, as I'm not really satisfied with it. (I use "continuations" as well, but it still not quite what we intend). Arnaud