Re: Weird behavior with mutually recursive type definitions

From: Francois Pottier (Francois.Pottier@inria.fr)
Date: Mon Aug 16 1999 - 08:31:58 MET DST


Date: Mon, 16 Aug 1999 08:31:58 +0200
From: Francois Pottier <Francois.Pottier@inria.fr>
To: Jacques GARRIGUE <garrigue@kurims.kyoto-u.ac.jp>
Subject: Re: Weird behavior with mutually recursive type definitions
In-Reply-To: <19990813104206X.garrigue@kurims.kyoto-u.ac.jp>; from Jacques GARRIGUE on Fri, Aug 13, 1999 at 10:42:06AM +0900

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



This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:24 MET