Re: The option -rectypes

From: Gerd Stolpmann (Gerd.Stolpmann@darmstadt.netsurf.de)
Date: Thu Nov 25 1999 - 21:51:21 MET


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