RE: [Caml-list] ocaml considered dangerous

["Jon Harrop" <jon@ffconsultancy.com>]

> 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.

Just curious: is that a drop-in replacement?

Cheers,
Jon.

-----Original Message-----
From: caml-list-request@inria.fr [mailto:caml-list-request@inria.fr] On Behalf Of Jacques Garrigue
Sent: 17 January 2014 02:39
To: OCaML List Mailing
Subject: Re: [Caml-list] ocaml considered dangerous

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

--
Caml-list mailing list.  Subscription management and archives:
https://sympa.inria.fr/sympa/arc/caml-list
Beginner's list: http://groups.yahoo.com/group/ocaml_beginners
Bug reports: http://caml.inria.fr/bin/caml-bugs=