[Caml-list] 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

_______________________________________________
Caml-list mailing list. Subscription management:
http://yquem.inria.fr/cgi-bin/mailman/listinfo/caml-list
Archives: http://caml.inria.fr
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs

[Damien Guichard]

Hello,

First, you really need strong tyupe checking because your definition is actually
incorrect.

Second, see polymorphic-recursion :
http://alaska-kamtchatka.blogspot.com/2009/05/polymorphic-recursion.html

Be sure to read the comments by bluestorm.

There is also pa_polyrec, a syntax extension for polymorphic recursion in OCaml
:
http://www.mail-archive.com/caml...@yquem.inria.fr/msg04795.html

Finally, here is your (corrected) code using vanilla ocaml :

type map =
{ map : 'a 'b. ('a -> 'b) -> 'a t -> 'b t }
let map =
let rec map =
{ map = fun f -> function
| E -> E
| D (t1, t2) -> D (map.map f t1, map.map f t2)

| O a -> O (f a)

| I tt -> I (map.map (map.map f) tt)
}
in map.map

- damien

Le 17/02/2010 à 17:34:24, "Stéphane Gimenez" <stephane...@pps.jussieu.fr>
à écrit :

--
Mail created using EssentialPIM Free - www.essentialpim.com

[Damien Guichard]

I have to apologize because your definition is actually correct.
Sorry i have read it too fast and didn't see map burried in type casting.

It seems to me your are doing structural recursion on some binary tree structure.
Presumably to fast-merge binary heaps or something like that.
pa_polyrec is probably a must have for such things.

[Boris Yakobowski]

Hi Gim,

On Wed, Feb 17, 2010 at 5:34 PM, St�phane Gimenez
<stephane...@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

[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

[Boris Yakobowski]

On Wed, Feb 17, 2010 at 9:25 PM, Dario Teixeira <dariot...@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

[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".