Accueil     À propos     Téléchargement     Ressources     Contactez-nous

Ce site est rarement mis à jour. Pour les informations les plus récentes, rendez-vous sur le nouveau site OCaml à l'adresse ocaml.org.

Type issue
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: 2007-11-23 (13:44) From: Vincent Aravantinos Subject: Re: [Caml-list] Type issue
```
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