This site is updated infrequently. For up-to-date information, please visit the new OCaml website at ocaml.org.

Re: type recursifs et abreviations cyclique and Co
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
 Date: -- (:) From: Jason Hickey 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

```