Re: [Caml-list] ocaml considered dangerous

[Gabriel Scherer <gabriel.scherer@gmail.com>]

> After some investigations it turned out that the Ocaml compiler shows a questionable understanding of type checking.

After immediate reading it turned out that the post author shows a
complete misunderstanding of the type system he's talking about.

It's great that he felt motivated to look at the internals of the
admittedly-complex type checker and experiment with language
extensions. The problem is the arrogance in assuming other people are
wrong.

For anyone interested in understanding the core of the type checker,
there is a very nice presentation by Oleg at
  http://okmij.org/ftp/ML/generalization.html
(It does not cover the issues that are treated here, rather the simple
ML fragment on let-generalization, but it's a start and it helps
understand the way mutation is used in the implementation, which
indeed makes it not a piece of cake.)


On Fri, Jan 17, 2014 at 3:38 AM, Jacques Garrigue
<garrigue@math.nagoya-u.ac.jp> wrote:
> 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