Version française
Home     About     Download     Resources     Contact us    

This site is updated infrequently. For up-to-date information, please visit the new OCaml website at

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: Andreas Rossberg <rossberg@p...>
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