From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: <alain@frisch.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=AWL 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 47EA8BC69
	for <caml-list@yquem.inria.fr>; Fri, 23 Nov 2007 10:14:58 +0100 (CET)
X-IronPort-Anti-Spam-Filtered: true
X-IronPort-Anti-Spam-Result: AgAAAFopRkfB/BYdlmdsb2JhbACPNgEBAQEHBAYREQc
X-IronPort-AV: E=Sophos;i="4.21,455,1188770400"; 
   d="scan'208";a="19597320"
Received: from smtp20.orange.fr ([193.252.22.29])
  by mail4-smtp-sop.national.inria.fr with ESMTP; 23 Nov 2007 10:14:57 +0100
Received: from me-wanadoo.net (localhost [127.0.0.1])
	by mwinf2017.orange.fr (SMTP Server) with ESMTP id C87FB1C0009F
	for <caml-list@yquem.inria.fr>; Fri, 23 Nov 2007 10:14:57 +0100 (CET)
Received: from [192.168.1.59] (APuteaux-154-1-25-148.w83-199.abo.wanadoo.fr [83.199.80.148])
	by mwinf2017.orange.fr (SMTP Server) with ESMTP id 9BC4D1C0009A;
	Fri, 23 Nov 2007 10:14:57 +0100 (CET)
X-ME-UUID: 20071123091457638.9BC4D1C0009A@mwinf2017.orange.fr
Message-ID: <47469A02.6010503@frisch.fr>
Date: Fri, 23 Nov 2007 10:14:42 +0100
From: Alain Frisch <alain@frisch.fr>
User-Agent: Thunderbird 2.0.0.9 (Windows/20071031)
MIME-Version: 1.0
To: Jonathan T Bryant <jtbryant@valdosta.edu>
Cc: caml-list@yquem.inria.fr
Subject: Re: [Caml-list] Type issue
References: <2921298.1195790493072.JavaMail.jtbryant@valdosta.edu>
In-Reply-To: <2921298.1195790493072.JavaMail.jtbryant@valdosta.edu>
Content-Type: text/plain; charset=UTF-8; format=flowed
Content-Transfer-Encoding: 7bit
X-Spam: no; 0.00; frisch:01 frisch:01 bool:01 bool:01 val:01 recursion:01 recursive:01 occurences:01 recursive:01 sig:01 val:01 struct:01 hen:98 polymorphic:01 wrote:01 

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 = <fun>

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:

module rec M : sig val f : 'a t -> 'a end =
   struct
     let rec f t = match t with
     | Cond (c,t,e) -> if M.f c then f t else f e
     | Value x -> x
   end

let f = M.f


-- Alain