From mboxrd@z Thu Jan  1 00:00:00 1970
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id JAA19832 for caml-redistribution; Tue, 25 Nov 1997 09:20:21 +0100 (MET)
Received: from nez-perce.inria.fr (nez-perce.inria.fr [192.93.2.78]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id FAA17592 for <caml-list@pauillac.inria.fr>; Tue, 25 Nov 1997 05:41:06 +0100 (MET)
Received: from simon.cs.cornell.edu (SIMON.CS.CORNELL.EDU [128.84.154.10])
	by nez-perce.inria.fr (8.8.7/8.8.5) with ESMTP id FAA06802
	for <caml-list@inria.fr>; Tue, 25 Nov 1997 05:41:03 +0100 (MET)
Received: from cloyd.cs.cornell.edu (CLOYD.CS.CORNELL.EDU [128.84.227.15])
	by simon.cs.cornell.edu (8.8.5/8.8.5/R-1.8) with ESMTP id XAA21221;
	Mon, 24 Nov 1997 23:41:01 -0500 (EST)
Received: from JAOQUIN (CS-ANNEX-1-07.CS.CORNELL.EDU [128.84.254.37])
	by cloyd.cs.cornell.edu (8.8.5/8.8.5/M-1.9) with SMTP id XAA25085;
	Mon, 24 Nov 1997 23:40:54 -0500 (EST)
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
cc: crary@cs.cornell.edu, hayden@cs.cornell.edu,
        Olivier Montanuy <montanuy@lannion.cnet.fr>,
        Emmanuel Engel <Emmanuel.Engel@lri.fr>,
        Jerome Vouillon <vouillon@clipper.ens.fr>,
        Francisco Valverde <fva@tsc.uc3m.es>
Subject: Re: type recursifs et abreviations cyclique and Co
Sender: weis

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