Re: The option -rectypes

[Gerd Stolpmann <Gerd.Stolpmann@darmstadt.netsurf.de>]

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                     
----------------------------------------------------------------------------