Re: recursive datatypes

[Xavier Leroy <Xavier.Leroy@inria.fr>]

> Why does Caml type-check the following program? It wouldn't in Standard ML
> and I don't see the use for it, as it may lead to infinite programs...
> type 'a tree = Tree of 'a
> let f x = Tree (f x)

Objective Caml supports recursive types (i.e. type expressions with
cycles) because the object types need them, in particular in
situations involving binary methods.

The simplest implementation is to allow recursion in types almost
anywhere.  That's what the current 1.05 release of OCaml does.

The main drawback with this is that a number of programming errors
result in programs being well-typed with weird recursive types,
instead of being rejected by the type system as in a normal (no
recursive types) type system.  (BTW, the argument with "infinite
programs" doesn't hold, as there is nothing you can do with recursive
types that you can't do with datatypes, including embeddings of the
untyped lambda-calculus.)

For this reason, the next release of OCaml will restrict recursive
types in such a way that the recursion must go through an object type.
That should match everyone's intuitive expectations about the type
system, though it probably rules out a few cool examples.

- Xavier Leroy