type generalization of recursive calls

type generalization of recursive calls

[Stéphane Gimenez]

Hi,

I just realized that ocaml generalizes the type of a recursively
defined function *only* for calls which are outside it's own
definition. Recursive calls cannot use a generalized type.

In fact, I'm tring to work with such a data type:

type 'a t =
  | E
  | D of 'a t * 'a t
  | O of 'a
  | I of 'a t t

And, I'm forced to use some dark magic to define simple operations on
it:

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

Questions:
  - Is it theoreticaly safe to generalize recursive calls ?
  - Is there a syntactical trick to use generalized recursive calls ?
  - Could such a generalization be added to the type checker ?
      - Performance issues ?
      - More obfusctated type checking errors ?

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

Cheers,
Stéphane

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

[Boris Yakobowski]

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

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

[Dario Teixeira]

Hi,

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

Assuming "3.13" is not a typo, and that you do not actually mean the
upcoming 3.12, what features can we expect in future versions of Ocaml?

Just curious,
Dario Teixeira

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

[Boris Yakobowski]

On Wed, Feb 17, 2010 at 9:25 PM, Dario Teixeira <darioteixeira@yahoo.com> wrote:
> Assuming "3.13" is not a typo, and that you do not actually mean the
> upcoming 3.12, what features can we expect in future versions of Ocaml?

Sorry, I went too far. I indeed meant 3.12.

-- 
Boris

Re: type generalization of recursive calls

[Stéphane Gimenez]

Hi,

Thanks for your answers. Thanks to Damien for the handy
workarounds and to Boris for the sevral insightful comments.

I'll probably switch to the svn version, waiting for 3.12...

I think 3.13 was a typo, see:
  http://caml.inria.fr/svn/ocaml/trunk/Changes

Stéphane

PS:
btw, looks like coq is not really fond of this data type:

Inductive t a : Type :=
  | E : t a
  | D : t a -> t a -> t a
  | O : a -> t a
  | I : t (t a) -> t a
.

Error: Non strictly positive occurrence of "t" in "t (t a) -> t a".