Weird behavior with mutually recursive type definitions

Weird behavior with mutually recursive type definitions

[Francois Pottier]

Hello,

I am puzzled by O'Caml 2.02's bizarre behavior regarding mutually recursive
type declarations. 

Let's start by defining a dummy, unary type constructor.

  type 'a dummy = Dummy

(The right-hand side of this definition isn't relevant here; the problem
also shows up when 'a dummy is an abstract type constructor, provided by
a functor argument.)

Then, consider the following type definitions:

  type 'a t = 'a dummy
  type specialized = int t

The first type declaration simply renames ``dummy'' into ``t'', and the second
one creates a specialized instance of it. O'Caml correctly analyzes these
declarations.

Now, here's the problem. Let's change just one word, and make the type
declarations mutually recursive, even though they needn't be:

  type 'a t = 'a dummy
   and specialized = int t

O'Caml still accepts the code, but this time, it constrains 'a to be equal to
int, as if the type constructor t could not be used polymorphically within its
own declaration:

  type 'a t = 'a dummy constraint 'a = int
                       ^^^^^^^^^^^^^^^^^^^
  type specialized = int t

Why is this? Can someone explain, or is it a typechecker bug?

Thanks,

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

Re: Weird behavior with mutually recursive type definitions

[Hendrik Tews]

Francois Pottier writes:

   Date: Wed, 4 Aug 1999 15:52:39 +0200
   Subject: Weird behavior with mutually recursive type definitions
   
   [...]

     type 'a t = 'a dummy
      and specialized = int t
   
   O'Caml still accepts the code, but this time, it constrains 'a
   to be equal to int, as if the type constructor t could not be
   used polymorphically within its own declaration:
   
     type 'a t = 'a dummy constraint 'a = int
                          ^^^^^^^^^^^^^^^^^^^
     type specialized = int t
   
   Why is this? Can someone explain, or is it a typechecker bug?
   
A few month ago we run into the same problem. From a private
conversation with Jacques Garrigue I understood, that the above
behavior is actually a feature of the typechecker, because there
is no better solution known at the moment. :-(

We solved the problem by eliminating type abbreviations (by
replacing it with its expansion) until these constraints
vanished. (You can use option ocamlc -i on your code to see which
constraints are generated.) The elimination of the abbreviations
leads to ugly and unreadable code, but it works at least.

Hope this helps,

Hendrik

Re: Weird behavior with mutually recursive type definitions

[Jacques GARRIGUE]

From: Francois Pottier <Francois.Pottier@inria.fr>

> Now, here's the problem. Let's change just one word, and make the type
> declarations mutually recursive, even though they needn't be:
> 
>   type 'a t = 'a dummy
>    and specialized = int t
> 
> O'Caml still accepts the code, but this time, it constrains 'a to be equal to
> int, as if the type constructor t could not be used polymorphically within its
> own declaration:
> 
>   type 'a t = 'a dummy constraint 'a = int
>                        ^^^^^^^^^^^^^^^^^^^
>   type specialized = int t
> 
> Why is this? Can someone explain, or is it a typechecker bug?

As Hendrik Tews already answered, this is not a bug.
Like value definitions, recursive type abbreviation definitions are
not polymorphic (while they are defined). So if in your defintion you
use the abbreviation at a different type, a constraint is added.

Why is it so? Constraints are required for the object system, and if
there are constraints you must expand abbreviations inside definitions
to check them.  If recursion occurs before the abbreviation is
generalized, this means that all occurences of an abbreviation in the
same type definition will be unified, and have the same constraints.

I personnaly think that, like for polymorphic recursion, the semantics
could be changed so that the user has to write explicitely the
constraints. In type definitions, this makes sense. If a constraint
appears to be needed somewhere and was not declared, there would be an
error.  Technically this would probably mean doing two passes on type
definitions: one to introduce definitions (polymorphically) and one to
check the constraints. In such a way, one could avoid this strange
side-effect of the object system on the rest of the language.

Comments, Jerome ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: Weird behavior with mutually recursive type definitions

[Francois Pottier]

> Why is it so? Constraints are required for the object system, and if
> there are constraints you must expand abbreviations inside definitions
> to check them.  If recursion occurs before the abbreviation is
> generalized, this means that all occurences of an abbreviation in the
> same type definition will be unified, and have the same constraints.

I fail to see why type abbreviations should be monomorphic while
their declaration is being checked. Is this intended to make the
type system safe, or to guarantee the typechecker's termination?

By the way, I find O'Caml's error messages on this topic rather
strange. If I try:

  type 'a t = ('a -> 'a) u
  and 'a u = ('a -> 'a) t

then I obtain

  This type ('a -> 'a) -> 'a -> 'a should be an instance of type 'a

which corresponds to the problem discussed so far. This seems to
indicate that t and u are understood as mutually recursive type
abbreviations. However, if I try:

  type t = u and u = t

then O'Caml answers

  A type variable is unbound in this type declaration

which surprises me. I would rather expect to be warned about
cyclic type abbreviations.

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

Re: Weird behavior with mutually recursive type definitions

[Jacques GARRIGUE]

From: Francois Pottier <Francois.Pottier@inria.fr>

> > Why is it so? Constraints are required for the object system, and if
> > there are constraints you must expand abbreviations inside definitions
> > to check them.  If recursion occurs before the abbreviation is
> > generalized, this means that all occurences of an abbreviation in the
> > same type definition will be unified, and have the same constraints.
> 
> I fail to see why type abbreviations should be monomorphic while
> their declaration is being checked. Is this intended to make the
> type system safe, or to guarantee the typechecker's termination?

My explanation probably lacked clarity.

Since abbreviations may contain constraints, one must expand them when
defining types depending on them (to check that the constraints are
satisfied).

If the abbreviation has been defined earlier, no problem, you just
extract its constraints.

But if it is yet to be defined (which is the case with mutually
recursive definitions), you must keep everything monomorphic so that
constraints can be enforced later.

What we want is just to enforce constraints from the abbreviation to
other type definitions, but as a result this means also introducing
constraints the other way round (classical problem with unification).

My comment was that such a restrictive algorithm is needed if we want
to collect all constraints in one pass, but if we require that all
abbreviation definitions contain explicitely all their constraints,
the above problem can be avoided with a two-pass algorithm.

> By the way, I find O'Caml's error messages on this topic rather
> strange.

Error messages with unification are hard.
You can see here another funny behaviour with recursive definitions:

	# type t = u and u = unit;;
	type t = unit
	type u = t


	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

More confusion with mutually recursive type definitions

[Francois Pottier]

> But if it is yet to be defined (which is the case with mutually
> recursive definitions), you must keep everything monomorphic so that
> constraints can be enforced later.

OK, so I understand the following error message:

  # type 'a t = 'a and u = int t and v = bool t;;
  This type bool should be an instance of type int

But then, why is the following declaration accepted?

  # type 'a t = 'a and u = A of int t and v = B of bool t;;
  type 'a t = 'a
  type u = | A of int t
  type v = | B of bool t

I am still confused...

-- 
François Pottier
Francois.Pottier@inria.fr
http://pauillac.inria.fr/~fpottier/

Re: More confusion with mutually recursive type definitions

[Jacques GARRIGUE]

> OK, so I understand the following error message:
> 
>   # type 'a t = 'a and u = int t and v = bool t;;
>   This type bool should be an instance of type int
> 
> But then, why is the following declaration accepted?
> 
>   # type 'a t = 'a and u = A of int t and v = B of bool t;;
>   type 'a t = 'a
>   type u = | A of int t
>   type v = | B of bool t
> 
> I am still confused...

And ought to be... this is a bug:

        Objective Caml version 2.02

# type 'a t = 'a constraint 'a = int and u = A of int t and v = B of bool t;;
Uncaught exception: Ctype.Unify(_)

Is it already corrected ?

	Jacques
---------------------------------------------------------------------------
Jacques Garrigue      Kyoto University     garrigue at kurims.kyoto-u.ac.jp
		<A HREF=http://wwwfun.kurims.kyoto-u.ac.jp/~garrigue/>JG</A>

Re: Weird behavior with mutually recursive type definitions

[Jerome Vouillon]

On Mon, Aug 16, 1999 at 08:31:58AM +0200, Francois Pottier wrote:

> By the way, I find O'Caml's error messages on this topic rather
> strange. If I try:
> 
>   type 'a t = ('a -> 'a) u
>   and 'a u = ('a -> 'a) t
> 
> then I obtain
> 
>   This type ('a -> 'a) -> 'a -> 'a should be an instance of type 'a
> 
> which corresponds to the problem discussed so far. This seems to
> indicate that t and u are understood as mutually recursive type
> abbreviations. However, if I try:
> 
>   type t = u and u = t
> 
> then O'Caml answers
> 
>   A type variable is unbound in this type declaration
> 
> which surprises me. I would rather expect to be warned about
> cyclic type abbreviations.

In fact, in the latter case, the abbreviations are underspecified :
the expansion of t and u could be any type. When typing this
declaration, the compiler first assumes that the type t expand to some
type variable 'a and then tries to use the equalities t = u and u = t
to refine the expansion. In this case, the expansion remains unchanged
and therefore, the compiler complains that the type t expands to an
unbound type variable 'a.

-- Jérôme

Re: Weird behavior with mutually recursive type definitions

[Jerome Vouillon]

On Fri, Aug 13, 1999 at 10:42:06AM +0900, Jacques GARRIGUE wrote:
> I personnaly think that, like for polymorphic recursion, the semantics
> could be changed so that the user has to write explicitely the
> constraints. In type definitions, this makes sense. If a constraint
> appears to be needed somewhere and was not declared, there would be an
> error.  Technically this would probably mean doing two passes on type
> definitions: one to introduce definitions (polymorphically) and one to
> check the constraints. In such a way, one could avoid this strange
> side-effect of the object system on the rest of the language.
> 
> Comments, Jerome ?

This would indeed be much less confusing.  It is not clear to me how
this can be done, though.

An alternative would be that the compiler automatically sorts the type
definitions so as to eliminate as much mutual recursion as possible.
Then, all correct type abbreviations could be defined using mutually
recursive type definitions and the user would not have to reorder
manually the definitions.

Type representations are already typed after the type abbreviations
have been computed, which explains why the following definition is
accepted:
  type 'a t = 'a and u = A of int t and v = B of bool t;;

-- Jérôme