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 E307E1E5 for ; Sat, 21 Apr 2018 09:45:27 +0000 (UTC) X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323901671" Received: from sympa.inria.fr ([193.51.193.213]) by mail2-relais-roc.national.inria.fr with ESMTP; 21 Apr 2018 11:45:25 +0200 Received: by sympa.inria.fr (Postfix, from userid 20132) id C960F82447; Sat, 21 Apr 2018 11:45:25 +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 A188A8240C for ; Sat, 21 Apr 2018 11:45:19 +0200 (CEST) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=yallop@gmail.com; spf=Pass smtp.mailfrom=yallop@gmail.com; spf=None smtp.helo=postmaster@mail-ot0-f174.google.com IronPort-PHdr: =?us-ascii?q?9a23=3AMqQz1hzW1FTi+A7XCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?1OweIJqq85mqBkHD//Il1AaPAd2Araocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze+/94HdbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiS?= =?us-ascii?q?cIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyeKfhwcb7Hfd4CR2VBUMZfWSJCDI2h?= =?us-ascii?q?cYUAE/EMPfpEo4Tnu1cCsQeyCAuqCejyyjFInHj23agi3uolDw7GxhIvH9cOsX?= =?us-ascii?q?/Jrtr6LqMSUeSyzKnQ0D7OaPNX1i356IjMdRAhueqBXb11ccXLyEkvExnJgUmX?= =?us-ascii?q?qYzgJj6Y0PkGvWac7+plT+2vimgnphlwojip3Mcsi5PGipgbylDe8yhy3YU7Jc?= =?us-ascii?q?WgRUN5btOoCoZcuz+aOodsQc4uXXtktDs4x7AJv5OwYTIEx449xxHFbvyKa4iI?= =?us-ascii?q?7QznVOaWOTp4gWhqeLO7hxqr9kig1vHwWtC60FpXrCdIncPAtn8K1xzU5ciHTu?= =?us-ascii?q?Vy8l291jaI0gDf8uBEIUYqmqrHM5MswLE9moAOvUjdHiL6gkb7gLGMekk5+OWl?= =?us-ascii?q?5PzrYrD8qZ+dM490hBv+MqMrmsGnAeU3KAwOX2yc+eSkz7Dj8kj5T69Ljv0yiK?= =?us-ascii?q?XWrJfaJcEDqq6jHwBVypoj6wq4Dzq+zNsXh3wHLFZcdBKDjojpIE3OLevjDfa/?= =?us-ascii?q?hlSsiC1ky+rHPr3nGJXNL2LMnK3vfbZnuAZgz18JytVW5pQcILgbLPXuEhvrs9?= =?us-ascii?q?nRDxkROQWuz+H6TttngNAwQ2WKV42UKq7XoBe57+YrJPHEMJ4cvDL6M9Aq4vfv?= =?us-ascii?q?iTkynlpLLvrh5ocedH3tRqcuGE6ee3e5x45ZST5b7Dp7d/TjjRi5aRAWYn+zW6?= =?us-ascii?q?wm4TRiUdCpCI7CQsamh7nThX7nTK0TXXhPDxW3KVmtb5+NAq5eZyebI8snmTsB?= =?us-ascii?q?B+D4Ft0RkCq2vQq/8IJJa+rZ/ipC68Dm3dlxourPzVQ8rGMoScua1G6JQid/mW?= =?us-ascii?q?ZaHzI=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CABwDGBttahq5SfUpbhFV6KAqDYINtk?= =?us-ascii?q?Q2BdAJzGodQiy4UgWQLJYRGAoI+BxkHAQQyFgECAQEBAQEBAQEBEwEBAQgLCwg?= =?us-ascii?q?oIwyCNSQBgkgBAQEBAQEBIwQZARsdAQMMBgULDQICJgICIgERAQUBHAYThHYBA?= =?us-ascii?q?w0ID5oLPIsFgWkWBQEXgnAFg1IKGSYNVFeCJgIGEneGfYITgQ+CVjWDBgsDgUe?= =?us-ascii?q?DGIJUAodKhVuKTgiFXIhkgW+KX4k2hmgPAx6BBCMHgXwzGggbFTsxghIJgiWDT?= =?us-ascii?q?oE+iRU+MAGQIQEB?= X-IPAS-Result: =?us-ascii?q?A0CABwDGBttahq5SfUpbhFV6KAqDYINtkQ2BdAJzGodQiy4?= =?us-ascii?q?UgWQLJYRGAoI+BxkHAQQyFgECAQEBAQEBAQEBEwEBAQgLCwgoIwyCNSQBgkgBA?= =?us-ascii?q?QEBAQEBIwQZARsdAQMMBgULDQICJgICIgERAQUBHAYThHYBAw0ID5oLPIsFgWk?= =?us-ascii?q?WBQEXgnAFg1IKGSYNVFeCJgIGEneGfYITgQ+CVjWDBgsDgUeDGIJUAodKhVuKT?= =?us-ascii?q?giFXIhkgW+KX4k2hmgPAx6BBCMHgXwzGggbFTsxghIJgiWDToE+iRU+MAGQIQE?= =?us-ascii?q?B?= X-IronPort-AV: E=Sophos;i="5.49,306,1520895600"; d="scan'208";a="323901633" Received: from mail-ot0-f174.google.com ([74.125.82.174]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 21 Apr 2018 11:45:18 +0200 Received: by mail-ot0-f174.google.com with SMTP id m22-v6so12189900otf.8 for ; Sat, 21 Apr 2018 02:45:18 -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=Ntv8Dib4+wbkJp7l2SFNMxfLCCqoT+bGfsrTh4hjDtM=; b=dv+dhUT9PrtR23Li62x9c7t572zhc2Ey5lW2yZ+x/QAsrzH3Q4VErj8J697p/VivHM 0lq2JqXQtOPpwLgiYmTAb5WjaJ3z9PRJLuq6YUTFau3x0OqYg1Mt8B6+EWyPXGc2G3+t PJbbuEShtytcWr/KNvzbgWxx+vyDIqZYQ3PKRlWHuPbzSlXVqEr9XhAu49U+/9MUAKoz U286sw5sr0g+fw57eIOZaQiKcyHkWxHcQJrp3A1KrMOXTRh7LEoGQWR1bt7BGhhUYlj1 pcMC0JDdZnsEegw53oqHtJanXEdI4+NkvGhu/T6AKC11arwUJMZuefzBbv5vwblP2x7Z LX6g== 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=Ntv8Dib4+wbkJp7l2SFNMxfLCCqoT+bGfsrTh4hjDtM=; b=oizrh0HLlqY31Epxed0+sEtNpO1G6dOWfAWClqf/lnLAHeXw7Ckkrd75IBruSVPn4e sZMJ5Kt2I4lvA/vnMs4NYkqD7xyNxWGnIZhbhyF/GcNvY7Oy4n2pyEDYGbrUu8a8Wc8h uwieBUV8gVFI7Luh79Xz3x+lnNxcdH/hjN7AQX175k7dFPxDQvTf5m9k7L2nA6A7MFnV SRc4sDQXUgPiIa2bPPMTeWyA0upCihMXfM6aJYNgvSxzG7Wk0rq/Oc3ZTvnpXlVLcKJM ljds2liYWGAw60ZkXISM5NoPB2yxiGeK1ffp7bm3gbrazVHEZ0I6ZlejUzAu6XBka3l6 nawQ== X-Gm-Message-State: ALQs6tCGTUXdyGGYrwRuaG/oF5oTevJhq1uUdQkzvm/MM0a3zkS+qyLi FdNPaD9LQPtnrpPOecmCwchR9waV8Y5f9nebO2s= X-Google-Smtp-Source: AIpwx4+DP9kvMEWqYq+w4fsy85e2UTk5dcEgUBO8d0bW2Rt8LlAJpZ/2iU9HJfSWbXIuZXNfqnS+C75XPu03EW4vh7k= X-Received: by 2002:a9d:21f4:: with SMTP id s107-v6mr8355007otb.237.1524303916933; Sat, 21 Apr 2018 02:45:16 -0700 (PDT) MIME-Version: 1.0 Received: by 10.74.91.132 with HTTP; Sat, 21 Apr 2018 02:45:16 -0700 (PDT) In-Reply-To: References: <2a9e479f-4ce0-fdf3-d0b7-501398691720@bardou.fr> From: Jeremy Yallop Date: Sat, 21 Apr 2018 10:45:16 +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: 16838 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 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. >> 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!) -- 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