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 SAA21240 for caml-redistribution; Wed, 14 Jul 1999 18:08:36 +0200 (MET DST) 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 RAA19578 for ; Wed, 14 Jul 1999 17:32:08 +0200 (MET DST) 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 RAA07514; Wed, 14 Jul 1999 17:32:07 +0200 (MET DST) Received: (from xleroy@localhost) by pauillac.inria.fr (8.7.6/8.7.3) id RAA24796; Wed, 14 Jul 1999 17:32:06 +0200 (MET DST) Message-ID: <19990714173206.15615@pauillac.inria.fr> Date: Wed, 14 Jul 1999 17:32:06 +0200 From: Xavier Leroy To: Andreas Rossberg , caml-list@inria.fr Subject: Re: Undecidability of OCaml type checking References: <378A23E4.ECEDD6DB@ps.uni-sb.de> Mime-Version: 1.0 Content-Type: text/plain; charset=us-ascii X-Mailer: Mutt 0.89.1 In-Reply-To: <378A23E4.ECEDD6DB@ps.uni-sb.de>; from Andreas Rossberg on Mon, Jul 12, 1999 at 07:20:36PM +0200 Sender: weis > I have been working through Mark Lillibridge's thesis on > translucent sums [1] recently. One main result of his work is > the undecidability (semi-decidability) of subtyping in his > system. Since the module system in OCaml is in many aspects > very similar to his system, I tried to code one of his > undecidable examples in OCaml. And it was indeed possible, the > following input will send the type checker into an infinite > loop: Right. I knew that manifest module types in OCaml modules lead to the same undecidability problem that Lillibridge's system has. However, I never wrote down the example, and the published papers on the OCaml module systems don't formalize the module types as components of structures. (I believe that type-checking is decidable in the absence of manifest module types in signatures.) Best regards, - Xavier Leroy