Undecidability of OCaml type checking

From: Andreas Rossberg (rossberg@ps.uni-sb.de)
Date: Mon Jul 12 1999 - 19:20:36 MET DST

Date: Mon, 12 Jul 1999 19:20:36 +0200
From: Andreas Rossberg <rossberg@ps.uni-sb.de>
To: caml-list@inria.fr
Subject: 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

     module type I =
       module type A
       module F :
         functor(X :
           module type A = A
           module F : functor(X : A) -> sig end
         end) -> sig end

     module type J =
       module type A = I
       module F : functor(X : I) -> sig end

     (* Try to check J <= I *)

     module Loop(X : J) = (X : I)

I am sure that Xavier and the other Caml developers are aware of
this. I do not think this behaviour is really a problem, as the
example is really contrived -- nobody would write such code.
Thus I find this property of the language perfectly
acceptable. However, IMHO you should at least document the
fact that type checking is incomplete and compilation may not
terminate due to this.

Best regards,

        - Andreas

[1] Mark Lillibridge
    "Translucent Sums: A Foundation for Higher-Order Modules",
    PhD Thesis, CMU, 1997

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