Undecidability of OCaml type checking

Undecidability of OCaml type checking

[Andreas Rossberg]

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:

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

     module type J =
     sig
       module type A = I
       module F : functor(X : I) -> sig end
     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

irritability of structure name conflicts

[Dave Mason]

I have the following as part of a type declaration:
	and variable = {name:scheme; mutable value:scheme; next:variable}
	and field = {fname:scheme;
		     fclass:scheme;
		     finit:scheme option;
		     fnext:field}
	and clause = {tags:scheme list;code:scheme list}
	and binding = {id:int;mutable set:bool;value:scheme}

all of which compiles fine, but I get the error:
	The label value belongs to the type Types.binding
	but is here mixed with labels of type Types.variable
at a line that says, in part:
	 {name=sym;value=r;next=symbol_table.(idx)}

I didn't get the error before I added the field type!  I'm (a)
confused, and (b) irritated that I have to keep making up names for
labels!

Is there some way I can force it to interpret the type constructor as
a particular type so that it chooses the labels from the correct set?

Thanks	../Dave

Re: irritability of structure name conflicts

[John Skaller]

At 13:59 13/07/99 -0400, Dave Mason wrote:
>Is there some way I can force it to interpret the type constructor as
>a particular type so that it chooses the labels from the correct set?

This problem pervades ocaml. Another case of it is variants:

	type A = X | Y;
	type B = X | Z;

which all compiles fine, but then X is a constructor for
the B variant.

C also has the same problem with enumerations:

	enum X {a,b,c}; /* a,b,c are globals */

The problem can be solved, clumbsily, by wrapping inside a module.
(In C++, inside a class or namespace)

While I'm also expressing irritation, when I compile
a file (as opposed to using the interactive system);
rebinding of symbols shouldn't be allowed:

	let a = 1;;
	...
	let a = 1.0;;
	...
	print_int a;; 

	(* what does that strange type error mean! 
   	   a is an integer! It is right there at the top of the file!
	*)

Another similar case is 

	open List
	open Map
	iter ... 

Woops! I meant List.iter, not Map.iter :-)

There are several solutions, but the one that could
be implemented now with least impact would be to
issue warnings whenever a symbol is rebound
in the same scope during batch compilation.

(No warning in the interactive system; rebinding
to fix mistakes is common)

-------------------------------------------------------
John Skaller    email: skaller@maxtal.com.au
		http://www.maxtal.com.au/~skaller
		phone: 61-2-96600850
		snail: 10/1 Toxteth Rd, Glebe NSW 2037, Australia

Re: Undecidability of OCaml type checking

[Xavier Leroy]

> 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

Re: irritability of structure name conflicts

[Xavier Leroy]

> I didn't get the error before I added the field type!  I'm (a)
> confused, and (b) irritated that I have to keep making up names for
> labels!

I agree it's an unpleasant feature of Caml, caused by the way we do
type inference on record accesses.  E.g. if a label "lbl" could belong
to two named record types t1 and t2, "fun x -> x.lbl" would have
two types "t1 -> ..." and "t2 -> ..."

> Is there some way I can force it to interpret the type constructor as
> a particular type so that it chooses the labels from the correct set?

Currently no, but we discussed several possible approaches on this
list a while ago.  If you're interested, you can search the archives
at http://caml.inria.fr/.  (The subject line was "CamlIDL - stub code
generator and COM binding for OCaml".)

Best,

- Xavier Leroy