Type issue
[
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:   (:) 
From:  Arnaud Spiwack <Arnaud.Spiwack@l...> 
Subject:  Re: [Camllist] Type issue 
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). Arnaud