Re: type recursifs et abreviations cyclique and Co
 Jason Hickey
[
Home
]
[ Index:
by date

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