From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <Alain.Frisch@inria.fr>
X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr
X-Spam-Level: 
X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled 
	version=3.1.3
X-Original-To: caml-list@yquem.inria.fr
Delivered-To: caml-list@yquem.inria.fr
Received: from discorde.inria.fr (discorde.inria.fr [192.93.2.38])
	by yquem.inria.fr (Postfix) with ESMTP id D9DCCBC0A
	for <caml-list@yquem.inria.fr>; Wed,  4 Apr 2007 07:27:29 +0200 (CEST)
Received: from smtp3-g19.free.fr (smtp3-g19.free.fr [212.27.42.29])
	by discorde.inria.fr (8.13.6/8.13.6) with ESMTP id l345RT4E031389
	for <caml-list@yquem.inria.fr>; Wed, 4 Apr 2007 07:27:29 +0200
Received: from [192.168.0.1] (rke75-3-82-229-183-156.fbx.proxad.net [82.229.183.156])
	by smtp3-g19.free.fr (Postfix) with ESMTP id 451B15DFE0;
	Wed,  4 Apr 2007 07:27:29 +0200 (CEST)
Message-ID: <46133740.3070305@inria.fr>
Date: Wed, 04 Apr 2007 07:27:28 +0200
From: Alain Frisch <Alain.Frisch@inria.fr>
User-Agent: Icedove 1.5.0.8 (X11/20061116)
MIME-Version: 1.0
To: Jeremy Yallop <jeremy.yallop@ed.ac.uk>
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Polymorphic recursion
References: <6f9f8f4a0704030959l8ebb155g8532e3ee6d31c66d@mail.gmail.com> <46128CEE.2090704@ed.ac.uk>
In-Reply-To: <46128CEE.2090704@ed.ac.uk>
X-Enigmail-Version: 0.94.0.0
Content-Type: text/plain; charset=ISO-8859-1
Content-Transfer-Encoding: 7bit
X-Miltered: at discorde with ID 46133741.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)!
X-Spam: no; 0.00; frisch:01 frisch:01 recursion:01 recursive:01 sig:01 val:01 seq:01 struct:01 seq:01 recursive:01 rewriting:01 struct:01 sig:01 val:01 quantified:01 

Jeremy Yallop wrote:
> Right.  You can write polymorphic-recursive functions if you wrap them
> in recursive modules, though:
> 
>   module rec Size : sig val size : 'a seq -> int end = struct
>     let rec size = function
>       | Unit -> 0
>       | Seq (_, b) -> 1 + 2 * Size.size b
>   end

Note that you don't even need the "rec" in this example, and that the
same idiom would support mutually recursive functions. To make an
automatic translation simpler, you can simply "open Size" at the
beginning of the structure to avoid rewriting self-references in the
function's body. To support local definitions, you can of course rely on
local modules:

let rec f : 'a 'b. t = E1 in E2

becomes:

let module X = struct
  module rec Y : sig val f : t end = struct
    open Y
    let f = E1
  end
  open Y
  let v = E2
end in
X.v

However, this encoding has an important drawback: you cannot use type
variables currently in scope in t, E1, E2 (as a consequence, we don't
need to explicitly quantify over variables in the function prototype,
the encoding forces all the variables in the function's type to be
universally quantified). By changing the encoding, you can allow
references to those type variables in E2:

let f =
 let module X = struct
   module rec Y : sig val f : t end = struct
     open Y
     let f = E1
   end
 end in
 X.Y.f
in
E2


-- Alain