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 778577EE25 for ; Fri, 25 Oct 2013 15:20:58 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rdicosmo@gmail.com) identity=pra; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rdicosmo@gmail.com designates 74.125.82.181 as permitted sender) identity=mailfrom; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="rdicosmo@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-we0-f181.google.com) identity=helo; client-ip=74.125.82.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rdicosmo@gmail.com"; x-sender="postmaster@mail-we0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ah8EANdvalJKfVK1lGdsb2JhbABZvRyGYhYOAQEBAQcLCwkSKoIlAQEEAScTBgE4AQMBCwEFBRgJJQ8FIAEFAQEhiAgDCQYEAZsTj2CEUCcNiWUBBQwKkmOBDQOYCZAcQYFkgm8 X-IPAS-Result: Ah8EANdvalJKfVK1lGdsb2JhbABZvRyGYhYOAQEBAQcLCwkSKoIlAQEEAScTBgE4AQMBCwEFBRgJJQ8FIAEFAQEhiAgDCQYEAZsTj2CEUCcNiWUBBQwKkmOBDQOYCZAcQYFkgm8 X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="38781930" Received: from mail-we0-f181.google.com ([74.125.82.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 15:20:37 +0200 Received: by mail-we0-f181.google.com with SMTP id t60so3695619wes.26 for ; Fri, 25 Oct 2013 06:20:35 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=sender:date:from:to:cc:subject:message-id:references:mime-version :content-type:content-disposition:in-reply-to:user-agent; bh=92bNdTs46ZuZMSCHVm6ESkpHovdDYwdKcO1BSMPo2tg=; b=Ud6UyStUFKOFlVg2kiCy/VS//xR0U3+AZ4TS4OMSg/Dfx2VWFUoLfCLMWC1mGptdjd Bma5KhRJ5y2jKK/rDadX4/7OUAL+VobX0JMo3dU5BftvMGx71VGZRr1DtwMefVw31kLA dma5LN4Vwt5CVDO5oH4tEWLPIGjTue8Kqguco+njhpvEESPFRjeg4AvIuSEm8mjqeZ2O nKGkyqQIvAX/FTjXV5boq/fQqY9to5YOAVn8htCoV9kG0UsSL+wE2wthGqvwjiqnbSmm rV4lKNUVE9Us1fvZlelzoKe1g1b3+O9iPlqRLehoHHO09Z9cBDB6k/tGx0v1RLMd5Uut qIUg== X-Received: by 10.194.206.5 with SMTP id lk5mr7372274wjc.46.1382707235486; Fri, 25 Oct 2013 06:20:35 -0700 (PDT) Received: from voyager (bny92-3-81-56-44-163.fbx.proxad.net. [81.56.44.163]) by mx.google.com with ESMTPSA id y20sm6100224wib.0.2013.10.25.06.20.33 for (version=TLSv1.2 cipher=RC4-SHA bits=128/128); Fri, 25 Oct 2013 06:20:34 -0700 (PDT) Sender: Roberto Di Cosmo Received: from dicosmo by voyager with local (Exim 4.80) (envelope-from ) id 1VZhJY-00052P-OP; Fri, 25 Oct 2013 15:20:32 +0200 Date: Fri, 25 Oct 2013 15:20:32 +0200 From: Roberto Di Cosmo To: Jonathan Protzenko Cc: Ivan Gotovchits , Andreas Rossberg , Jacques Garrigue , OCaML List Mailing Message-ID: <20131025132032.GB12951@voyager> References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <878uxhd62p.fsf@golf.niidar.ru> <20131025123517.GA21960@voyager> <526A6800.9020501@gmail.com> MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Content-Disposition: inline In-Reply-To: <526A6800.9020501@gmail.com> User-Agent: Mutt/1.5.20 (2009-06-14) Subject: Re: [Caml-list] Equality between abstract type definitions Hi Jonathan, I beg to disagree On Fri, Oct 25, 2013 at 02:45:52PM +0200, Jonathan Protzenko wrote: > You should also remember that the top-level, which is what most > beginners use, also favors the confusion. > > # let f x = x;; > val f : 'a -> 'a = OCaml is telling you: hey, your code is so generic that I can give it the type 'a -> 'a, you got a polymorphic function! > # let f : 'a -> 'a = fun x -> x + 1;; > val f : int -> int = > Here you are telling OCaml: look, I'd like to see f as having type 'a -> 'a, what do you think? And OCaml tells you: sorry sir, the best I can give you is int -> int > What OCaml is actually telling you is: "this function has type 'a -> 'a, > but if you write 'a -> 'a yourself, I'm going to give it a totally > different meaning". > > ~ jonathan The point on which I agree is that if we leave these annotations in the code, they may end up being read as specifications by whomever looks at the sources alone, and this may lead to confusion. But to spot such issues we do not need to change the syntax and semantics of type annotations, it would be enough to have yet another warning that informs us that the type annotations have been instanciated... something like # let f : 'a -> 'a = fun x -> x + 1;; _______ Warning 66: the user provided type constraint is too general: variable 'a has been instanciated to type int val f : int -> int = -- Roberto P.S.: I will not feed the troll any longer though, time to get back to work :-)