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 6275A7EE25 for ; Fri, 25 Oct 2013 14:45:56 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of jonathan.protzenko@gmail.com) identity=pra; client-ip=74.125.82.43; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="jonathan.protzenko@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of jonathan.protzenko@gmail.com designates 74.125.82.43 as permitted sender) identity=mailfrom; client-ip=74.125.82.43; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="jonathan.protzenko@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-wg0-f43.google.com) identity=helo; client-ip=74.125.82.43; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="jonathan.protzenko@gmail.com"; x-sender="postmaster@mail-wg0-f43.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApQDAKhmalJKfVIrlGdsb2JhbABZgma/doEiFg4BAQEBBwsLCRIqgiUBAQUnGQEbHAEBAwwGBQsNCRYPCQMCAQIBEREBBQEcBgEMAQcBAYdwAQMPAQSbIoxWgwqELQoZJw1kiQEBBQyPRweELAOYCpAbQYRT X-IPAS-Result: ApQDAKhmalJKfVIrlGdsb2JhbABZgma/doEiFg4BAQEBBwsLCRIqgiUBAQUnGQEbHAEBAwwGBQsNCRYPCQMCAQIBEREBBQEcBgEMAQcBAYdwAQMPAQSbIoxWgwqELQoZJw1kiQEBBQyPRweELAOYCpAbQYRT X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="31868603" Received: from mail-wg0-f43.google.com ([74.125.82.43]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 14:45:55 +0200 Received: by mail-wg0-f43.google.com with SMTP id b13so3677821wgh.34 for ; Fri, 25 Oct 2013 05:45:55 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=message-id:date:from:user-agent:mime-version:to:cc:subject :references:in-reply-to:content-type:content-transfer-encoding; bh=LYrisJj1MaKY6sL3lGC/XC8rKcjuznd6MySH3X/69PM=; b=sd45OT6wsGync6mCfIN1qNWGZSUNCaqJXX+O0/kucUHSmk46dgw9fVSW2BOHSCyGi9 kWGi91HvBMLyow/v553faCRsKKoe1wpFagbwUWnvxNgvo/sn0IdVpXjccLvtDK3KSviX tM8I2rXjytBNHcYKQt32vA6rU20QyWcAZE9/G/8gX8qyyPZ9a/GVBPZ/0Dw1bAk+Gw6o dqOTmTIfZgEwB/eEDYsbf+jK1jTh9+xz4XEOHkhH+HGW4uPRrdAmFTvQ+Kg0dTSNbhrW L8KMOd/CDbMwJnp7s1iN1iK2F5bSPsydAy5IZnlPSsEwa0rUdpCjxv6ptNEyUBBZDSJw omSw== X-Received: by 10.180.93.166 with SMTP id cv6mr2340982wib.37.1382705155468; Fri, 25 Oct 2013 05:45:55 -0700 (PDT) Received: from ?IPv6:2001:660:3013:3:f6ce:46ff:fe2d:a9ae? ([2001:660:3013:3:f6ce:46ff:fe2d:a9ae]) by mx.google.com with ESMTPSA id ft19sm5789234wic.5.2013.10.25.05.45.54 for (version=TLSv1 cipher=ECDHE-RSA-RC4-SHA bits=128/128); Fri, 25 Oct 2013 05:45:54 -0700 (PDT) Message-ID: <526A6800.9020501@gmail.com> Date: Fri, 25 Oct 2013 14:45:52 +0200 From: Jonathan Protzenko User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:27.0) Gecko/20100101 Thunderbird/27.0a1 MIME-Version: 1.0 To: Roberto Di Cosmo , Ivan Gotovchits CC: Andreas Rossberg , Jacques Garrigue , OCaML List Mailing References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <878uxhd62p.fsf@golf.niidar.ru> <20131025123517.GA21960@voyager> In-Reply-To: <20131025123517.GA21960@voyager> X-Enigmail-Version: 1.6 Content-Type: text/plain; charset=ISO-8859-1 Content-Transfer-Encoding: 7bit Subject: Re: [Caml-list] Equality between abstract type definitions On 10/25/2013 02:35 PM, Roberto Di Cosmo wrote: > Thanks Ivan, > the potential confusion between type annotations > in the code and type specifications in module interfaces > is a very good point. > > Writing > > let f : 'a -> 'a = fun x -> x+1 > > will just boil down to defining > > val f : int -> int = > > On the other side, declaring > > val f : 'a -> 'a > > in a module signature actually *requires* the implementation > to be at least as generic as 'a -> 'a, so a definition > let f = fun x -> x+1 in the body will not work. 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 = # let f : 'a -> 'a = fun x -> x + 1;; val f : 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