Re: [Caml-list] ocaml considered dangerous

[Jacques Garrigue <garrigue@math.nagoya-u.ac.jp>]

Let me repost here the answer I sent to Jurgen on the developer’s list.
I wonder why he posted simultaneously to both lists.


First remark, rather than posting such a (broken) link, it would be better
to file a report in the bug tracking system at
	http://caml.inria.fr/mantis/

Second, I’ve read your post (fortunately going to  http://www.pfitzenmaier.de/ let
me access it), and this appears to be a misunderstanding of the meaning of type
annotations in OCaml.
Namely, while type annotations in signatures are universally quantified
(which is why ‘a list = forall ‘a. ‘a list is more general than int list, and your first
example is not accepted), type annotations in expressions are existentially
quantified, i.e. the variables may be instantiated, and as a result your second
example is accepted (int list ref is an instance of ‘a list ref).
Same thing in your third example: the annotation ‘a list -> ‘a just means that
there should be some type a such that get_sum has type a list -> a, and here
that type is int.

If you want annotations in expressions to be universally quantified, you must be
explicit:

 let get_sum : 'a. 'a list -> 'a = A.sum

This one requires get_sum to be polymorphic, and will report an error.

Of course changing line 28 in includecore.ml solves nothing, since this line is
correct from the beginning.

Your examples with polymorphic variants are again a misunderstanding of
how typing works. Namely, in OCaml subtyping is always explicit.
So in F1 you should write:
	let get_count :> [`A] list -> 'a = A.count
(Note that in some case you also need to give the original type of the expression
for subtyping to work properly. Here this is not needed because the target type is
simple enough)

For your frightening discoveries, the definition of ty0 is on line 499… maybe too close
to see.

Last, the current implementation of Printf relies heavily on Obj.magic, which means
that you cannot tell much about the typing by what you see inside the implementation.
To my best knowledge, the exported interface is type safe.
By the way, there is now an implementation of Printf that avoids most of the Obj.magic
by using GADTs. It should be merged soon.

Finally I would suggest not to post such a blog before you discuss the problems
you encountered with somebody (not necessarily the developers, just somebody
knowledgeable enough in OCaml) as this may confuse people in a useless way.
This would also have avoided you to part from OCaml for inexistent reasons...

Best regards,

Jacques Garrigue