From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Received: from mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by c5ff346549e7 (Postfix) with ESMTPS id A57C51E5 for ; Sat, 21 Apr 2018 11:35:01 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323908982" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Apr 2018 13:34:59 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id ABC8782445; Sat, 21 Apr 2018 13:34:59 +0200 (CEST) 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 66E728240C for ; Sat, 21 Apr 2018 13:34:35 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=romain@bardou.fr; spf=Pass smtp.mailfrom=romain@bardou.fr; spf=None smtp.helo=postmaster@7.mo179.mail-out.ovh.net IronPort-PHdr: =?us-ascii?q?9a23=3AGYSjFh3+U5J6RPTgsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0RKvad9pjvdHbS+e9qxAeQG9mDsLQc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q99pHPbQhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb5Sqw5VDqg4qplURPklC?= =?us-ascii?q?gKPCM9/GzXlsB8iaRWqw+jqRNi2Y7ZeJybOuRwfq3dft0US2ROUclTWCNdDY2x?= =?us-ascii?q?dJcPAugbMOpEs4XwqVkDoB2jDgesHuPvzTpIi2fq06091uQuCwDG3Ao9FN8Tqn?= =?us-ascii?q?vUtsj6NKAPUeuoy6TI1zLDb/ZM1jf87ojFaQsuruuWXb1tdsrR1FMjFw3fjliJ?= =?us-ascii?q?r4HuIj2b1uMIs2eB7upgU/qii28hqwFrozig3N0giofTho8T11vK9j15zZ46KN?= =?us-ascii?q?C5UkJ3fMKoHZtKuyybKod6WMcvTm5wtCs+1rEKo4O3cDUWxJg9yRPSaOaLf5WW?= =?us-ascii?q?7h/jUuuaPC12i2h/eL2lgha/6UigxfP4VsmzyFtHrDBJktzLtnwQ1RHe7tKLSv?= =?us-ascii?q?5n8Ueg3TaDzgfT6vxYIUwukqrbNZ4hzqQ2lpUNrUTPBi72mEPog6+Kbkgp9eml?= =?us-ascii?q?5/76brn6ppKQLY55hhzkPqkqlcGzGeE4PRIPX2if9+S8zrrj/UjhTbVQif02l7?= =?us-ascii?q?PWsJHcJckAvaG2GRVV3Zsk6xaiFTum3s4YkWEdLF1ZYBKHk5TpO1bWLf/kF/i/?= =?us-ascii?q?hlCsnC5vx/DHJb3hHo7ALmPDkbfkZbZy8VRQyAs1zdBF5pJbEKsNIPzpWhy5iN?= =?us-ascii?q?uNBRY8N0mwwv37INR7zIIXH2yVUYGDN6aHi1iN7+Mpa8OFfoMSpX6pMf8g7v/o?= =?us-ascii?q?pXUwg1MaYO+nx81EOziDAv16LhDBMjLXidAbHDJX5lNvHtyvs0WLVHtoX1j3Wq?= =?us-ascii?q?s94j8hD4f/VNXJT5qhh6HH0j3pR8QKNFADMUiFFDLTT6vBQ+0FMXvAKMZ7njsZ?= =?us-ascii?q?E7a7Gdd4iEOe8TTiwr8iFdL6vy0VsZW5iooqoejUzE5jszl9DsDY1HyRCWZqni?= =?us-ascii?q?UOSiNkhK0=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CMBAClINtah149aS5bhFUDdyiDapZFC?= =?us-ascii?q?CF1GoMtj2WBZAslhEYCCII9GQcBBDMVAQIBAQEBAQEBAQETAQEBCA0JCCgjDII?= =?us-ascii?q?1DAyCVQEBAQEBAQEjBBFRCxgCAiYCAlcTBgIBAYUDDAulTIFpM4RYg3CCLoEJi?= =?us-ascii?q?RCBDyMMgic1gwYLA4FHGIMAgVIjXwKHSoVbik4IcIRsiF4GXYEShVuFBIk2hne?= =?us-ascii?q?BJTKBdDMaCB8RO4JDCYIlhQyJFm0BkCEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CMBAClINtah149aS5bhFUDdyiDapZFCCF1GoMtj2WBZAs?= =?us-ascii?q?lhEYCCII9GQcBBDMVAQIBAQEBAQEBAQETAQEBCA0JCCgjDII1DAyCVQEBAQEBA?= =?us-ascii?q?QEjBBFRCxgCAiYCAlcTBgIBAYUDDAulTIFpM4RYg3CCLoEJiRCBDyMMgic1gwY?= =?us-ascii?q?LA4FHGIMAgVIjXwKHSoVbik4IcIRsiF4GXYEShVuFBIk2hneBJTKBdDMaCB8RO?= =?us-ascii?q?4JDCYIlhQyJFm0BkCEBAQ?= X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323908948" Received: from 7.mo179.mail-out.ovh.net ([46.105.61.94]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 21 Apr 2018 13:34:34 +0200 Received: from player770.ha.ovh.net (unknown [10.109.105.38]) by mo179.mail-out.ovh.net (Postfix) with ESMTP id 33D23B9C1A for ; Sat, 21 Apr 2018 13:34:34 +0200 (CEST) Received: from [192.168.1.15] (LFbn-1-6077-125.w90-110.abo.wanadoo.fr [90.110.38.125]) (Authenticated sender: romain@bardou.fr) by player770.ha.ovh.net (Postfix) with ESMTPSA id 04C0AC0081 for ; Sat, 21 Apr 2018 13:34:33 +0200 (CEST) To: caml-list@inria.fr References: <2a9e479f-4ce0-fdf3-d0b7-501398691720@bardou.fr> From: Romain Bardou Message-ID: Date: Sat, 21 Apr 2018 13:34:34 +0200 User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:52.0) Gecko/20100101 Thunderbird/52.7.0 MIME-Version: 1.0 In-Reply-To: Content-Type: text/plain; charset=utf-8; format=flowed Content-Language: en-US Content-Transfer-Encoding: 7bit X-Ovh-Tracer-Id: 2434758552088299807 X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: 50 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrgedtgedrjeelgdegfecutefuodetggdotefrodftvfcurfhrohhfihhlvgemucfqggfjpdevjffgvefmvefgnecuuegrihhlohhuthemuceftddtnecuogetfeejfedqtdegucdlhedtmd X-Validation-by: romain@bardou.fr Subject: Re: [Caml-list] Why doesn't relaxed value restriction apply here? Reply-To: Romain Bardou X-Loop: caml-list@inria.fr X-Sequence: 16839 Errors-to: caml-list-owner@inria.fr Precedence: list Precedence: bulk Sender: caml-list-request@inria.fr X-no-archive: yes List-Id: List-Archive: List-Help: List-Owner: List-Post: List-Subscribe: List-Unsubscribe: On 04/21/2018 11:45 AM, Jeremy Yallop wrote: > On 21 April 2018 at 10:14, Romain Bardou wrote: >> On 04/21/2018 11:04 AM, Jeremy Yallop wrote: >>> >>> On 21 April 2018 at 09:41, Romain Bardou wrote: >>>> >>>> According to the manual >>>> (http://caml.inria.fr/pub/docs/manual-ocaml/polymorphism.html) and to the >>>> paper "Relaxing the Value Restriction" >>>> >>>> (http://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf), >>>> the relaxed value restriction allows to generalize type variables which >>>> only >>>> appear in covariant positions. >>>> >>>> The following code : >>>> >>>> let f = let _ = ref 0 in fun f -> f [] >>>> >>>> returns the following in the toplevel: >>>> >>>> val f : ('_a list -> '_b) -> '_b = >>>> >>>> In this type, '_a only appears in covariant position. So, why is it not >>>> generalized? >>> >>> >>> I think the current implementation only generalizes variables that >>> only occur in *strictly* positive positions -- that is, that do not >>> appear to the left of any arrow. In your example, "'a" occurs in a >>> positive position (to the left of an even number of arrows) that is >>> not strictly positive (to the left of zero arrows). >> >> >> Interesting. I wonder what the reason is behind this choice: is it about >> soundness, or about simplicity. Your example below seems to indicate that >> this is not about soundness as one can hide the depth of a type variable >> using an abstract type. > > I think it's about principality. Since type variables in > contravariant positions are not generalized, the following definition > of 'h' receives a non-polymorphic type: > > let h = (fun x -> x) (fun _ -> ()) > val h : '_a -> unit > > and so a program that uses 'h' with some arbitrary argument type is allowed > > let m = h () > > but a program that use 'h' at multiple types is rejected: > > let p = (h print_int, h print_float) > > However, 'h' could also be given the less general type ('b -> unit) -> > unit, in which the type variable only appears in covariant positions. > If this type variable were generalized then 'p' would be allowed, but > 'm' would be rejected: there's no longer a best type for 'h' that can > be determined solely from its definition. The restriction to strictly > positive positions avoids this situation. I see, it makes sense. >>> This choice can lead to some slightly surprising situations, where >>> exposing valid type equalities can cause previously-valid programs to >>> be rejected. For example, the following program, which is based on >>> your example, is accepted: >>> >>> module M : >>> sig >>> type (+'a,'b) t >>> val g : unit -> ('a,'b) t >>> end = >>> struct >>> type (+'a,'b) t = ('a list -> 'b) -> 'b >>> let g () = let _ = ref 0 in fun f -> f [] >>> end;; >>> >>> let f = M.g () in ((f : (int, unit) M.t), (f : (float, unit) M.t));; >>> >>> but if the signature for 'M' is removed then the program is rejected. >> >> That's very interesting actually. > > There are a few such ways to break OCaml programs by exposing type > equalities: something similar happens with unboxed float records, and > with GADT exhaustiveness checking. (Details left as an exercise for > the reader!) Now that you mention it, I already encountered this issue several times with GADTs. It was rather annoying actually. Thanks again, this really helped Cheers, -- Romain Bardou -- 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