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 ESMTP id 7F1CA1E5 for ; Sat, 21 Apr 2018 09:15:32 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323899939" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Apr 2018 11:15:30 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 3367982447; Sat, 21 Apr 2018 11:15:30 +0200 (CEST) Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id DEB668240C for ; Sat, 21 Apr 2018 11:15:01 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=romain@bardou.fr; spf=Pass smtp.mailfrom=romain@bardou.fr; spf=None smtp.helo=postmaster@10.mo173.mail-out.ovh.net IronPort-PHdr: =?us-ascii?q?9a23=3A/S5dpxB1ZcRQMwkljlGJUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPT7o8bcNUDSrc9gkEXOFd2Cra4c0KyO6+jJYi8p2d65qncMcZhBBVcuqP?= =?us-ascii?q?49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6?= =?us-ascii?q?JvjvGo7Vks+7y/2+94fcbglUijexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfO?= =?us-ascii?q?pWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnM?= =?us-ascii?q?VhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iS?= =?us-ascii?q?cHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRttfWTJPAo28?= =?us-ascii?q?bIUBAeQOMulaoIbhqFUDtge+CAu2Ce/z1jNFiH370Ksn2OohCwHG2wkgEsoSvn?= =?us-ascii?q?TTqdX6LqYSUeaox6TV1zrDde5Z2TDg6IPVdR0hu/aMXbdqfsrQz0kiDBjKgU+K?= =?us-ascii?q?qYP4ODOVy/4Bs2aB7+d5U++klmApqwZ0oje1x8csjJHEhoMTylDe9CV22pw5Jd?= =?us-ascii?q?OiSEN9fNWqE4NQujmVOoZ3WM8uXn1ktSYgxrAEtpO3ZjUGxZskyhLHb/GLb5KE?= =?us-ascii?q?7g/+WOqNOzt1inFodKiiixqs8UWtzPD3WNOu31ZQtCVFl8HBtnAT2BzX7ciKUu?= =?us-ascii?q?Zx8lu71TaK0ADf9+NJLE4umareMZEhw7owmoMUsUTeAi/6gkL2jLGWdkk+/Oin?= =?us-ascii?q?9fjnbq3npp+aKYB0lhnzP6svl8ClHOg0LggDU3KZ9OmzzrHv4EL0TbZSgv0ziK?= =?us-ascii?q?bZsZTaJcoBpq6+Bg9Yypwj6xG6Dzi80dQYm2IKI0lfdxKdkofpPEzOLOr2Dfel?= =?us-ascii?q?m1isiitkx+jaPr39BZXANmTMn63kfbZ58kJczAszzctD559PEbEAIPfzWlfru9?= =?us-ascii?q?DCDx85NRa0w+f9B9ln2IMeQzHHPqjMEq7IvFqZrtMmJ+2LfMdBqT/5L/89z/Hr?= =?us-ascii?q?hH4931QaeP/684EQbSWCGfFvIkPRS3P2jtAcWTMQuQ83TerCglSYXTlOIXioCf?= =?us-ascii?q?FvrgonAZ6rWN+QDrumh6aMiWLiRsUPNzJ2T2uUGHKtTL2qHvIFaSacOMhky2VW?= =?us-ascii?q?X7G7R4g8kx+05lajl+hXa9HM8yhdjqrNkcBv7rSKxxs77zBzEoKTyTPVFjwmri?= =?us-ascii?q?YzXzYzmZtHjwl9x1OEi/cq2qQeENsKuKgPVw47Mdvb0vA8DM7yHATMYoXRRQ?= =?us-ascii?q?=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0A3AQC3ANtah5RKaS5bg0mBDAN3KINql?= =?us-ascii?q?kUpgQ+TEYFkCyWERAIIgj0ZBwEEMxUBAgEBAQEBAQEBARMBAQEIDQkIKCMMgjU?= =?us-ascii?q?kAYJIAQEBAQEBASMEEUEFCwsYAgImAgJXBg0GAgEBhQMMC6VAgWkzhFiDcIIug?= =?us-ascii?q?QmJEIEygjM1gwYLA4FHGIMAglQCh0qFW4pOCHCEbIheBl2BEoVbhQSJNoZ2gSU?= =?us-ascii?q?ygXQzGggfETuCQwmCJYEDAQiEAIkWbQGQAAEB?= X-IPAS-Result: =?us-ascii?q?A0A3AQC3ANtah5RKaS5bg0mBDAN3KINqlkUpgQ+TEYFkCyW?= =?us-ascii?q?ERAIIgj0ZBwEEMxUBAgEBAQEBAQEBARMBAQEIDQkIKCMMgjUkAYJIAQEBAQEBA?= =?us-ascii?q?SMEEUEFCwsYAgImAgJXBg0GAgEBhQMMC6VAgWkzhFiDcIIugQmJEIEygjM1gwY?= =?us-ascii?q?LA4FHGIMAglQCh0qFW4pOCHCEbIheBl2BEoVbhQSJNoZ2gSUygXQzGggfETuCQ?= =?us-ascii?q?wmCJYEDAQiEAIkWbQGQAAEB?= X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="262850475" Received: from 10.mo173.mail-out.ovh.net ([46.105.74.148]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 21 Apr 2018 11:15:01 +0200 Received: from player770.ha.ovh.net (unknown [10.109.120.81]) by mo173.mail-out.ovh.net (Postfix) with ESMTP id 18C6EBD6BB for ; Sat, 21 Apr 2018 11:15:01 +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 D3DD2C0080; Sat, 21 Apr 2018 11:14:59 +0200 (CEST) To: Jeremy Yallop Cc: Caml List References: <2a9e479f-4ce0-fdf3-d0b7-501398691720@bardou.fr> From: Romain Bardou Message-ID: Date: Sat, 21 Apr 2018 11:14:59 +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: 77687093582317855 X-VR-SPAMSTATE: OK X-VR-SPAMSCORE: -100 X-VR-SPAMCAUSE: gggruggvucftvghtrhhoucdtuddrgedtgedrjeelgddugecutefuodetggdotefrodftvfcurfhrohhfihhlvgemucfqggfjpdevjffgvefmvefgnecuuegrihhlohhuthemuceftddtnecusecvtfgvtghiphhivghnthhsucdlqddutddtmd 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: 16837 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: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. > 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. Thanks a lot for your quick answer and your example :) 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