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 DF8D37FA5E for ; Thu, 20 Apr 2017 11:25:08 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=lwhite@janestreet.com; spf=Pass smtp.mailfrom=lwhite@janestreet.com; spf=None smtp.helo=postmaster@mxout3.mail.janestreet.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lwhite@janestreet.com) identity=pra; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lwhite@janestreet.com"; x-sender="lwhite@janestreet.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of lwhite@janestreet.com designates 38.105.200.229 as permitted sender) identity=mailfrom; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lwhite@janestreet.com"; x-sender="lwhite@janestreet.com"; 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@mxout3.mail.janestreet.com) identity=helo; client-ip=38.105.200.229; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lwhite@janestreet.com"; x-sender="postmaster@mxout3.mail.janestreet.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AnAyWPR2oaoAfCvvcsmDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0eLPad9pjvdHbS+e9qxAeQG96Kt7Qc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q89pDXbAhEniaxba9vJxiqsAvdsdUbj5F/Iagr0BvJpXVIe+?= =?us-ascii?q?VSxWx2IF+Yggjx6MSt8pN96ipco/0u+dJOXqX8ZKQ4UKdXDC86PGAv5c3krgfM?= =?us-ascii?q?QA2S7XYBSGoWkx5IAw/Y7BHmW5r6ryX3uvZh1CScIMb7Vq4/Vyi84Kh3SR/okC?= =?us-ascii?q?YHOCA/8GHLkcx7kaZXrAu8qxBj34LYZYeYP+d8cKzAZ9MXXWhOXshRWSJPAY2y?= =?us-ascii?q?cpUBAPYaMOlCs4XwvUEDoQeiCQSuAu7k1z9GhmXx3a0/y+kvFx/J3As9FN0OsH?= =?us-ascii?q?TUrcn1O7kPWu2yyKnJwzXDb/JK2Tjj84XIcAouofeSUrJrbcrR01cgGB3ZjlmK?= =?us-ascii?q?tYPlODaV2/0LvmOG7ORgTfqihmAkpg1rvzSj2schhpPXio4J1lzI7zt1zJgxKN?= =?us-ascii?q?GgVkJ3fdqpHIFTuiyaLYd6XN0uTm9ytConzrALvZi2dzUQxps93R7QcfmHfpCI?= =?us-ascii?q?4h39UOaRJi91hHdqebK4mhay7Uatxvf5Vsau0VZKqjBJktvWuXALyRPT8dSHSu?= =?us-ascii?q?Fj8Ui/xTaDzRzc6uZBIUwslKrbLYAuwqIom5cdsknPBDL6lFn2gaOMaEko5vSk?= =?us-ascii?q?5/75brn4opKQL4p0hRv/MqQqlMy/G+M4Mg0WUmif9+W81Lzj/VHnT7hRjP05iK?= =?us-ascii?q?/Zv47BJcQHvK62HRFa0po55xmjCDem1cwUnWMbI1JdZBKHk4/pNknSL//iCPe/?= =?us-ascii?q?h02gkDNqx/DdIr3sGY7NL3jGkLf5Z7lx8U9cyAwpzdBe/Z1YEL8BIOigEnP24f?= =?us-ascii?q?/VCB4yMw386v3uCZ0p35gXWEqOGemeO6Pb91aDoOA3dbqifogQ7RLwLLAa5//y?= =?us-ascii?q?gDdtnUAdfLWk9Zkebn2jAu5rLlnfan3p1IRSWVwWtxYzGbS5wGaJViReMjPrB/?= =?us-ascii?q?ox?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BtAAAHffhYfeXIaSZcDhAGDBkGDIJDg?= =?us-ascii?q?lIHg2CBBJp0lWOCD4YkAoNxBz8YAQEBAQEBAQEBAQESAQEJFghXgjMiAYJAAQI?= =?us-ascii?q?CASMEGQEBNwEECwsEByIVAgIiEgEFARwGE4oUCAOeDj+LHGiBbDqDCAEBBYgUA?= =?us-ascii?q?QEBAQEFAQEBAQEBAQEYCBKGQYR2hRaCDQwugl+dNpMCinGGXpJKFB+BFR+BPUM?= =?us-ascii?q?gFVwGhDmBUT50iGsBAQE?= X-IPAS-Result: =?us-ascii?q?A0BtAAAHffhYfeXIaSZcDhAGDBkGDIJDglIHg2CBBJp0lWO?= =?us-ascii?q?CD4YkAoNxBz8YAQEBAQEBAQEBAQESAQEJFghXgjMiAYJAAQICASMEGQEBNwEEC?= =?us-ascii?q?wsEByIVAgIiEgEFARwGE4oUCAOeDj+LHGiBbDqDCAEBBYgUAQEBAQEFAQEBAQE?= =?us-ascii?q?BAQEYCBKGQYR2hRaCDQwugl+dNpMCinGGXpJKFB+BFR+BPUMgFVwGhDmBUT50i?= =?us-ascii?q?GsBAQE?= X-IronPort-AV: E=Sophos;i="5.37,225,1488841200"; d="scan'208,217";a="220944290" Received: from mxout3.mail.janestreet.com ([38.105.200.229]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 20 Apr 2017 11:25:07 +0200 Received: from [172.27.56.68] (helo=tot-qpr-mailcore1) by mxout3.mail.janestreet.com with esmtps (TLSv1.2:ECDHE-RSA-AES256-GCM-SHA384:256) (Exim 4.89) (envelope-from ) id 1d18Kn-0003cZ-9L for caml-list@inria.fr; Thu, 20 Apr 2017 05:25:05 -0400 X-JS-Flow: external X-JS-Scanner-attachment: (ok) No attachments Received: by tot-qpr-mailcore1 with JS-mailcore (0.1) (envelope-from ) id BY-H5x-AJzaTM-Ix; 2017-04-20 05:25:05.283408-04:00 Received: from mail-io0-f199.google.com ([209.85.223.199]) by mxgoog1.mail.janestreet.com with esmtps (TLSv1.2:ECDHE-RSA-AES128-GCM-SHA256:128) (Exim 4.89) (envelope-from ) id 1d18Kn-0004Xl-8F for caml-list@inria.fr; Thu, 20 Apr 2017 05:25:05 -0400 Received: by mail-io0-f199.google.com with SMTP id r16so51512948ioi.7 for ; Thu, 20 Apr 2017 02:25:05 -0700 (PDT) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=janestreet.com; s=google; h=mime-version:in-reply-to:references:from:date:message-id:subject:to :cc; bh=FTRI9WKUSfzK8oarraFtN/uhCp3PEbO57kiosi4UB9Q=; b=E30+61WpFoU3GuW/uN+MTcJ2Mg83p8D6g0VeHrTt5cmz5So0RNw9RsPHlEaTapm2+Z ujfgym/CT5PUOhx2EptHTZFwh/64aepKe+a1+0lu2rz/r/cbKNRwiKnyd5AnZGAJOWrB jujZA4DrdOvC6yURg/4lMUJuOncF2QGH1/YX8= 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=FTRI9WKUSfzK8oarraFtN/uhCp3PEbO57kiosi4UB9Q=; b=pNBL2nMp7amXDslR2s5vB6iLEqr5zm2IN8snjCTZDyvzVYkCZVQxnpW34gII0I3V3v 2d2yXpg+RISxN7ttHyy1Aafo/Eunrprqkcu7B0H7J/p1IZ6FHbkNovf2nJu96gyTh8UF hS52hR1wTuxfg6v02cO2S+rO9EF1zTuqimocnPsK4O/90Quxh4cLuug0C61S05OWuVmF mFuS6PAPkKk0j1BQRpV68NBmgeluiq8W1fjdVgK9xDhqtnumVLEymbqilahLshkDmxhA wTEaCwFK3ZTWNI9Buf4FLiH5nxt0CnOrxOCRikd7bTgokoqtO0ssznfi1cU4oLczGept UkGw== X-Gm-Message-State: AN3rC/51KXProYeTC9QCsS9KFoiiwPhqG3GB+77xQMQm8G5mCrgK2Anr ZoCBjuMGG7j8e22xzBJCW6xNEhBkiYsgkYFo630tkVf8O9DGmshAMH6Uk3V32yVTIPLvsXTDrvT EhP/PC3abEaOWkCpD X-Received: by 10.107.17.220 with SMTP id 89mr8330353ior.177.1492680303971; Thu, 20 Apr 2017 02:25:03 -0700 (PDT) X-Received: by 10.107.17.220 with SMTP id 89mr8330342ior.177.1492680303800; Thu, 20 Apr 2017 02:25:03 -0700 (PDT) MIME-Version: 1.0 Received: by 10.107.4.131 with HTTP; Thu, 20 Apr 2017 02:25:03 -0700 (PDT) In-Reply-To: <20170420001502.GA65316@pllab.is.ocha.ac.jp> References: <20170419104058.GA63988@pllab.is.ocha.ac.jp> <20170420001502.GA65316@pllab.is.ocha.ac.jp> From:Leo White Date: Thu, 20 Apr 2017 10:25:03 +0100 Message-ID: To:Kenichi Asai Cc:caml users Content-Type: multipart/alternative; boundary=001a113f5e18459197054d95b7b4 X-JS-Processed-by: mailcore Subject: Re: [Caml-list] Question on "more general" --001a113f5e18459197054d95b7b4 Content-Type: text/plain; charset=UTF-8 The expression: let a = assert false in fun x -> 1 is not a syntactic value, so because of the value restriction it has type: '_a -> int That '_a comes from the `x` parameter. > the variable a is not used in fun x -> 1 OCaml doesn't take account of whether `a` is used in deciding if something is a value, although if you had written: ignore (assert false); fun x -> 1 then it would have been a value. I suspect the part you are missing is that generalization happens as part of `let` (and `match`, class definitions, polymorphic record creation, etc...). If you had written: let a = assert false in let f = fun x -> 1 in f then the type associated with `x` would have been generalized as part of the definition of `f` although the resulting function would still have type: '_a -> int Regards, Leo On 20 April 2017 at 01:15, Kenichi Asai wrote: > > Without looking too closely at your question I would assume that is just > the > > value restriction. > > But both in the expressions: > > > let a = 1 in fun x -> 1 > > let a = assert false in fun x -> 1 > > the variable a is not used in fun x -> 1. How can the type of x be > affected by an unused binding for a around fun x -> 1? > > It also seems that assert false can be used polymorphically (because > of the relaxed value restriction?): > > # fun () -> let a = assert false in (a 1, a true);; > Warning 20: this argument will not be used by the function. > Warning 20: this argument will not be used by the function. > - : unit -> 'a * 'b = > > -- > Kenichi Asai > --001a113f5e18459197054d95b7b4 Content-Type: text/html; charset=UTF-8 Content-Transfer-Encoding: quoted-printable
The expression:

=C2=A0 let a =3D assert= false in
=C2=A0 =C2=A0 fun x -> 1

is= not a syntactic value, so because of the value restriction it has type:

=C2=A0 =C2=A0 '_a -> int

=
That '_a comes from the `x` parameter.

&g= t;=C2=A0the variable a is not used in fun = x -> 1

OCaml doesn't take account of= whether `a` is used in deciding if something is a value, although if you h= ad written:

=C2=A0 ignore (assert false);
=C2=A0 fun x -> 1

then it would have been a v= alue.

I suspect the part you are missing is that g= eneralization happens as part of `let` (and `match`, class definitions, pol= ymorphic record creation, etc...). If you had written:

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

then the type associated= with `x` would have been generalized as part of the definition of `f` alth= ough the resulting function would still have type:

=C2=A0 '_a -> int

Regards,

<= /div>
Leo
=C2=A0=C2=A0
=
On 20 April 2017 at 01:15, Kenichi Asai <a= sai@is.ocha.ac.jp> wrote:
<= span class=3D"">> Without looking too closely at your question I would a= ssume that is just the
> value restriction.

But both in the expressions:

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

the variable a is not used in fun x -> 1.=C2=A0 How can the type = of x be
affected by an unused binding for a around fun x -> 1?

It also seems that assert false can be used polymorphically (because
of the relaxed value restriction?):

# fun () -> let a =3D assert false in (a 1, a true);;
Warning 20: this argument will not be used by the function.
Warning 20: this argument will not be used by the function.
- : unit -> 'a * 'b =3D <fun>

--
Kenichi Asai

--001a113f5e18459197054d95b7b4--