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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 5F9697EE99 for ; Mon, 20 Jan 2014 11:07:31 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=pra; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of goswin-v-b@web.de) identity=mailfrom; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="goswin-v-b@web.de"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mout.web.de) identity=helo; client-ip=212.227.15.14; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="goswin-v-b@web.de"; x-sender="postmaster@mout.web.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ArcCAGP03FLU4w8OnGdsb2JhbABZg0O2RIVPgQwWDgEBAQEBBg0JCRQogiUBAQEEMgFWCxgJJQ8FKIgkARgJvRgfhiWPBhaEIgSYIYYxEo8E X-IPAS-Result: ArcCAGP03FLU4w8OnGdsb2JhbABZg0O2RIVPgQwWDgEBAQEBBg0JCRQogiUBAQEEMgFWCxgJJQ8FKIgkARgJvRgfhiWPBhaEIgSYIYYxEo8E X-IronPort-AV: E=Sophos;i="4.95,689,1384297200"; d="scan'208";a="53980571" Received: from mout.web.de ([212.227.15.14]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES128-SHA; 20 Jan 2014 11:07:31 +0100 Received: from frosties.localnet ([37.49.32.119]) by smtp.web.de (mrweb001) with ESMTPSA (Nemesis) id 0MaJc8-1VlKUz2qlc-00Jt7C for ; Mon, 20 Jan 2014 11:07:29 +0100 Received: from mrvn by frosties.localnet with local (Exim 4.80) (envelope-from ) id 1W5BlR-0007Gc-6F for caml-list@inria.fr; Mon, 20 Jan 2014 11:07:29 +0100 Date: Mon, 20 Jan 2014 11:07:29 +0100 From: Goswin von Brederlow To: caml-list@inria.fr Message-ID: <20140120100729.GG26447@frosties> References: <2112632769.281907.1389913202532.open-xchange@communicator.strato.de> <52D87CA9.4070500@braud-santoni.eu> MIME-Version: 1.0 Content-Type: text/plain; charset=iso-8859-1 Content-Disposition: inline Content-Transfer-Encoding: 8bit In-Reply-To: <52D87CA9.4070500@braud-santoni.eu> User-Agent: Mutt/1.5.21 (2010-09-15) X-Provags-ID: V03:K0:WzQwkah5kH2vVSxNy8VZch4MM9+BcWFtuj1+aMVXQQQZ1oPL/qh UcKAY7pB4cYp4uvB/HpsJfCCunVorB0igitbrsY+gnyF2VixKO6vZo/xuxDAB70pD+OdUoP 11pIfX6xjzw/96aZPGmROZh7ZD4o+fVcs7NCh4XyxB6GdVkBzR5nDD935xRDkDiVYhP6+jz FIQ9c1AV4JF4xbR0ivQwA== Subject: Re: [Caml-list] ocaml considered dangerous 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