Type issue

Jonathan T Bryant
 Andrej Bauer
 Florian Weimer

Alain Frisch

Arnaud Spiwack
 Vincent Aravantinos

Arnaud Spiwack
 Oliver Bandel
 Angela Zhu
[
Home
]
[ Index:
by date

by threads
]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
[ Message by date: previous  next ] [ Message in thread: previous  next ] [ Thread: previous  next ]
Date:  20071123 (13:44) 
From:  Vincent Aravantinos <vincent.aravantinos@y...> 
Subject:  Re: [Camllist] 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 typespecialized function which are > intended to be used as initial "recursive calls". > They are themselves really recursive >  you write your final function by using the typespecialized 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.