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
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:13 MET