**Next message:**Xavier Leroy: "Re: Deletion of ioctl_ptr in Caml 1.06"**Previous message:**Jason Hickey: "Re: recursive types"**In reply to:**Jason Hickey: "Re: type recursifs et abreviations cyclique and Co"**Next in thread:**Cuoq Pascal: "Re: type recursifs et abreviations cyclique and Co"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

From: Xavier Leroy <Xavier.Leroy@inria.fr>

Message-Id: <199711251009.LAA22148@pauillac.inria.fr>

Subject: Re: recursive types

In-Reply-To: <199711250440.XAA25085@cloyd.cs.cornell.edu> from Jason Hickey at "Nov 24, 97 11:40:54 pm"

To: jyh@cs.cornell.edu (Jason Hickey)

Date: Tue, 25 Nov 1997 11:09:04 +0100 (MET)

Here is the straight dope (or my view of it, anyway) about recursive

types, or more precisely, the fact that all recursive type expressions

are no longer allowed in OCaml 1.06:

1- It is true that recursive (infinite) type expressions such as

'a where 'a = 'a list (standing for the infinite type

... list list list list

can be added to the ML type system without causing major theoretical

difficulties. In particular, unification and type inference work just

as well on recursive types (infinite terms) than on regular types

(finite terms).

2- "Classic" ML does not have recursive types, just finite terms as

type expressions. Except some versions of Objective Caml, you won't

find any implementation of ML that accepts them.

3- The reason Objective Caml supports recursive types is that they are

absolutely needed by the object stuff. More precisely, recursive

types naturally arise when doing type inference for objects (without

prior declarations of object types). Hence, Objective Caml performs

type inference using full recursive types (cyclic terms) internally.

4- Still (and now comes the language design issue), one may decide to

impose extra restrictions on type expressions, such as "all cycles in

a type must go through an object type", thus prohibiting recursive

types that don't involve object types, such as ... list list list above.

In OCaml, we have experimented with several such restrictions. I

think early releases (up to 1.04) had restrictions, though I don't

remember which; 1.05 had no restrictions at all, and was strongly

criticized for that (see below); 1.06 has the "all cycles must go

through an object type" restriction.

5- The main problem with unrestricted recursive types is that they

allow type inference to give nonsensical types to clearly wrong code,

instead of issuing a type error immediately. For instance, consider

the function

let f x y = if ... then x @ y else x

Assume I make a typo and type "@" instead of "::" :

let f x y = if ... then x :: y else x

Any sane ML implementation reports a type error. But OCaml 1.05 (the

one with unrestricted types) would accept the definition above, and

infer the deeply obscure type:

val f : ('a list as 'a) -> ('b list as 'b) list -> ('c list as 'c)

Calls to the function f will probably be ill-typed, so the error will

eventually be caught, but possibly very far from the actual error (the

definition of f).

Some users of OCaml 1.05 loudly complained that unrestricted recursive

types make the language much harder to use for beginners and

intermediate programmers. We agreed that they had a strong point

here. You don't want types such as the above for f. Really. Trust me.

So we and decided to go back to recursive types restricted to objects

only --- the reasoning being that this does not reject any "classic"

ML code (which type-checks without recursive types already), but still

lets the right types for objects being inferred.

6- Of course, we forgot that users would exploit the "unrestricted

recursive types" bug of OCaml 1.05, and come back at us claiming it's

a useful feature. So, let's see how useful are recursive types that

are not objects. I'm taking Jason Hickey's examples here.

*> type x = x option
*

*> the type "x" should probably be isomorphic to the natural numbers
*

Such a type can be written more clearly as type x = Z | S of x

(or even better type x = int, but that's a different story).

*> Consider an unlabeled abstract binary tree:
*

*>
*

*> type 'a t = ('a option) * ('a option) (* abstract *)
*

*> ...
*

*> type node = X of node t
*

Again, I don't see the point of the 'a t type. A much clearer way to

describe unlabeled binary trees is:

type node = Empty | Node of node * node

Notice: no extra boxing here.

The point I'm trying to make here is that pretty much all the time,

recursive types can be avoided ad clarity of the code can be improved

by using the right concrete types (sums or records) to hide the

recursion, rather than using generic sum or product types such as

"option" and "*", then obtain the desired recursive structure by using

recursive type expressions.

I know of only one or two cool examples where recursive type

expressions come in handy and avoid code duplication that the regular

ML type system forces you to do otherwise.

Now, in reply to Jason Hickey's points:

*> 1. The interpretation of the general recursive type has a
*

*> well-defined type theoretic meaning.
*

Yes, but this doesn't imply it's a desirable feature in a programming

language.

*> Why not issue a warning rather than forbidding the construction?
*

That's one option, though issuing meaningful warnings is probably

harder than just rejecting the program. Another option we discussed

is a command-line flag that changes the behavior of the type-checker

w.r.t. recursive types.

*> For instance, the following code is
*

*> not forbidden:
*

*> let flag = (match List.length [] with 0 -> true)
*

*> even though constructions of this form are "prone to error,"
*

*> and generate warning messages.
*

Right. Some of us think all warnings should be errors, though. In

this particular case, upward compatibility with the "classic ML" way

leads to accepting the program and just issue a warning. For

recursive types, the same argument argues in favor of rejecting the

program.

*> 2. The policy imposes a needless efficiency penalty on type
*

*> abstraction.
*

Only if you don't hide the recursion inside the abstraction, and

insist on taking fixpoints outside the abstraction. As I've shown

before, the penalty can almost always be avoided by writing your

concrete types in a "natural" style. Anyway (warning--silly joke

ahead), since when type theorists are worried about efficiency? (end

of silly joke).

*> 3. If the type system can be bypassed with an extraneous boxing,
*

*> type x = x t -----> type x = X of x t
*

*> then what is the point?
*

The programmers write the "X" constructor explicitely in the program,

thus making their intentions clear. It's completely different from an

inferred recursive type, which is more often than not an unintended

consequence of a coding error.

*> 4. (Joke) All significant programs are "prone to error." Perhaps the
*

*> OCaml compiler should forbid them all!
*

This is an old Usenet-style argument. Another (joke) conclusion is

that for the same reasons, we should turn off all type-checking and

error checking in the compiler.

*> I use this construction extensively in Nuprl (theorem proving)
*

*> and Ensemble (communications) applications; do I really need
*

*> to change my code?
*

We should have released 1.06 earlier; this would have left you less

time to exploit 1.05's bugs so thoroughly... At any rate, I'd

certainly encourage you to think about the data structures you use,

and whether you couldn't rewrite them in a clearer way by getting rid

of recursive types and using Caml's concrete datatypes (sums and

records) instead. Of course, if you come up with convincing real-life

examples (not just type-theoretic examples) of why recursive types are

useful, we'll reconsider.

- Xavier Leroy

**Next message:**Xavier Leroy: "Re: Deletion of ioctl_ptr in Caml 1.06"**Previous message:**Jason Hickey: "Re: recursive types"**In reply to:**Jason Hickey: "Re: type recursifs et abreviations cyclique and Co"**Next in thread:**Cuoq Pascal: "Re: type recursifs et abreviations cyclique and Co"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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