Re: [Caml-list] ocaml considered dangerous

[Goswin von Brederlow <goswin-v-b@web.de>]

On Fri, Jan 17, 2014 at 01:43:21AM +0100, Nicolas Braud-Santoni wrote:
> Dear Jürgen,
> 
> First, for completeness' sake, the correct URL is
> http://www.pfitzenmaier.de/posts/ocaml-considered-dangerous.html
> 
> It seems that most of the points in this blog post boil down to your
> confusion regarding the signification of 'a in types.
> Consider the following:
> let x : 'a = 0;;
> val x : int = 0
> 
> whereas
> let x: 'a. 'a = 0;;
> Error: This definition has type int which is less general than 'a. 'a
> 
> In the first case, 'a is a unification variable, which the compiler may
> unify with int.
> In the second case, we quantify universally over 'a.
> 
> As such, I would say that your claims of unsoundness were rather hasty,
> especially given that you follow-up by advertising your services.
> Moreover, as Daniel Bünzli pointed out, problem reports are usually done
> on the bugtracker.
> 
> Kind regards,
> Nicolas

It should also be noted that he claims the compiler produces faulty
programms. But all his examples are about the compiler rejecting some
bit of code that he thinks should be accepted.

So his code, which the compiler currently accepts or he couldn't run
it, crashes and he blames the compiler because other code doesn't get
accepted. Does that make any sense?

Seems to me that the crashes are more likely caused by his tinkering
with the compiler trying to get code accepted that the compiler
currently rejects because they are (or could be) unsound. Punhcing
holes in the type system like that obviously can cause crashes as can
use of Obj.magic to work around the type system.

Dear Jürgen,

Your first half seems to be, as mentioned, about misunderstanding the
type system. You might want to read up on universal and existential
types and unification. I also recommend reading up on the value
restriction, which explains why you sometimes loose polymorphism
unless you lift arguments.

As for your "Frightening discoveries" in the second half of your post:
Ocaml inferes types. Some types are infered by how the function is
declared and some types are infered by how the function (or method) is
USED, esspecially within objects. In the full example the use of the
method lets the compiler infere the right type so everything works.
But when you simplify the example to the point where the use case
disapears that is no longer possible and the compiler tells you so.

This can be surprising and anoying at times but that is how it works.
It does not mean the compiler accepted something in the longer example
that was unsound.

MfG
	Goswin