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 127737EE25 for ; Fri, 25 Oct 2013 15:06:24 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of wojciech.meyer@gmail.com) identity=pra; client-ip=209.85.214.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="wojciech.meyer@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of wojciech.meyer@gmail.com designates 209.85.214.176 as permitted sender) identity=mailfrom; client-ip=209.85.214.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="wojciech.meyer@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-ob0-f176.google.com) identity=helo; client-ip=209.85.214.176; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="wojciech.meyer@gmail.com"; x-sender="postmaster@mail-ob0-f176.google.com"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AjwEAFFsalLRVdawlGdsb2JhbABZgz9Uq2qKGIhHgRoIFg4BAQEBBwsLCRIqgiUBAQQBQAEbDwMLAQMBCwYFCw0NISIBEQEFAQoSBhMSCYdZAQMJBg2bBYxWgwqELQoZJwMKZIkBAQUMjX2BRgQHhCwDlCqDYIEvjmwYKYJmgWw7 X-IPAS-Result: AjwEAFFsalLRVdawlGdsb2JhbABZgz9Uq2qKGIhHgRoIFg4BAQEBBwsLCRIqgiUBAQQBQAEbDwMLAQMBCwYFCw0NISIBEQEFAQoSBhMSCYdZAQMJBg2bBYxWgwqELQoZJwMKZIkBAQUMjX2BRgQHhCwDlCqDYIEvjmwYKYJmgWw7 X-IronPort-AV: E=Sophos;i="4.93,570,1378850400"; d="scan'208";a="38779551" Received: from mail-ob0-f176.google.com ([209.85.214.176]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/RC4-SHA; 25 Oct 2013 15:06:24 +0200 Received: by mail-ob0-f176.google.com with SMTP id uy5so862222obc.21 for ; Fri, 25 Oct 2013 06:06:21 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20120113; h=mime-version:in-reply-to:references:date:message-id:subject:from:to :cc:content-type; bh=hbAFTBs4waRBdkpogK+3Anv3qu+ZoJTegCttpS/AJ94=; b=gnTCxpQaCrUZvh+tGpAO60HOGlHXDdXAghoGF+wWYfkFlb8CceUrHklrwpMX8dWt74 BhmwhkimmWnyy8v0gMVzFywBK+AROTFNMkRnuooIcNZ9977VvZ1ZeQvd+PBdCSxW0wfK aeK4CoByk69Huv+OIO4CgBzX4DpnB7XM25w0mvomu6f5+U/kL/sNIK+Yc7mdZU1NkTks IMB95ni+BPdLUNrLkVwg7hWllwh9BnAfi8b0nbDI/VegGHdzzbDjVpSA+dswmzTJRmzb YcR8yXdDI8qgkbv9unEcH3TLMECC9C8766xdysZ+wmT3OdD7PtK0xIM65oR5JOpJFDu5 wEhA== MIME-Version: 1.0 X-Received: by 10.60.131.232 with SMTP id op8mr319378oeb.75.1382706381668; Fri, 25 Oct 2013 06:06:21 -0700 (PDT) Received: by 10.182.125.34 with HTTP; Fri, 25 Oct 2013 06:06:21 -0700 (PDT) In-Reply-To: <526A6693.9010302@frisch.fr> References: <526A37ED.6080901@frisch.fr> <526A55AE.8080208@inria.fr> <526A6693.9010302@frisch.fr> Date: Fri, 25 Oct 2013 14:06:21 +0100 Message-ID: From: Wojciech Meyer To: Alain Frisch Cc: Didier Remy , Caml List Content-Type: multipart/alternative; boundary=047d7b47266ab55bc504e9906a32 Subject: Re: [Caml-list] Robust left to right flow for record disambiguation --047d7b47266ab55bc504e9906a32 Content-Type: text/plain; charset=ISO-8859-1 Not being here a type system's expert so excuse if I did a serious mistake or I said something trivial. Wouldn't make sense to perform the unification of the arguments (GADT constructors and function arguments), in both ways? First propagate the type information left right and then right left, and then finally unify the results? Alternatively, we could also add check such that if the left right type checking fails (being not principal), then we try also right to left. On Fri, Oct 25, 2013 at 1:39 PM, Alain Frisch wrote: > On 10/25/2013 01:27 PM, Didier Remy wrote: > >> I don't think specifying the information flow between left and right >> (always-left-to-right, always-right-to-left, or depending-on-examples) is >> a >> good design. This leads to non predictable type inference and less robust >> programs : refactoring a function by just changing the order of >> parameters >> (and consistently changing the order of arguments in all uses of the >> function) may break existing programs and also require new annotations. >> > > This is already the case, except for people using -principal. I know it > is recommended to use this option (at least once in a while), but I doubt > many users actually do it. (And FWIW, -principal is so slow on our code > base that we cannot actually use it in practice -- this is probably related > to the way we use object types.) > > As a user, I think I'm willing to pay the price of risking having to add a > few annotations on the next refactoring if this makes a very common idiom > more practical. > > > > Also, such a biased will encourage people to write parameters of functions >> in an order that works well for the uses they have in mind. I think it >> odd >> that type inference would have such an influence in choosing the order of >> function parameters. >> > > If the ordering used for the (specified) information flow were drawn from > the actual call site, labeled arguments would be a good solution. > > > Alain > > > -- > 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 > --047d7b47266ab55bc504e9906a32 Content-Type: text/html; charset=ISO-8859-1 Content-Transfer-Encoding: quoted-printable
Not being here a type system's expert so excuse i= f I did a serious mistake or I said something trivial.

Wouldn&= #39;t make sense to perform the unification of the arguments (GADT construc= tors and function arguments), in both ways? First propagate the type inform= ation left right and then right left, and then finally unify the results? A= lternatively, we could also add check such that if the left right type chec= king fails (being not principal), then we try also right to left.



On = Fri, Oct 25, 2013 at 1:39 PM, Alain Frisch <alain@frisch.fr> w= rote:
On 10/25/2013 01:27 PM, Di= dier Remy wrote:
I don't think specifying the information flow between left and right
(always-left-to-right, always-right-to-left, or depending-on-examples) is a=
good design. This leads to non predictable type inference and less robust programs =A0: refactoring a function by just changing the order of paramete= rs
(and consistently changing the order of arguments in all uses of the
function) may break existing programs and also require new annotations.

This is already the case, except for people using -principal. =A0I know it = is recommended to use this option (at least once in a while), but I doubt m= any users actually do it. =A0(And FWIW, -principal is so slow on our code b= ase that we cannot actually use it in practice -- this is probably related = to the way we use object types.)

As a user, I think I'm willing to pay the price of risking having to ad= d a few annotations on the next refactoring if this makes a very common idi= om more practical.



Also, such a biased will encourage people to write parameters of functions<= br> in an order that works well for the uses they have in mind. =A0I think it o= dd
that type inference would have such an influence in choosing the order of function parameters.

If the ordering used for the (specified) information flow were drawn from t= he actual call site, labeled arguments would be a good solution.


Alain

--047d7b47266ab55bc504e9906a32--