Le 23 nov. 07 à 14:38, Arnaud Spiwack a écrit :

> 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).

This is just wonderful !

Thanks,
V.