From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr 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 922437EC6E for ; Fri, 17 Jan 2014 03:39:54 +0100 (CET) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mailhost.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.5; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@mailhost.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgADAJFf2FKFBoIFdGdsb2JhbABZg0ODVLgTgSUOAQwVCDyCJgEBBCMEHAE3DgUGGgIYDgICVwYkh3KoL3aDYgKTOoR/EAeBKY0jOoJvNYEUiUmOXIExiy6IdA X-IPAS-Result: AgADAJFf2FKFBoIFdGdsb2JhbABZg0ODVLgTgSUOAQwVCDyCJgEBBCMEHAE3DgUGGgIYDgICVwYkh3KoL3aDYgKTOoR/EAeBKY0jOoJvNYEUiUmOXIExiy6IdA X-IronPort-AV: E=Sophos;i="4.95,670,1384297200"; d="scan'208";a="45103895" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail3-smtp-sop.national.inria.fr with ESMTP; 17 Jan 2014 03:39:51 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 4960C63EE for ; Fri, 17 Jan 2014 11:39:49 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id BA2B440E1; Fri, 17 Jan 2014 11:39:48 +0900 (JST) DomainKey-Signature: h=Received:Subject:Mime-Version:Content-Type:From:X-Priority:In-Reply-To:Date:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=; c=nofws; d=math.nagoya-u.ac.jp; q=; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 811EF3974; Fri, 17 Jan 2014 11:39:48 +0900 (JST) Mime-Version: 1.0 (Mac OS X Mail 7.1 \(1827\)) Content-Type: text/plain; charset=utf-8 From: Jacques Garrigue X-Priority: 3 In-Reply-To: <2112632769.281907.1389913202532.open-xchange@communicator.strato.de> Date: Fri, 17 Jan 2014 11:38:52 +0900 Content-Transfer-Encoding: quoted-printable Message-Id: <0290505B-A21A-4A05-A1C9-4C5F765DFEB5@math.nagoya-u.ac.jp> References: <2112632769.281907.1389913202532.open-xchange@communicator.strato.de> To: OCaML List Mailing X-Mailer: Apple Mail (2.1827) Subject: Re: [Caml-list] ocaml considered dangerous Let me repost here the answer I sent to Jurgen on the developer=E2=80=99s l= ist. 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=E2=80=99ve read your post (fortunately going to http://www.pfitz= enmaier.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 =E2=80=98a list =3D forall =E2=80=98a. =E2=80=98a list is mor= e 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 se= cond example is accepted (int list ref is an instance of =E2=80=98a list ref). Same thing in your third example: the annotation =E2=80=98a list -> =E2=80= =98a 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 mu= st 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 lin= e 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 expr= ession 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=E2= =80=A6 maybe too close to see. Last, the current implementation of Printf relies heavily on Obj.magic, whi= ch means that you cannot tell much about the typing by what you see inside the imple= mentation. To my best knowledge, the exported interface is type safe. By the way, there is now an implementation of Printf that avoids most of th= e Obj.magic by using GADTs. It should be merged soon. Finally I would suggest not to post such a blog before you discuss the prob= lems 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=