The option -rectypes

The option -rectypes

[Gerd Stolpmann]

I have some code that compiled in 2.02, but in 2.03 I need the new option
-rectypes of the compilers.

My class definitions look like (the signatures)

class type [ 'node ] extension =
  object ('self)
    method clone : 'self 
    method node : 'node
    method set_node : 'node -> unit
  end
;;

class type [ 'ext ] node =
  object ('self)
    constraint 'ext = 'ext node #extension
    method extension : 'ext
    (* ... more methods ... *)
  end
;;

This works in both versions out of the box. If I add 

val f : 'a node extension as 'a

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.)
- What is the background of this change?
- 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.

Gerd
--
----------------------------------------------------------------------------
Gerd Stolpmann      Telefon: +49 6151 997705 (privat)
Viktoriastr. 100             
64293 Darmstadt     EMail:   Gerd.Stolpmann@darmstadt.netsurf.de (privat)
Germany                     
----------------------------------------------------------------------------

Re: The option -rectypes

[Pascal Cuoq]

> I have some code that compiled in 2.02, but in 2.03 I need the new option
> -rectypes of the compilers.
> 
> - What is the background of this change?

I can't say much about your example, but maybe I can say a few
words about the context.  I was one of the people who lobbied
to have at least a compiler option to allow recursive types.

The application in which we needed recursive types in Caml is
Lucid Synchrone, a strongly typed, higher-order synchronous language
which uses Ocaml as its target language:
http://www-spi.lip6.fr/~pouzet/lucid-synchrone/

In this kind of application, the type system of Ocaml only can get in
the way, because Lucid Synchrone already type-checks the
Lucid Synchrone programs.  It happens to be that (roughly) a well-typed
Lucid Synchrone program is compiled in an Ocaml program which 
is well-typed if recursive types are accepted, and ill-typed if they
aren't.

The Caml implementors will probably tell you that the use of this
flag is discouraged for hand-written programs.  This "feature" was
removed from Ocaml 1.05 for a good reason (the type-checker reports
errors too late) and it should not be used lightly.

This said, there must be another change in the objects systems
which explains that your program is rejected without -rectypes.

Pascal

Re: The option -rectypes

[Xavier Leroy]

> 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

Re: The option -rectypes

[Anton Moscal]

On Wed, 24 Nov 1999, Xavier Leroy wrote:

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

May be will be better to produce warning instead of error about recursive
types, if no -rectypes specified?

Regards,
Anton Moscal

Re: The option -rectypes

[Stefan Monnier]

>>>>> "Anton" == Anton Moscal <msk@post.tepkom.ru> writes:
> May be will be better to produce warning instead of error about recursive
> types, if no -rectypes specified?

Or to not infer recursive types but to accept them in type annotations?


	Stefan

Re: The option -rectypes

[Gerd Stolpmann]

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

Re: The option -rectypes

[Jerome Vouillon]

On Wed, Nov 24, 1999 at 01:59:36AM +0100, Gerd Stolpmann wrote:
> I have some code that compiled in 2.02, but in 2.03 I need the new option
> -rectypes of the compilers.

This is a bug in the occur check. It will be corrected in the next
release.

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

The type of self cannot be unified with closed object type: this would
prevent a further extension of the class.  But a type such as
#extension can be unified with a closed object type.  In particular,
it can always be unified with the same type without "#".

-- Jérôme