**Next message:**Jason Hickey: "Re: recursive types"**Previous message:**Fritz Heinrichmeyer: "imenu and ocaml-mode 1.05"**Next in thread:**Xavier Leroy: "Re: recursive types"**Reply:**Xavier Leroy: "Re: recursive types"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

Date: Mon, 24 Nov 1997 23:40:54 -0500 (EST)

Message-Id: <199711250440.XAA25085@cloyd.cs.cornell.edu>

From: Jason Hickey <jyh@cs.cornell.edu>

To: caml-list@inria.fr

Subject: Re: type recursifs et abreviations cyclique and Co

Although my French is not what I would like, I gather that the feature

of general recursive types in OCaml has been drawn back because it is

prone to error. For instance, the type I originally proposed

type x = x option

is not allowed because types of that form are prone to error. The

solution would be to apply an explicit boxing:

type x = X of x option.

I would like to make an argument against this policy.

1. The interpretation of the general recursive type has a

well-defined type theoretic meaning. For instance, the type

type x = x option

is isomorphic to the natural numbers. The _type_theory_ does not

justify removing it from the language. Why not issue a warning rather

than forbidding the construction? 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.

2. The policy imposes a needless efficiency penalty on type

abstraction. For instance, suppose we have an abstract type

type 'a t

then we can't form the recursive type

type x = x t

without a boxing. Although the type

type x = X of x t

is equivalent, it requires threading a lot of superfluous X's through

the code, and ocaml will insert an extraneous boxing for each

occurrence of an item of type x in t. Consider an unlabeled

abstract binary tree:

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

...

type node = X of node t

Every node is boxed, with a space penalty that is

linear in the number of nodes.

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?

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

OCaml compiler should forbid them all!

I use this construction extensively in Nuprl (theorem proving)

and Ensemble (communications) applications; do I really need

to change my code?

Jason

**Next message:**Jason Hickey: "Re: recursive types"**Previous message:**Fritz Heinrichmeyer: "imenu and ocaml-mode 1.05"**Next in thread:**Xavier Leroy: "Re: recursive types"**Reply:**Xavier Leroy: "Re: recursive types"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ]

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