I had a dream: make the best printed book. For that goal I wrote a lot of code in Ocaml during the last years:
Now this dream is endangered. The bugs in Ocaml make it impossible to use it. It was a hard way towards my decision to drop Ocaml. Where can I go from here? Should I convert all of my code to SML by some sed-hackery? Should I start anew in a sane, better-defined language like scheme?
Some months ago I had to find the reason behind the mysterious infrequent crashes my programm suffered. After some investigations it turned out that the Ocaml compiler shows a questionable understanding of type checking. (Mind: Due to a missing formal definition of the Ocaml language this can not be named a bug. The compiler is its own definition; this could be not the best idea.) All examples are for ocaml-3.12.1. Everything should also apply to other versions just references to line numbers in the source code change.
module type S = sig val x : 'a list end module M : S = struct let x : int list =  end
Yields this message:
Error: Signature mismatch: Modules do not match: sig val x : int list end is not included in S Values do not match: val x : int list is not included in val x : 'a list
But this compiles without complaints:
module type S = sig val x : int list ref end module M : S = struct let x : 'a list ref = ref  end
This is inconvenient but not that dangerous. But consider this:
module type S = sig val sum : int list -> int end module F = functor(A : S) -> struct let get_sum : 'a list -> 'a = A.sum end module M = F(struct let sum = List.fold_left (+) 0 end) (* let s = M.get_sum [ 2.3; 45.43];; *)
The compiler accepts this and says:
module type S = sig val sum : int list -> int end module F : functor (A : S) -> sig val get_sum : int list -> int end module M : sig val get_sum : int list -> int end
Only if we uncomment the last line there is an error message:
File "/tmp/TESTS/cv1.ml", line 9, characters 20-23: Error: This expression has type float but an expression was expected of type '1114a
The reason for this strange behaviour is hidden in typing/includecore.ml:
27 let value_descriptions env vd1 vd2 = 28 if Ctype.moregeneral env true vd1.val_type vd2.val_type then begin
because in typing/includemod.ml we read:
43 (* All functions "blah env x1 x2" check that x1 is included in x2, 44 i.e. that x1 is the type of an implementation that fulfills the 45 specification x2. If not, Error is raised with a backtrace of the error. *)
but Ctype.moregeneral works the other way: it checks if its first argument is more general than its second. Therefore line 28 of typing/includecore.ml should read:
28 if Ctype.moregeneral env true vd2.val_type vd1.val_type then begin
But then hell breaks loose and the ocaml-suite can not be build anymore. That change triggers some serious issues in Ctype.unify and Typecore that I neglect at this moment (no notion of contravariant function arguments because this implementation of unification has no idea of direction; some names are bound too early; some things should stay unbound, etc.)
With variants the situation gets really strange independent of the problem in line 28 of typing/includecore.ml. Trying "ocamlc -i" on:
1 module type S1 = sig 2 val count : [ `A | `B] list -> int 3 end 4 module F1 = functor(A : S1) -> struct 5 let get_count : [ `A] list -> 'a = A.count 6 end 7 module M1 = F1(struct let count = List.length end)
File "/tmp/TESTS/cv0a.ml", line 5, characters 37-44: Error: This expression has type [ `A | `B ] list -> int but an expression was expected of type [ `A ] list -> 'a The second variant type does not allow tag(s) `B
and trying "ocamlc -i" on:
1 module type S2 = sig 2 val count : [ `A] list -> int 3 end 4 module F2 = functor(A : S2) -> struct 5 let get_count : [ `A | `B] list -> 'a = A.count 6 end 7 module M2 = F2(struct let count = List.length end)
File "/tmp/TESTS/cv0b.ml", line 5, characters 42-49: Error: This expression has type [ `A ] list -> int but an expression was expected of type [ `A | `B ] list -> 'a The first variant type does not allow tag(s) `B
One part of this problem is due to a missing resp. broken handling of contravariant function arguments, the other part could be a problem when unifying variant rows because this:
1 module type S1 = sig 2 val count : [< `A | `B] list -> int 3 end 4 module F1 = functor(A : S1) -> struct 5 let get_count : [`A] list -> 'a = A.count 6 end 7 module M1 = F1(struct let count = List.length end)
compiles with "ocamlc -i" as:
module type S1 = sig val count : [< `A | `B ] list -> int end module F1 : functor (A : S1) -> sig val get_count : [ `A ] list -> int end module M1 : sig val get_count : [ `A ] list -> int end
There is not only a missing handling of contravariance but Ctype.unify resp. Ctype.unify2 doesn't really care about direction, see line 1612 of ctype.ml:
1609 if (t1 == t1') || (t2 != t2') then 1610 unify3 env t1 t1' t2 t2' 1611 else 1612 try unify3 env t2 t2' t1 t1' with Unify trace -> 1613 raise (Unify (List.map (fun (x, y) -> (y, x)) trace))
while every caller of Ctype.unify trys to maintain the same ordering when matching a computed type against an expected type; but this is in vain because switching the arguments in line 1612 destroy that ordering.
For most of the problems in Ctype and Typecore there will be a closer examination with suggestions on how to fix them.
Update Fri Jan 17 04:08:33 CET 2014: I mixed things up, got confused and wrote total rubbish about a non-existing error in typing/ctype.ml:499 in the next paragraph. Hopefully this update will get everything corrected.
Here I'll just mention two really scary things. Look at this definition in ocamldoc/odoc_html.ml (omitting some details):
197 class virtual text = 198 object (self) ... 456 method virtual html_of_info_first_sentence : _ ... 517 end
This is accepted by the compiler as can be seen by doing "make ocamldoc". But trying to compile the very much simplified version without all the details:
class virtual text = object(self) method virtual html_of_info_first_sentence : _ end
yields this error:
File "testvirtual.ml", line 1, characters 6-57: Error: Some type variables are unbound in this type: class virtual c : object method virtual f : 'a end The method f has type 'a where 'a is unbound
What is the ocaml type-checker really doing here when building the ocaml-suite? Rolling a dice?
The definition of Ctype.closed_class could be a bit too strict because this:
let f = List.length class c = object(self) method f = List.length end
yields an error:
File "../testf.ml", line 2, characters 6-51: Error: Some type variables are unbound in this type: class c : object method f : 'a list -> int end The method f has type 'a list -> int where 'a is unbound
But explicitly marking polymorphy:
let f = List.length class c = object(self) method f : 'a . 'a list -> int = List.length end
helps and "ocamlc -i" yields:
val f : 'a list -> int class c : object method f : 'a list -> int end
Why is the free variable 'a considered a problem for the method f but not for the function f?
Ever experienced strange things when using one of the printf-functions or something with a type constructor and a lot of type parameters ? Look at stdlib/printf.mli:
118 val sprintf : ('a, unit, string) format -> 'a 136 val ksprintf : (string -> 'a) -> ('b, unit, string, 'a) format4 -> 'b;; 151 val kprintf : (string -> 'a) -> ('b, unit, string, 'a) format4 -> 'b;;
If you look at the definitions in stdlib/printf.ml you will notice that it should read:
118 val sprintf : ('a, Buffer.t, string) format -> 'a 136 val ksprintf : (string -> 'a) -> ('b, Buffer.t, 'c) format -> 'b;; 151 val kprintf : (string -> 'a) -> ('b, Buffer.t, 'c) format -> 'b;;
But as usual no complaints from the compiler when matching the implementation printf.ml against the broken interface printf.mli.
The main reason for this is a glitch in Ctype.expand_abbrev_gen: When an abbrevation is found expand_abbrev_gen just yields the looked up type without considering the type parameters of the abbreviated type: after unification it could be that some of the parameters are no longer a type variable but are linked to a concrete type. These concrete types should be substituted into the just found type.
After (partially) fixing these issue in the compiler my own code shows the same mysterious behaviour that I attribute to a still broken Ocaml. Considering that it would take me about a day to convert most of my stuff to mlton or poly/ml and about two weeks to convert the MoreFun-preprocessor (only the Forth type checker could be a hard case), while I already spent 4 months trying to fix ocaml with no avail, I have to stop using Ocaml now. There are nice alternatives with sound and explicitly written definitions of the respective language; maybe I give Shen or Racket a try.
I suggest that you also think about dropping Ocaml. If you still insist on using Ocaml you can hire me; at least I know some of its problems and your money may cure my headaches concerning the use of a broken implementation.