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 EB07D7EE25 for ; Sun, 27 Oct 2013 16:26:03 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of gabriel.scherer@gmail.com) identity=pra; client-ip=209.85.214.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of gabriel.scherer@gmail.com designates 209.85.214.53 as permitted sender) identity=mailfrom; client-ip=209.85.214.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="gabriel.scherer@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-bk0-f53.google.com) identity=helo; client-ip=209.85.214.53; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="gabriel.scherer@gmail.com"; x-sender="postmaster@mail-bk0-f53.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjIEAC0vbVLRVdY1lGdsb2JhbABQCYM/VKwAihiIR4EUCBYOAQEBAQcLCwkSKoIlAQEEAScZARsSCwEDAQsGBQsDCg0hIQEBEQEFAQoSBhMSh2IBAwkGDZlPjFaDCoNzChknAwpkiQEBBQyMWYEugT4EB4QsA5YfgWuBL4shg0sYKYRSOw X-IPAS-Result: AjIEAC0vbVLRVdY1lGdsb2JhbABQCYM/VKwAihiIR4EUCBYOAQEBAQcLCwkSKoIlAQEEAScZARsSCwEDAQsGBQsDCg0hIQEBEQEFAQoSBhMSh2IBAwkGDZlPjFaDCoNzChknAwpkiQEBBQyMWYEugT4EB4QsA5YfgWuBL4shg0sYKYRSOw X-IronPort-AV: E=Sophos;i="4.93,580,1378850400"; d="scan'208";a="39017737" Received: from mail-bk0-f53.google.com ([209.85.214.53]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 27 Oct 2013 16:25:58 +0100 Received: by mail-bk0-f53.google.com with SMTP id d7so1392231bkh.40 for ; Sun, 27 Oct 2013 08:26:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc:content-type; bh=lejgXoDa+1ONsh6ukHWoZD5eARGPbq+ZpLT8T5FCxF4=; b=PHz4Ps5G7VlKcJs7Vsj9jRxHIY3oG3aIN5ygsZ1VH+9GuwBcL+rrYyOmY2sfxm8UQy ISB91cj/8SQoB91SWfhuUQoz/Gd/xK2LSAwvA0MEMMPSd0c6M/NWc+JPwUWn4oCK8xtV 6+q58m5uztEznnGK3C5Se9YGGMODrxNK8N81Szx36BuSvTpsjDdP7Ssa7tur2+11fz6u MvpVe8ICZNztbLFRUyk9nitZSuxcKvaCOXc+u+5CXZoPRwBTt6hdX5d2NvDDd83/NfYV 4x/Oo6UnFj6R3HozPEFfmGmN9qwkCYt+X8l7HhcYVKqkQtiSeJN2G8midZSUXjTa8IXH itRQ== X-Received: by 10.204.64.78 with SMTP id d14mr164661bki.40.1382887562383; Sun, 27 Oct 2013 08:26:02 -0700 (PDT) MIME-Version: 1.0 Received: by 10.204.122.72 with HTTP; Sun, 27 Oct 2013 08:25:22 -0700 (PDT) In-Reply-To: References: <97627FCD-30E1-45AD-A72B-CD423170C0AC@math.nagoya-u.ac.jp> <20131025082911.GB23798@voyager> <878uxhd62p.fsf@golf.niidar.ru> <526A7F33.6040203@mpi-sws.org> <66AB5484-8BFC-4A1C-ADAC-99C75716B054@mpi-sws.org> From: Gabriel Scherer Date: Sun, 27 Oct 2013 16:25:22 +0100 Message-ID: To: Yaron Minsky Cc: Andreas Rossberg , OCaML List Mailing Content-Type: multipart/alternative; boundary=001a11c396e0ebc4e704e9ba9941 Subject: Re: [Caml-list] Equality between abstract type definitions --001a11c396e0ebc4e704e9ba9941 Content-Type: text/plain; charset=ISO-8859-1 Today the only time where you see '_a is for variable that did not get generalized, and as a output of the type inference, never as input. But it would be consistent to extend their meaning to flexible variables anywhere, regardless of whether they'll get generalized later. Andreas' idea is to have '_a meaning "instantiate me with any suitable type that makes this expression type-check" (including a freshly generalized variable), and have 'a meaning instead "this type must remain a polymorphic variable". The interpretation for '_a corresponds to the meaning it has when printed by the type-checker today -- and the interpretation of 'a would behave as the (type a) construct does today, minus possibly the specific GADT interaction. (One minor difference being that, today, the type-checker is not too careful about respecting weak variable identity when printing them. The weak variables appearing in the two phrases I've shown have the same name '_a, when they in fact denote distinct flexible variables which occur in the same scope.) On Sun, Oct 27, 2013 at 3:43 PM, Yaron Minsky wrote: > But isn't this the exact opposite of Andreas' proposal? He was > proposing using '_a as a unification variable, which may very well be > generalized. It is exactly this use case for '_a that seems at odds > with Andreas' proposal. > > y > > On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer > wrote: > >> > Note how OCaml already uses '_a for a sort of flexible variable in its > >> > output. > >> Where? > > > > '_a is used for type variables that cannot be generalized. > > > > # let x = ref None;; > > val x : '_a option ref = {contents = None} > > # let id x = x in id id;; > > - : '_a -> '_a = > > > > > > > > On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky > > wrote: > >> > >> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg > > >> wrote: > >> > On Oct 25, 2013, at 22:32 , Yaron Minsky > wrote: > >> >> Changing the semantics of this will, I think, break a _lot_ of code. > >> > > >> > Interesting. Do you have specific examples in mind? > >> > >> I know that I've seen many examples come up in my code. One common > >> use is to partially specify a type. For example, if I wanted to > >> ignore a return value that is a Tcp.Server.t from Async, I would > >> probably write it like this: > >> > >> (ignore server : ('a,'b) Tcp.Server.t) > >> > >> without specifying the sometimes rather complicated details of those > >> types. Similarly, if I were to ignore a Map, I might write > >> > >> (ignore map : (int,string,'a) Map.t > >> > >> since it's not helpful here to specify the comparator type, which is > >> what goes into the third slot here. > >> > >> Nowadays, I would probably use an underscore in these cases rather > >> than an explicit type variable, but our codebase has plenty of old > >> examples of this kind of thing. If a change like the one you propose > >> is changed, I presume that _ would keep its current meeting, which > >> would address many use cases. > >> > >> Given the existence of such use-cases, I would hope that we could > >> avoid making the change in a way that would non-optionally break lots > >> of code. If people agree this change should be made, perhaps it > >> should be done in the mode of -strict-sequence. That change was added > >> as a flag, so users could take it at their own pace. > >> > >> >> For what it's worth, I suspect that most people who are surprised by > >> >> this are people who were trained on Standard ML. At Jane Street > we've > >> >> had a lot of people learn the language, and the complaints I've heard > >> >> about this feature are, I think, mostly from that group. > >> > > >> > Maybe, but it's not my impression that this is true for most people I > >> > see asking related questions here on the list or on SO. > >> > >> To be clear, my guess above is less than scientific. > >> > >> >> I also don't find Andreas suggestion particularly intuitive. I would > >> >> have guessed that (x: '_a) would constrain x to be a weakly > >> >> polymorphic value, which is at odds with the proposal. > >> > > >> > Now, _that_ is something I would only expect from programmers trained > on > >> > SML -- ancient SML'90 to be precise. ;) > >> > > >> > Note how OCaml already uses '_a for a sort of flexible variable in its > >> > output. > >> > >> Where? > >> > >> > /Andreas > >> > > >> > >> -- > >> Caml-list mailing list. Subscription management and archives: > >> https://sympa.inria.fr/sympa/arc/caml-list > >> Beginner's list: http://groups.yahoo.com/group/ocaml_beginners > >> Bug reports: http://caml.inria.fr/bin/caml-bugs > > > > > --001a11c396e0ebc4e704e9ba9941 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Today the only time where you see '_a is for vari= able that did not get generalized, and as a output of the type inference, n= ever as input. But it would be consistent to extend their meaning to flexib= le variables anywhere, regardless of whether they'll get generalized la= ter.

Andreas' idea is to have '_a meaning "instantia= te me with any suitable type that makes this expression type-check" (i= ncluding a freshly generalized variable), and have 'a meaning instead &= quot;this type must remain a polymorphic variable". The interpretation= for '_a corresponds to the meaning it has when printed by the type-che= cker today -- and the interpretation of 'a would behave as the (type a)= construct does today, minus possibly the specific GADT interaction.

(One minor difference being that, today, the type= -checker is not too careful about respecting weak variable identity when pr= inting them. The weak variables appearing in the two phrases I've shown= have the same name '_a, when they in fact denote distinct flexible var= iables which occur in the same scope.)


=


On Sun, Oct 2= 7, 2013 at 3:43 PM, Yaron Minsky <yminsky@janestreet.com> wrote:
But isn't this the exact opposite of And= reas' proposal? =A0He was
proposing using '_a as a unification variable, which may very well be generalized. =A0It is exactly this use case for '_a that seems at odds<= br> with Andreas' proposal.

y

On Sun, Oct 27, 2013 at 10:28 AM, Gabriel Scherer
<gabriel.scherer@gmail.com<= /a>> wrote:
>> > Note how OCaml already uses '_a for a sort of flexible va= riable in its
>> > output.
>> Where?
>
> '_a is used for type variables that cannot be generalized.
>
> # let x =3D ref None;;
> val x : '_a option ref =3D {contents =3D None}
> # let id x =3D x in id id;;
> - : '_a -> '_a =3D <fun>
>
>
>
> On Sun, Oct 27, 2013 at 1:56 PM, Yaron Minsky <yminsky@janestreet.com>
> wrote:
>>
>> On Sun, Oct 27, 2013 at 8:16 AM, Andreas Rossberg <rossberg@mpi-sws.org>
>> wrote:
>> > On Oct 25, 2013, at 22:32 , Yaron Minsky <yminsky@janestreet.com> wrote:
>> >> Changing the semantics of this will, I think, break a _lo= t_ of code.
>> >
>> > Interesting. Do you have specific examples in mind?
>>
>> I know that I've seen many examples come up in my code. =A0One= common
>> use is to partially specify a type. =A0For example, if I wanted to=
>> ignore a return value that is a Tcp.Server.t from Async, I would >> probably write it like this:
>>
>> =A0 =A0 (ignore server : ('a,'b) Tcp.Server.t)
>>
>> without specifying the sometimes rather complicated details of tho= se
>> types. =A0Similarly, if I were to ignore a Map, I might write
>>
>> =A0 =A0 (ignore map : (int,string,'a) Map.t
>>
>> since it's not helpful here to specify the comparator type, wh= ich is
>> what goes into the third slot here.
>>
>> Nowadays, I would probably use an underscore in these cases rather=
>> than an explicit type variable, but our codebase has plenty of old=
>> examples of this kind of thing. =A0If a change like the one you pr= opose
>> is changed, I presume that _ would keep its current meeting, which=
>> would address many use cases.
>>
>> Given the existence of such use-cases, I would hope that we could<= br> >> avoid making the change in a way that would non-optionally break l= ots
>> of code. =A0If people agree this change should be made, perhaps it=
>> should be done in the mode of -strict-sequence. =A0That change was= added
>> as a flag, so users could take it at their own pace.
>>
>> >> For what it's worth, I suspect that most people who a= re surprised by
>> >> this are people who were trained on Standard ML. =A0At Ja= ne Street we've
>> >> had a lot of people learn the language, and the complaint= s I've heard
>> >> about this feature are, I think, mostly from that group.<= br> >> >
>> > Maybe, but it's not my impression that this is true for m= ost people I
>> > see asking related questions here on the list or on SO.
>>
>> To be clear, my guess above is less than scientific.
>>
>> >> I also don't find Andreas suggestion particularly int= uitive. =A0I would
>> >> have guessed that (x: '_a) would constrain x to be a = weakly
>> >> polymorphic value, which is at odds with the proposal.
>> >
>> > Now, _that_ is something I would only expect from programmers= trained on
>> > SML -- ancient SML'90 to be precise. ;)
>> >
>> > Note how OCaml already uses '_a for a sort of flexible va= riable in its
>> > output.
>>
>> Where?
>>
>> > /Andreas
>> >
>>
>> --
>> Caml-list mailing list. =A0Subscription management and archives: >> https://sympa.inria.fr/sympa/arc/caml-list
>> Beginner's list: http://groups.yahoo.com/group/ocaml_beginner= s
>> Bug reports: http://caml.inria.fr/bin/caml-bugs
>
>

--001a11c396e0ebc4e704e9ba9941--