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 661467EE25 for ; Sun, 27 Oct 2013 16:41:44 +0100 (CET) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of yminsky@janestreet.com) identity=pra; client-ip=38.105.200.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of yminsky@janestreet.com designates 38.105.200.229 as permitted sender) identity=mailfrom; client-ip=38.105.200.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="yminsky@janestreet.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@tot-dmz-mxout1.janestreet.com) identity=helo; client-ip=38.105.200.229; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="yminsky@janestreet.com"; x-sender="postmaster@tot-dmz-mxout1.janestreet.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AsoBANszbVImacjlnGdsb2JhbABQCYM/VKwAkl+BFB4OAQEBAQEGFgk8giUBAQQBJxkBASwLAQ8LCw0NISEBEgEFAQoSBhMSDIdXAwkGAwIImVKLDYRTAQWENgMKiWUGjGWBLoFCB4QsliKBa4EviyGDSxgphG0 X-IPAS-Result: AsoBANszbVImacjlnGdsb2JhbABQCYM/VKwAkl+BFB4OAQEBAQEGFgk8giUBAQQBJxkBASwLAQ8LCw0NISEBEgEFAQoSBhMSDIdXAwkGAwIImVKLDYRTAQWENgMKiWUGjGWBLoFCB4QsliKBa4EviyGDSxgphG0 X-IronPort-AV: E=Sophos;i="4.93,580,1378850400"; d="scan'208";a="39018822" Received: from mx5.janestreet.com (HELO tot-dmz-mxout1.janestreet.com) ([38.105.200.229]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-SHA; 27 Oct 2013 16:41:38 +0100 Received: from tot-oib-smtp1.delacy.com ([172.27.22.15] helo=tot-smtp) by tot-dmz-mxout1.janestreet.com with esmtp (Exim 4.76) (envelope-from ) id 1VaSTG-0000I6-1P for caml-list@inria.fr; Sun, 27 Oct 2013 11:41:42 -0400 Received: from tot-dmz-mxgoog1.delacy.com ([172.27.224.14] helo=mxgoog2.janestreet.com) by tot-smtp with esmtps (TLSv1:AES256-SHA:256) (Exim 4.72) (envelope-from ) id 1VaSTG-0002kQ-0O for caml-list@inria.fr; Sun, 27 Oct 2013 11:41:42 -0400 Received: from mail-ee0-f46.google.com ([74.125.83.46]) by mxgoog2.janestreet.com with esmtp (Exim 4.76) (envelope-from ) id 1VaSTF-00081O-Rz for caml-list@inria.fr; Sun, 27 Oct 2013 11:41:41 -0400 Received: by mail-ee0-f46.google.com with SMTP id c1so2936312eek.19 for ; Sun, 27 Oct 2013 08:41:41 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=7dxx2RhaAM1TIwD8gpl+NS0lZVfMFgtquB6B7NqAzUo=; b=g5lm/zXECH5BafMcYGBkqpdIUi2/aAutqA2LSKuYb+ujFHmPzsRQzFtltR6G9L8omE 5j1ighK30amDPnsAL9zptmrTFxCqTWF7UcFdthJmb2lxqa6pTXvYAlUyk9kRNz4t1cdH dizX4UDSW9YWu29bUH/2e/5QjiLICq7IVmbF4= X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20130820; h=x-gm-message-state:mime-version:in-reply-to:references:date :message-id:subject:from:to:cc:content-type; bh=7dxx2RhaAM1TIwD8gpl+NS0lZVfMFgtquB6B7NqAzUo=; b=iXsUy1diPwMMzupTXxNIWf4f/zT0hYDiWdryMgnB62nm95fAGBlcTuiGsvdCnUFaca nFOk/+E0ZCq0/MIvyhuPX2H4itJhM7isd+LoBGXjzW2yC0/Je3HzyhsdbPWBhzZ281qY H93Rn0scT6+6Gb4tyEWQPIxIQw0YmcNzszIY3doXSP1Tnfl70xL0kqj2CGPOvE1RE/SD 7Vsf1w/8otR6t3awFkxeX7pu1Gdm4s/jKrTmTw3vXlGr2PQuuEZbxRPz/0ac6j/wuPEy dmD3gN27URVDilNpTFdflHglULXaHKn/zdYp8sLf8XmOgBUGVmNlsUSAnjDJ5+/5phfu s60g== X-Gm-Message-State: ALoCoQkxYecvpW8DrvIs6+joaQWxu9m3NqQywZKUIwDnf6xicSOI9oJWlCWONWhsZOkU5pRlv5JrpfS/82YO1hrJA+yPqsVyGISeNY9gzoXY9hQrAmegc6u3NV2VutxutRZIddNXOHFJqwBn2D6CVejf3JACNJvSqw== X-Received: by 10.14.174.131 with SMTP id x3mr17303779eel.25.1382888501220; Sun, 27 Oct 2013 08:41:41 -0700 (PDT) MIME-Version: 1.0 X-Received: by 10.14.174.131 with SMTP id x3mr17303771eel.25.1382888501090; Sun, 27 Oct 2013 08:41:41 -0700 (PDT) Received: by 10.223.180.138 with HTTP; Sun, 27 Oct 2013 08:41:40 -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> Date: Sun, 27 Oct 2013 11:41:40 -0400 Message-ID: From: Yaron Minsky To: Gabriel Scherer Cc: Andreas Rossberg , OCaML List Mailing Content-Type: text/plain; charset=ISO-8859-1 Subject: Re: [Caml-list] Equality between abstract type definitions I trust you that it's a consistent interpretation, but it still strikes me as surprising, and I suspect it would be so for new users. >From a user's perspective, you only see '_a now when there a weakly polymorphic type variable is inferred. Andreas' proposal is that as an annotation, this should imply a unification variable, i.e., a constraint on what can be inferred for that type. I don't know why those both count as "flexible variables" (not surprising, since I had not heard of them before this conversation), but I'm not sure it matters much. The new situation seems not a lot clearer than the old, merely moving around the confusion from one syntax to another. All told, following Roberto's observation, I suspect there isn't enough of a win here to justify changing the meaning of old syntax. y On Sun, Oct 27, 2013 at 11:25 AM, Gabriel Scherer wrote: > 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 >> > >> > > >