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 = <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:
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 = <fun>
val f_deep : bool t -> bool = <fun>
val f : 'a t -> 'a = <fun> 


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