Re: recursive datatypes

From: Xavier Leroy (Xavier.Leroy@inria.fr)
Date: Wed Nov 12 1997 - 16:05:56 MET


From: Xavier Leroy <Xavier.Leroy@inria.fr>
Message-Id: <199711121505.QAA07586@pauillac.inria.fr>
Subject: Re: recursive datatypes
In-Reply-To: <Pine.A32.3.96.971111174455.16668X-100000@meijin> from Simon Helsen at "Nov 11, 97 05:51:35 pm"
To: helsen@informatik.uni-tuebingen.de (Simon Helsen)
Date: Wed, 12 Nov 1997 16:05:56 +0100 (MET)

> 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



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:12 MET