From: Gerd Stolpmann <Gerd.Stolpmann@darmstadt.netsurf.de>
To: caml-list@inria.fr
Subject: Re: The option -rectypes
Date: Thu, 25 Nov 1999 21:51:21 +0100
Message-Id: <99112522264600.07026@ice>
On Wed, 24 Nov 1999, Xavier Leroy wrote:
>> - What is the effect of -rectypes? (I did not find a good explanation in the
>> manual.)
>
>It relaxes the type-checking so that recursive types are accepted
>everywhere. The "standard" behavior is that recursive types are
>rejected if the recursion doesn't cross an object type, e.g.
>
> < m : 'a -> 'a> as 'a
>
>is accepted, but
>
> ('a -> 'a) as 'a
>
>is not.
In my example, the recursion does only formally not cross an object type. If
you expand 'a node extension as 'a, you get
< clone : 'a; node : 'a node; 'a node -> unit > as 'a
Perhaps this is the reason why Ocaml 2.02 accepts the type, and 2.03 does not;
the order when type constructors are expanded might have changed.
Note that Ocaml 2.03 still accepts 'a node #extension as 'a. (Perhaps the
compiler interprets the hash mark as indicator that an "extension" is actually
an object type?)
>The reason for this restriction is that while recursive types
>are a necessity for typing objects, they are a mixed blessing for
>other kinds of types. Granted, they allow more programs to be
>type-checked, but they also lead to programming mistakes not being
>detected by the type-checker, instead the type-checker infers
>nonsensical recursive types. For instance, conside the function
>
> let f x = x @ x
>
>and assume that by mistake I type
>
> let f x = x :: x
>
>instead. Without recursive types, I get a type error. With
>unrestricted recrusive types, f is well-typed but with an essentially
>unusable type
>
> ('a list) as 'a
>
>and attempts to use f later will fail with very strange type error
>messages. We tried to put unrestricted recursive types in one of the
>OCaml releases, and got many, many complains from users telling us
>that this made the language much harder to use, especially for teaching.
This means: It is impossible that an incorrectly typed program can at once be
compiled only because I use an almost undocumented option. The main effect is
that more correctly typed programs can be compiled, and the side effect is that
the quality of error message decreases.
I think that the restriction of recursive types is okay as long as abbreviated
object types are handled permissively.
Gerd
-- ---------------------------------------------------------------------------- Gerd Stolpmann Telefon: +49 6151 997705 (privat) Viktoriastr. 100 64293 Darmstadt EMail: Gerd.Stolpmann@darmstadt.netsurf.de (privat) Germany ----------------------------------------------------------------------------
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:29 MET