From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id 7A8897EC6E for ; Fri, 17 Jan 2014 10:01:49 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.47 as permitted sender) identity=mailfrom; client-ip=209.85.214.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-bk0-f47.google.com) identity=helo; client-ip=209.85.214.47; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f47.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsECAJFf2FLRVdYvlWdsb2JhbABZDoM1VqgokmmBBwgWDgEBAQEHDQkJEiqCJQEBAQMBJxkBGxILAQMBCwYFCw0NISIBEQEFAQoSBhMICoddAQMJCA2dDoxcgwmSFAoZJwMKZIRyEQEFDIx4gUgzB4Q4BJghgTGLLoNLGCmEGkA7 X-IPAS-Result: AsECAJFf2FLRVdYvlWdsb2JhbABZDoM1VqgokmmBBwgWDgEBAQEHDQkJEiqCJQEBAQMBJxkBGxILAQMBCwYFCw0NISIBEQEFAQoSBhMICoddAQMJCA2dDoxcgwmSFAoZJwMKZIRyEQEFDIx4gUgzB4Q4BJghgTGLLoNLGCmEGkA7 X-IronPort-AV: E=Sophos;i="4.95,670,1384297200"; d="scan'208";a="45136620" Received: from mail-bk0-f47.google.com ([209.85.214.47]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 17 Jan 2014 10:01:48 +0100 Received: by mail-bk0-f47.google.com with SMTP id d7so410504bkh.34 for ; Fri, 17 Jan 2014 01:01:48 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type:content-transfer-encoding; bh=k8htI8rxgt57nn8DyfM/1aDkLOXEDBNYxV7cz0z4knI=; b=vlYO3ahVHeZaqcikHEpdzk5Y1Z7JU/P5EEckCzJWcWm/+b/vLghR6OdI5GO6XBMuAg ku6CeRqPg8bMWLCA7d/MaHbN4t5KXyACSD9fUD/CzbK9NnvHXMTSxsq55l21Mf0GvMN8 G1+Rv6r7TZQd7vp4jxkYgrWYpYP5ZBTrKMOmTVLmYo9OEZOIJ9GiDQwa6DfmMD8mXwd+ 4hHsqP5SrJ0XWbDJ2plI28oup5BG5UIbr8P0IfCa8K5Fmwq8C+0e8Ddwdcym71qXfWDu sIcAGmiNG0mOua/pG0B0sW1h5KxjBXoc87ray+zYCNsy8Mdj+EvnjeM7FA7qyVYl2Oci IRnA== X-Received: by 10.205.38.4 with SMTP id tg4mr432853bkb.55.1389949307810; Fri, 17 Jan 2014 01:01:47 -0800 (PST) MIME-Version: 1.0 Received: by 10.205.45.5 with HTTP; Fri, 17 Jan 2014 01:01:07 -0800 (PST) In-Reply-To: <0290505B-A21A-4A05-A1C9-4C5F765DFEB5@math.nagoya-u.ac.jp> References: <2112632769.281907.1389913202532.open-xchange@communicator.strato.de> <0290505B-A21A-4A05-A1C9-4C5F765DFEB5@math.nagoya-u.ac.jp> From: Gabriel Scherer Date: Fri, 17 Jan 2014 10:01:07 +0100 Message-ID: To: Jacques Garrigue Cc: OCaML List Mailing Content-Type: text/plain; charset=windows-1252 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] ocaml considered dangerous > After some investigations it turned out that the Ocaml compiler shows a q= uestionable 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 wrote: > Let me repost here the answer I sent to Jurgen on the developer=92s 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=92ve read your post (fortunately going to http://www.pfitzenma= ier.de/ let > me access it), and this appears to be a misunderstanding of the meaning o= f type > annotations in OCaml. > Namely, while type annotations in signatures are universally quantified > (which is why =91a list =3D forall =91a. =91a list is more general than i= nt list, and your first > example is not accepted), type annotations in expressions are existential= ly > quantified, i.e. the variables may be instantiated, and as a result your = second > example is accepted (int list ref is an instance of =91a list ref). > Same thing in your third example: the annotation =91a list -> =91a just m= eans that > there should be some type a such that get_sum has type a list -> a, and h= ere > 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 =3D 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 l= ine 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 =3D A.count > (Note that in some case you also need to give the original type of the ex= pression > for subtyping to work properly. Here this is not needed because the targe= t type is > simple enough) > > For your frightening discoveries, the definition of ty0 is on line 499=85= maybe too close > to see. > > Last, the current implementation of Printf relies heavily on Obj.magic, w= hich means > that you cannot tell much about the typing by what you see inside the imp= lementation. > 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 pr= oblems > you encountered with somebody (not necessarily the developers, just someb= ody > knowledgeable enough in OCaml) as this may confuse people in a useless wa= y. > This would also have avoided you to part from OCaml for inexistent reason= s... > > 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