Version française
Home     About     Download     Resources     Contact us    
Browse thread
Undecidability of OCaml type checking
[ Home ] [ Index: by date | by threads ]
[ Search: ]

[ Message by date: previous | next ] [ Message in thread: previous | next ] [ Thread: previous | next ]
Date: -- (:)
From: Xavier Leroy <Xavier.Leroy@i...>
Subject: Re: Undecidability of OCaml type checking
> 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