Re: [Caml-list] type generalization of recursive calls

[Boris Yakobowski <boris@yakobowski.org>]

Hi Gim,

On Wed, Feb 17, 2010 at 5:34 PM, Stéphane Gimenez
<stephane.gimenez@pps.jussieu.fr> wrote:
> Questions:
>  - Is it theoreticaly safe to generalize recursive calls ?

Yes. And this is done in explicitly-typed languages, such as in Coq.

>  - Is there a syntactical trick to use generalized recursive calls ?

Not in the current Ocaml, as type annotations cannot be used to
introduce type polymorphism. However, see below.

>  - Could such a generalization be added to the type checker ?
>      - Performance issues ?
>      - More obfusctated type checking errors ?

Unfotunately, it is worse than that : type inference is undecidable in
the presence of polymorphic recursion. See e.g.
http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.42.3091

> In a related disscution I found, one asked about generalization
> between mutualy recursive definitions (same problem). No answers, but
> maybe I just lack pointers.

If I'm not mistaken, you can encode all cases of polymorphic recursion
using mutual monomorphic recursion. For your example, this would give

let rec map f = function
  | E -> E
  | D (t1, t2) -> D (map f t1, map f t2)
  | O a -> O (f a)
  | I tt -> I (map2 (map f) tt)
and map2 x = map x

Here, map is always called with type ('a -> 'b) -> 'a t -> 'b t inside
its own body (and is instantiated only inside map2). Thus this second
problem is even harder than polymorphic recursion.

Finally, starting from Ocaml 3.13, you can simply write

let rec map : 'a 'b. ('a -> 'b) -> 'a t -> 'b t = fun f -> function
  | E -> E
  | D (t1, t2) -> D (map f t1, map f t2)
  | O a -> O (f a)
  | I tt -> I (map (map f) tt)

Hope this helps,

-- 
Boris