From mboxrd@z Thu Jan  1 00:00:00 1970
Return-Path: weis
Received: (from weis@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id XAA10367 for caml-redistribution; Wed, 24 Nov 1999 23:26:13 +0100 (MET)
Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id VAA00380 for <caml-list@pauillac.inria.fr>; Wed, 24 Nov 1999 21:58:15 +0100 (MET)
Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35])
	by concorde.inria.fr (8.8.7/8.8.7) with ESMTP id VAA24183;
	Wed, 24 Nov 1999 21:56:30 +0100 (MET)
Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id VAA27353; Wed, 24 Nov 1999 21:56:30 +0100 (MET)
Message-ID: <19991124215630.05496@pauillac.inria.fr>
Date: Wed, 24 Nov 1999 21:56:30 +0100
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Gerd.Stolpmann@darmstadt.netsurf.de, caml-list@inria.fr
Subject: Re: The option -rectypes
References: <99112402223302.32002@ice>
Mime-Version: 1.0
Content-Type: text/plain; charset=us-ascii
X-Mailer: Mutt 0.89.1
In-Reply-To: <99112402223302.32002@ice>; from Gerd Stolpmann on Wed, Nov 24, 1999 at 01:59:36AM +0100
Sender: weis

> val f : 'a node extension as 'a

I'm actually surprised that this works in 2.02, because it's a
recursive type where the recursion doesn't go through an (explicit)
object type (see below).

> the 2.03 compiler only accepts the type if I add -rectypes. I have several
> questions:
> 
> - 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.  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.

> - What is the background of this change?

The main reason for adding this (still experimental) -rectypes flag is
to support a couple of research project that involve "compiling" some other
languages (namely, the join-calculus and a reactive language) into
OCaml.  For those encodings, it is important to have unrestricted
recursive types in the target language.

The second reason is to allow users to play with recursive types and
maybe even use them in their programs if they think that the benefits
outweight the late detection of stupid errors illustrated above.

> - I have thought about the type 'a node extension as 'a. If I apply the
>   constraint of "node", the condition must hold that 
>       ('a node extension as 'a) node extension 
>   unifies with
>       ('a node extension as 'a) node #extension
>   Normally, a closed class type does not unify with an open class type,
>   and I wonder why this is accepted at all.
> 
>   Without -rectypes, the 2.03 compiler only accepts
>       val f : 'a node #extension as 'a
>   but this is a much more difficult type.

I pass.  Maybe one of our OO typing gurus will answer this.

- Xavier Leroy