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 A9D6A7EE25 for ; Fri, 25 Oct 2013 11:59:35 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.217.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: PermError (mail2-smtp-roc.national.inria.fr: cannot correctly interpret sender authenticity information from domain of ivg@ieee.org) identity=mailfrom; client-ip=209.85.217.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; 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-lb0-f181.google.com) identity=helo; client-ip=209.85.217.181; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-lb0-f181.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AugCAINAalLRVdm1lWdsb2JhbABZhya7NoEgFg4BAQEBBw0JCRIqgiUBAQQBIwRSEAsaAgUhAgIPAQQgAQUBIhOIAQYEAZphjAOSToEpjiQHgmqBQgOJOY5RkBtBhFQ X-IPAS-Result: AugCAINAalLRVdm1lWdsb2JhbABZhya7NoEgFg4BAQEBBw0JCRIqgiUBAQQBIwRSEAsaAgUhAgIPAQQgAQUBIhOIAQYEAZphjAOSToEpjiQHgmqBQgOJOY5RkBtBhFQ X-IronPort-AV: E=Sophos;i="4.93,569,1378850400"; d="scan'208";a="38753125" Received: from mail-lb0-f181.google.com ([209.85.217.181]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 11:59:27 +0200 Received: by mail-lb0-f181.google.com with SMTP id x18so528028lbi.26 for ; Fri, 25 Oct 2013 02:59:34 -0700 (PDT) X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:from:to:cc:subject:references:date:in-reply-to :message-id:user-agent:mime-version:content-type :content-transfer-encoding; bh=ld+mUPIutC1m7QCkVH/9SZeqnEuqrq5gqB+z6GbmxiA=; b=F7TWuMPfhHIfcI72sOwixF/x3eeWKkmcnpLBgMvAaipTlH/NIa5R62n1XTVImzPaw7 v0dWhFazdALbqWzwtZ5b2XyxXrvxeGekko6AhK3ewNItSSWqSBOV6yNi+zAGgIMZkW83 k8Zqi8O3ndQApQDuo1RuCEFYw60I8bmijtt2H7MbDVPg0Bv9CPHAGY8Zg8cGYX6Yu//6 qcxpCODSDSk7qJFbv/emO1sxzEbH8gMq1WzYMXGgfU3cZPLhnd1jfB2K2IHAlSwEbkZf u0L9vcW6u3vQ8Ljge9cEZg7pve/DJpueqGJb3T1IWy1+UXBo6gfXs1Hq4B7Q40rhg+hm WVZg== X-Gm-Message-State: ALoCoQkGL7KOeWyxzfR5o3LPqiqy4aO01+bxeqW4IU0hJqUobv+Y9i6NF79nQokf/LTgGtYaTsEz X-Received: by 10.112.133.5 with SMTP id oy5mr273970lbb.64.1382695174606; Fri, 25 Oct 2013 02:59:34 -0700 (PDT) Received: from golf.niidar.ru.niidar.ru ([109.188.127.202]) by mx.google.com with ESMTPSA id u18sm2000651lbp.4.2013.10.25.02.59.33 for (version=TLSv1.1 cipher=RC4-SHA bits=128/128); Fri, 25 Oct 2013 02:59:34 -0700 (PDT) From: Ivan Gotovchits To: Roberto Di Cosmo Cc: Andreas Rossberg , Jacques Garrigue , OCaML List Mailing References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> Date: Fri, 25 Oct 2013 13:59:26 +0400 In-Reply-To: <20131025082911.GB23798@voyager> (Roberto Di Cosmo's message of "Fri, 25 Oct 2013 10:29:11 +0200") Message-ID: <878uxhd62p.fsf@golf.niidar.ru> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.2 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=utf-8 Content-Transfer-Encoding: quoted-printable Subject: Re: [Caml-list] Equality between abstract type definitions Roberto Di Cosmo writes: > > I am curious to know why you consider this a pitfall: if it is > not what people expect, it is probably because nobody explained > their meaning to them properly, and I am quite interested in > understanding how to explain this better. > I think that people expect that an expression: ``` let a : int =3D b=20 ``` is a declaration that value `a` has type int (Just like C'ish=20 `int a =3D b;`). But, indeed, it should be understood as a type constraint. Thus the following, will be readily accepted by the type checker (because we =C2=ABconstrain=C2=BB a to be anything): ``` let a : 'a =3D 12 ``` The root of misunderstanding, I think, lies in that the same syntax is used for type annotations and value specifications. Consider the following example: ``` module T : sig val sum: 'a -> 'a -> 'a end =3D struct let sum: 'a -> 'a -> 'a =3D=20 fun x y -> x + y end ``` It looks like that the value sum has the same type in the module specification and in the module implementation. So if compiler accepts definition, it should accept that it conforms to the specification.=20 Indeed, it's rather intuitional - this types do look the same! So, I think, that it should be clarified by someone, who knows OCaml and English much better than me, what is the difference between this two cases. And it would be great if it will be described in the manual, too.=20 --=20 (__)=20 (oo)=20 /------\/=20 / | ||=20=20=20 * /\---/\=20 ~~ ~~=20=20=20 ...."Have you mooed today?"...