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 mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by sympa.inria.fr (Postfix) with ESMTPS id CC94F7FA5E for ; Fri, 12 May 2017 15:49:28 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=ivg@ieee.org; spf=Pass smtp.mailfrom=ivg@ieee.org; spf=None smtp.helo=postmaster@mail-yw0-f177.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of ivg@ieee.org) identity=pra; client-ip=209.85.161.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of ivg@ieee.org designates 209.85.161.177 as permitted sender) identity=mailfrom; client-ip=209.85.161.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="ivg@ieee.org"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-yw0-f177.google.com) identity=helo; client-ip=209.85.161.177; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="ivg@ieee.org"; x-sender="postmaster@mail-yw0-f177.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AdfUIeRyB194WlQzXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2+4WIJqq85mqBkHD//Il1AaPBtSHraocw8Pt8InYEVQa5piAtH1QOLdtbDQizf?= =?us-ascii?q?ssogo7HcSeAlf6JvO5JwYzHcBFSUM3tyrjaRsdF8nxfUDdrWOv5jAOBBr/KRB1?= =?us-ascii?q?JuPoEYLOksi7ze6/9pncbglSmDaxfa55IQmrownWqsQYm5ZpJLwryhvOrHtIeu?= =?us-ascii?q?BWyn1tKFmOgRvy5dq+8YB6/ShItP0v68BPUaPhf6QlVrNYFygpM3o05MLwqxbO?= =?us-ascii?q?SxaE62YGXWUXlhpIBBXF7A3/U5zsvCb2qvZx1S+HNsDtU7s6RSqt4LtqSB/wiS?= =?us-ascii?q?cIKTg58H3MisdtiK5XuQ+tqwBjz4LRZoyaM+dwfr7GfdMCW2VOQtpRWSJGAoO5?= =?us-ascii?q?dYQPDuwBNvtco4Tyo1YCqB2zDhSuCuzy0D9Fnn353aM63eovEg/IwRIuEM4VvX?= =?us-ascii?q?vOsNn4Lr0fXfypwKTKyzjIcvNY2S366IjNah0vou+MUqh2ccHMyEcvEB/FjlKO?= =?us-ascii?q?qYP5PzOV1/gNs3OG5OdnVOKvlWEnphpwojex2MgjlJPFhoUPylDL7Ch0xps+K9?= =?us-ascii?q?O/SE5+e9GkEZ1QujmbN4twWMMiQntntDw0yr0coZK7cykKyIgnxx7CcPOLaZSH?= =?us-ascii?q?4hXmVOqJITZ3nnJleLW4hxqo7Uegzej8W8+p21hJtipIisfAumwJ2hDJ6cWKSu?= =?us-ascii?q?Fx8lqg1DqSzQzf9+NJLEIymKHGMZAu2KQwmYAWsUnbHi/5hkH2jKiOe0Uh4Oeo?= =?us-ascii?q?6uDnbqzmp56SK4N4kw/+Prksl8G9G+g4PQ8OX2+U+eS4yrLv51H2QLJPjvEuk6?= =?us-ascii?q?nZto7VJdgDq6KnHwNY1pwv5hW/Aju8zdgVnGQLIEhYdB+FjYXlI1TOL+r5Dfe7?= =?us-ascii?q?jVSsijBrx/XeM73gHJXNIWPOkLb/crlj9UFQ0g0zzcpQ555MELEOPOrzWlPttN?= =?us-ascii?q?zfFhI2Lxa7w+PjCNlk0oMeWHmPArOCPaPJsV6I4/ovLPOWaI8Uvjb9Mfkl6OT0?= =?us-ascii?q?gX83g19ONZWuiLgabnGzHvUuCl6QYDK4i8wIEE8LpUw5R+zjzlSJFzxLMSWcRa?= =?us-ascii?q?U5sxAlAYTuIoDfQZ6mgL2dx2/vH4NZTmFLB13KFm3nIdbXE8wQYT6fd5cy2gcP?= =?us-ascii?q?UqKsHsp8jBw=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BUAQBEvBVZgLGhVdFcDg4BAQQBAQoBA?= =?us-ascii?q?RcBAQQBAQoBAYQMgQwHg2SBNohikVyCPopoiE6CDyyFeAKFEgc/GAEBAQEBAQE?= =?us-ascii?q?BAQEBEgEBCQ0JCCYxgjMkgkIBAgIBIwQZAQEsCwEECwkCBAcaHQICIhIBBQEKE?= =?us-ascii?q?gYTEol5AwgFCA6RXpEaP4sdaoFsOoMJAQEFhCMDg0IBAQEBAQEEAQEBAQEBAQE?= =?us-ascii?q?YCBKGTYR5hRCCZYJgAYdrDIFRjSuHG4cci3+CBFWPEoh/iXwUH4EVDxCBQn0IR?= =?us-ascii?q?hkGhB4qgVFZJDYBiGoBAQE?= X-IPAS-Result: =?us-ascii?q?A0BUAQBEvBVZgLGhVdFcDg4BAQQBAQoBARcBAQQBAQoBAYQ?= =?us-ascii?q?MgQwHg2SBNohikVyCPopoiE6CDyyFeAKFEgc/GAEBAQEBAQEBAQEBEgEBCQ0JC?= =?us-ascii?q?CYxgjMkgkIBAgIBIwQZAQEsCwEECwkCBAcaHQICIhIBBQEKEgYTEol5AwgFCA6?= =?us-ascii?q?RXpEaP4sdaoFsOoMJAQEFhCMDg0IBAQEBAQEEAQEBAQEBAQEYCBKGTYR5hRCCZ?= =?us-ascii?q?YJgAYdrDIFRjSuHG4cci3+CBFWPEoh/iXwUH4EVDxCBQn0IRhkGhB4qgVFZJDY?= =?us-ascii?q?BiGoBAQE?= X-IronPort-AV: E=Sophos;i="5.38,330,1491256800"; d="scan'208,217";a="223428600" Received: from mail-yw0-f177.google.com ([209.85.161.177]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 12 May 2017 15:49:27 +0200 Received: by mail-yw0-f177.google.com with SMTP id l135so11187824ywb.2 for ; Fri, 12 May 2017 06:49:27 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=ieee-org.20150623.gappssmtp.com; s=20150623; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=kXHNFlU0EbaoUdDZTbGwArBhb2PAqlIsqhZxI+JFAFs=; b=YFJ4lkuBvlVpmAkydVwIh3qTDj1n/zQUuvBsf4UW5mW8JofqfSND5ojMlj8IzWgEnE fxmg93uH3laYrDeFmadfrIrV7FUnII0ml9AM0g8eRl1D4Kk6FoH0yeZuuyPov1wzjpLZ Vo3miBeaN+qWVutIXJrGDuYcUwkdBjuaBbZ45cfi5b147N7Zk0Y3xiunJ1zfRYITGx/2 QMhIS1KRGUsbzJm5TI3XFwpBcgh1niMIpD0y6lsdV7rVUwZxrSjmdmistZkE3Pwm5CPl 8zwTAUd3RVZdalBs3Oe037sp9CS8qDFzWp/gwhJvsUDZSA69qahK3ymB8tUUrL5mzjbv FsyA== 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=kXHNFlU0EbaoUdDZTbGwArBhb2PAqlIsqhZxI+JFAFs=; b=toa4qcZ9rEtBXqS9bvOYwOs+maGvMsCakrINk4OFlSYRax7nrxjeFhDzNZtssM2FU2 48sPJUklC912Cjwg9eYXdJ6L093q9RMUFE21u7tmZwQhk87uNLVEjZf4/22E7bi2owWi ASIA8G7DlsLUlvMMy9paZdwxOI3Zmc3cfWvB1HWSyR979FYbOSRI8i3xMbc69raeBhRc FuSxDRFIg1hMra/S+qBquTw9V9Trgkok+j3YJsSbLk6KlJyLsN88lJJxHe8yw1d0qaOP wy/d/uCvqFVmy4uG5AVSg4IwszYffUFaHA54zhCHPmvuQsQhjIxOlSwYARnL00mI+9E9 tAAg== X-Gm-Message-State: AODbwcBkOnDh0cT8l05jMLPGBhFSO3rFFu3KlngUPLNYA/8qFnIMhpI5 tQgZesgQA3QIhzYL/zYzYAOHE3Gyoh+6ghs= X-Received: by 10.129.79.81 with SMTP id d78mr3488519ywb.132.1494596966199; Fri, 12 May 2017 06:49:26 -0700 (PDT) MIME-Version: 1.0 Received: by 10.129.130.66 with HTTP; Fri, 12 May 2017 06:49:25 -0700 (PDT) In-Reply-To: <20170420151331.GA3452@pllab.is.ocha.ac.jp> References: <20170419104058.GA63988@pllab.is.ocha.ac.jp> <20170420001502.GA65316@pllab.is.ocha.ac.jp> <20170420151331.GA3452@pllab.is.ocha.ac.jp> From: Ivan Gotovchits Date: Fri, 12 May 2017 09:49:25 -0400 Message-ID: To: Kenichi Asai Cc: Leo White , caml users Content-Type: multipart/alternative; boundary="001a114dcc7240ee65054f53f942" Subject: Re: [Caml-list] Question on "more general" --001a114dcc7240ee65054f53f942 Content-Type: text/plain; charset="UTF-8" A small update. But before the update, let me clarify the original reason, why the expression `let a = assert false in fun x -> 1` is not generalized. The reason is because the `assert false` is not nonexpansive (sorry for the double negation). A nonexpansive value, in OCaml compiler parlance, is a value that has "no _observable_ side effects". The `assert false` is currently typed as a special expression, that is assumed to have a side effect (i.e., it is expansive). Thus, it is basically treated the same as `let a = print_int 1 in fun x -> 1` that is also not generalized, as the evaluation of the `print_int 1 in fun x -> 1` has some effect. Apparently, the assumption that `assert false` is expansive was too conservative, as it was already subsumed (in some cases) with the value restriction relaxation. So it will be relaxed soon, see GPR#1142 [1]. And soon both of your functions will have the same type. [1]: https://github.com/ocaml/ocaml/pull/1142 On Thu, Apr 20, 2017 at 11:13 AM, Kenichi Asai wrote: > Thank you! That's very clear. So instead of writing assert false, if > I could write a "value" of type 'a, then the type of x becomes 'a. > > I confirmed it with the following file: > > -------------------------------- > let v = assert false > > let g1 = let a = v in > let f = fun x -> 1 in > f > > let g2 = let a = assert false in > let f = fun x -> 1 in > f > -------------------------------- > > If I see the types of variables via "ocamlc -i", I obtained: > > val v : 'a > val g1 : 'a -> int > val g2 : '_a -> int > > Thank you again! > > -- > Kenichi Asai > > -- > 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 > --001a114dcc7240ee65054f53f942 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
A small update.=C2=A0

But before the up= date, let me clarify the original reason, why the expression `let a =3D ass= ert false in fun x -> 1` is not generalized. The reason is because the `= assert false` is not nonexpansive (sorry for the double negation). A nonexp= ansive value, in OCaml compiler parlance, is a value that has "no _obs= ervable_ side effects". The `assert false` is currently typed as a spe= cial expression, that is assumed to have a side effect (i.e., it is expansi= ve).=C2=A0 Thus, it is basically treated the same as `let a =3D print_int 1= in fun x -> 1` that is also not generalized, as the evaluation of the `= print_int 1 in fun x -> 1` has some effect.=C2=A0

Apparently, the assumption that `assert false` is expansive was too cons= ervative, as it was already subsumed (in some cases) with the value restric= tion relaxation. So it will be relaxed soon, see GPR#1142 [1]. And soon bot= h of your functions will have the same type.=C2=A0



=

On Thu, Apr 20, 2= 017 at 11:13 AM, Kenichi Asai <asai@is.ocha.ac.jp> wrote:
Thank you!=C2=A0 That's very clear.=C2= =A0 So instead of writing assert false, if
I could write a "value" of type 'a, then the type of x become= s 'a.

I confirmed it with the following file:

--------------------------------
let v =3D assert false

let g1 =3D let a =3D v in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0let f =3D fun x -> 1 = in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0f

let g2 =3D let a =3D assert false in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0let f =3D fun x -> 1 = in
=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0f
--------------------------------

If I see the types of variables via "ocamlc -i", I obtained:

val v : 'a
val g1 : 'a -> int
val g2 : '_a -> int

Thank you again!

--
Kenichi Asai

--
Caml-list mailing list.=C2=A0 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

--001a114dcc7240ee65054f53f942--