Date: Wed, 14 Jul 1999 17:32:06 +0200
From: Xavier Leroy <Xavier.Leroy@inria.fr>
To: Andreas Rossberg <rossberg@ps.uni-sb.de>, caml-list@inria.fr
Subject: Re: Undecidability of OCaml type checking
In-Reply-To: <378A23E4.ECEDD6DB@ps.uni-sb.de>; from Andreas Rossberg on Mon, Jul 12, 1999 at 07:20:36PM +0200
> 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
This archive was generated by hypermail 2b29 : Sun Jan 02 2000 - 11:58:23 MET