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 532B51E5 for ; Sat, 21 Apr 2018 09:04:12 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323899037" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Apr 2018 11:04:10 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id 5F63682446; Sat, 21 Apr 2018 11:04:10 +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 AE2EE8240C for ; Sat, 21 Apr 2018 11:04:03 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-ot0-f182.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AR1PNHhBpXYjztT8YbOrLUyQJP3N1i/DPJgcQr6Af?= =?us-ascii?q?oPdwSPv9r8bcNUDSrc9gkEXOFd2Cra4c0KyO6+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/Risxsl6JQvRatqwViz4LIfI2ZMfxzdb7fc9wHX2pMRsReVyJBDI2y?= =?us-ascii?q?bIUBEvQPMvpDoonhu1cDtweyCRWwCO7tzDJDm3/43bc90+QkCQzI2BIvH8gQv3?= =?us-ascii?q?TRrNT+KaUdXvqxzKnMyjXDd+5d1DD96YfSdhAhpfaMXaprfMrezEkgDQLFjlGK?= =?us-ascii?q?pYP5ODOV0/0Avm6G5ORuUuKvjnQoqwB3ojW3x8csjJPJhoMPxVze+yV52oA4Ls?= =?us-ascii?q?C7Rk5jedOpEpRduzuHO4doQs4uWWJltDggxrEbupO3Yi4Hw4k9yRHFcfyIaY2I?= =?us-ascii?q?7wrjVOmPJTd4g2poeLeliBaz9Uis0+r8VtWo3FpToCpJj9rBum4X2xzc7ciHTf?= =?us-ascii?q?R9/kO/1jqVyw/T7eRELVg1lardNZEh3qY9m5gcvEjZAyP6hkX7gLWVe0k64OSk?= =?us-ascii?q?9ufqbqv+qp+ZLYB0iwX+Mqo0msy4BOQ1KggPUHKf+eS4073j5Vb0QLpPjvIsk6?= =?us-ascii?q?nZtIrWKtgcpq68GwNVyJos6w6jDze619QVhWUII0hAeBKDloTpP1DOIOvkDfqk?= =?us-ascii?q?mFStkDJrx+jcMbH7A5XNKGLDkLb7crpn5U5c0ll78dcK3ZVRA7AHaNj6QEP2qZ?= =?us-ascii?q?SMFBg8Og2y6+zuEtl6y8UQQzTcLLWeNfbwvEWF4/NnEuCIYIgN8GLsIvwh4ObG?= =?us-ascii?q?gnowmFtbdq6si8hEIEukF+hrdh3KKUHnhc0MRCJT5lJnHb7azWaaWDsWXE6cGq?= =?us-ascii?q?c15zU1EoWjVN6RSYWkgbjH1yC+TMQPOjJ2T2uUGHKtTL2qHu8WYXvLcMBkmz0A?= =?us-ascii?q?E7OmTt15jEz8hErB07Nia9Hs1GgYuJbkjoYn4uTSkVQ16WQxAZ3NiSeCSGZ7mm?= =?us-ascii?q?5OTDgzjvhy?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0DNAAAv/dpaf7ZSfUpbhBg9eigKg2CDb?= =?us-ascii?q?ZENgXQCgQ2HUIstFIFkCyWERAKCPgcZBwEEMBgBAgEBAQEBAQEBARMBAQkLCwg?= =?us-ascii?q?mJQyCNSQBgkkBAgECIwQZARsdAQMMBgULDQICJgICIgERAQUBHAYTCIRuAQMVD?= =?us-ascii?q?5l5PIsFgWkWBQEXgnAFg1IKGSYNVFeCJgIGEneGfYITg2U1gwYLA4FHgxiCVAK?= =?us-ascii?q?HSoVbik4IhVyIZIFvil+JNoZnDwMegQQcggozGggbFTsxghIJhXOBPokVPjABk?= =?us-ascii?q?AABAQ?= X-IPAS-Result: =?us-ascii?q?A0DNAAAv/dpaf7ZSfUpbhBg9eigKg2CDbZENgXQCgQ2HUIs?= =?us-ascii?q?tFIFkCyWERAKCPgcZBwEEMBgBAgEBAQEBAQEBARMBAQkLCwgmJQyCNSQBgkkBA?= =?us-ascii?q?gECIwQZARsdAQMMBgULDQICJgICIgERAQUBHAYTCIRuAQMVD5l5PIsFgWkWBQE?= =?us-ascii?q?XgnAFg1IKGSYNVFeCJgIGEneGfYITg2U1gwYLA4FHgxiCVAKHSoVbik4IhVyIZ?= =?us-ascii?q?IFvil+JNoZnDwMegQQcggozGggbFTsxghIJhXOBPokVPjABkAABAQ?= X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="262849928" Received: from mail-ot0-f182.google.com ([74.125.82.182]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Apr 2018 11:04:02 +0200 Received: by mail-ot0-f182.google.com with SMTP id h8-v6so8431216otb.2 for ; Sat, 21 Apr 2018 02:04:02 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=20161025; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=0RR5k3ueAjkOV9lzhWJT0NTTc6OkYFMhDJRn57C1Utg=; b=ev39qOX/o+DYPqdeEGupBPEwF1IlZiMOHTL99D0F+9b2rPDkgN+QpyvFZqnjybh56q sFthOrYvmF1WVl5KpS2qXadpxpS/1vBYctbpBqorg+DBJjNEFFZhpucBJGtjB3q3QUWD kRMZXvLHzqHg+EPtuodt/WjlkTbVj14CWjsj6hZco1PNkuvTiff9O6IReNxs2c8xXegS q2jHNb/5LzB/xbOqHEM6yJI2nRv2KczVwJ7nKPCmp+VQYFZa5FEGO0HsftRv5OoavcWa vadx3MkVcEQhFrL3f9Ws/+RXD1hCbQO1UrN7O3Sx1/6ZSyeilo/BuMqGtLmRuDAi0/lU /pcA== X-Google-DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=1e100.net; s=20161025; h=x-gm-message-state:mime-version:in-reply-to:references:from:date :message-id:subject:to:cc; bh=0RR5k3ueAjkOV9lzhWJT0NTTc6OkYFMhDJRn57C1Utg=; b=nDagjwOsMHyunskNi3NsH3ZpsZCUNBJNqMIVYE8KB//WDvYUfUgbtpNxgdiAzqh5DF nRVeGYhH6iB12LxTpOVMEjcMNRjUHNSYjn9HnfXKUvyiOA/ng/cyWRFx0JlSruhSTKD/ gvxdvIqmgFA1YvWluReLvrWvRpGWxQHgIzv3zgDjq4NxtBMGQgaaCdK22hqFTeYDXcdd NhV6ST8UCcWYsb+pFG5QWIK9VQv/aAIALgabl8NTbID3bKf3op/WMAq1G1RrH1Y5pH5T v5GQxEgkdhrgbemrpa8cmVb4hRsObhITPynRYfR42K8OjJBbrbFIwUfc3jVnJZGs95Ja L9Bg== X-Gm-Message-State: ALQs6tAc3sv2wIYTYxsJAJOp4Yi0n5QVootIK5OPayfevHmjhtA6b+Pr wqYMh0r5Wzz9tTH/4Gdfzfacc5CkNoPC9YjCRCRJiQ== X-Google-Smtp-Source: AIpwx4+hW/CBNkrcsztijhkAjI4DeuKaGDKHojYP7YbnP3nhM/HoZdXSu4Ewi4Tn1U5K0nC12IJ6AP+QCxof+uVVXMA= X-Received: by 2002:a9d:55cc:: with SMTP id z12-v6mr9109721oti.378.1524301440919; Sat, 21 Apr 2018 02:04:00 -0700 (PDT) MIME-Version: 1.0 Received: by 10.74.91.132 with HTTP; Sat, 21 Apr 2018 02:04:00 -0700 (PDT) In-Reply-To: <2a9e479f-4ce0-fdf3-d0b7-501398691720@bardou.fr> References: <2a9e479f-4ce0-fdf3-d0b7-501398691720@bardou.fr> From: Jeremy Yallop Date: Sat, 21 Apr 2018 10:04:00 +0100 Message-ID: To: Romain Bardou Cc: Caml List Content-Type: text/plain; charset="UTF-8" Subject: Re: [Caml-list] Why doesn't relaxed value restriction apply here? Reply-To: Jeremy Yallop X-Loop: caml-list@inria.fr X-Sequence: 16836 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 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). 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. -- 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