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 26ED78015D for ; Fri, 26 May 2017 10:38:53 +0200 (CEST) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=philippe.veber@gmail.com; spf=Pass smtp.mailfrom=philippe.veber@gmail.com; spf=None smtp.helo=postmaster@mail-yb0-f169.google.com Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of philippe.veber@gmail.com) identity=pra; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.national.inria.fr: domain of philippe.veber@gmail.com designates 209.85.213.169 as permitted sender) identity=mailfrom; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="philippe.veber@gmail.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@mail-yb0-f169.google.com) identity=helo; client-ip=209.85.213.169; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="philippe.veber@gmail.com"; x-sender="postmaster@mail-yb0-f169.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3AtQPzVxxXEY4j4LPXCy+O+j09IxM/srCxBDY+r6Qd?= =?us-ascii?q?2uofIJqq85mqBkHD//Il1AaPBtSFra8bw6qO6ua7CDNGuc7A+Fk5M7VyFDY9yv?= =?us-ascii?q?8q1zQ6B8CEDUCpZNXLVAcdWPp4aVl+4nugOlJUEsutL3fbo3m18CJAUk6nbVk9?= =?us-ascii?q?Kev6AJPdgNqq3O6u5ZLTfx9IhD2gar9uMRm6twvcu80XjId4Kqs8yAbCrn9Ud+?= =?us-ascii?q?hL329lK1aekhTm6sus4JJv9jlbtu48+cJHTaj1cKM0QKBCAjghL247+tDguwPZ?= =?us-ascii?q?TQuI6HscU2EWnQRNDgPY8hz0XYr/vzXjuOZl1yaUIcP5TbYvWTS/9KhrUwPniD?= =?us-ascii?q?0GNzEi7m7ajNF7gb9BrxKgoxx/xJPUYJ2QOfFjcK7RYc8WSGxcVclWSiJBH5i8?= =?us-ascii?q?b5MRAOUdIeZWoY79p14Uohu/AwmnGefjxzBMi3Pz26AxzuYvHhzc3AE4Hd0Ovn?= =?us-ascii?q?Taotv2OqkPT+660LLFwi/fY/5Mwzrx9JTEfxInrPqRXbxwa83RyUw3Gg3fjlWQ?= =?us-ascii?q?qIjlPzKN1uQVrWeQ8uVvWvy0hGE5sQF6vz+ixt8sionIgoIVy0jE9T1nz4ovO9?= =?us-ascii?q?23VlV0bsC+EJZLuCGaMpF5QsImQ21ypCk6zbgGtIe9cSMXxponwBvfZOaGc4iO?= =?us-ascii?q?+h/jVeCRIS15hH1/Yr6/iQyy/VCgy+LmVsm011FKojBZndnLs3AA0QHY5MufSv?= =?us-ascii?q?Zl4EutxTKC2xrQ5+xEO0w4i7fXJpA7zrItl5cetULOFTLslkrslq+ZbEAk9/Co?= =?us-ascii?q?6+v5ZrXmoYeRN4puhQH/NqQig8y+Dv8kPgQXUWiX5OWx2bn58U32R7VKifI2kq?= =?us-ascii?q?3Hv5zAOcsboau5DxdU0oYl9Rm/Ey+r3MoEkXQDNl5IexKKg5L3N13TLv30F+qz?= =?us-ascii?q?jlWonTtzwvDJJLzhApHDLnjZl7fheK5w61ZcyAoyydBf5opUCqkfL/7pRE/+qs?= =?us-ascii?q?fXAQEjMwGvzObnDc9y1oIaWW6VHqCZN6bSvUeS5u0zO+mMeJMVuDHlJvc5/fHu?= =?us-ascii?q?iHs5lUYZfamoxpsXdGu1Hu9mIkWceXrjmM0NEWYMvgokTezlkkeOUTBJZyX6Y6?= =?us-ascii?q?VpwzgnBYDuLoDYR4Pl1OHegnuwRscHbD4WWlvVGi/kLdmNAfpdNymefZE9nBQL?= =?us-ascii?q?ULGgT8kq0hT45yHgzL8yFurV/iwArZ+r6tV/6vebwQky9Dh1F9yQlX+ARWxutm?= =?us-ascii?q?wNTj4ymqt4pBoumR+4zaFkjqkARpRo7PRTX1JmZJM=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BqAADV6CdZhqnVVdFdHAEBBAEBCgEBF?= =?us-ascii?q?wEBBAEBCgEBg00/exIHg2iBNohikWOCP5M6gg8uhXYCgwAHPxgBAQEBAQEBAQE?= =?us-ascii?q?BARIBAQEICwsIKC+CMwyCWgECAQEBIwQZARsPAwsBAwELBgMCBAcaHQICIQEBE?= =?us-ascii?q?QEFAQoSBhMSiX8BAw0IEI0tkRo/jAeBbBgFARyDCgWDXAoZJwMKVoM7AQEBAQE?= =?us-ascii?q?BAQEBAQEBAQEBAQEZAgYShk2EeoJXgjyCZYJgAQSHaQyBS4hEi2Q7ghCFEIcwh?= =?us-ascii?q?FiCW48cizKHVBQfgRUPEHdLMCEjWxmEMCofgXE+NgGJCAEBAQ?= X-IPAS-Result: =?us-ascii?q?A0BqAADV6CdZhqnVVdFdHAEBBAEBCgEBFwEBBAEBCgEBg00?= =?us-ascii?q?/exIHg2iBNohikWOCP5M6gg8uhXYCgwAHPxgBAQEBAQEBAQEBARIBAQEICwsIK?= =?us-ascii?q?C+CMwyCWgECAQEBIwQZARsPAwsBAwELBgMCBAcaHQICIQEBEQEFAQoSBhMSiX8?= =?us-ascii?q?BAw0IEI0tkRo/jAeBbBgFARyDCgWDXAoZJwMKVoM7AQEBAQEBAQEBAQEBAQEBA?= =?us-ascii?q?QEZAgYShk2EeoJXgjyCZYJgAQSHaQyBS4hEi2Q7ghCFEIcwhFiCW48cizKHVBQ?= =?us-ascii?q?fgRUPEHdLMCEjWxmEMCofgXE+NgGJCAEBAQ?= X-IronPort-AV: E=Sophos;i="5.38,396,1491256800"; d="scan'208,217";a="225229704" Received: from mail-yb0-f169.google.com ([209.85.213.169]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 26 May 2017 10:38:51 +0200 Received: by mail-yb0-f169.google.com with SMTP id 130so893044ybl.3 for ; Fri, 26 May 2017 01:38:51 -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=RSo5jc4tPJL6rYFlRfBGZUHOq3ijgIGUyTx6n7MmatE=; b=KuCt4CPMrAvWghd31g6wIYgWOJ+6hv6YcCYB3ZIbVy8DhFC0vcXfv+6YqGJPgKmRMx MR1EkDW18+RdvNauW6hgZapHkl7kP0rRsrVDAo0zKGg755JvwcxYejGWPGdmCMU5Vv+r BhdoTLbuNZJvTXgaj4biCDJfT8Y0pKN3EDAZQgt6biIyXuEaJ6hsxcUbnrEsQWjkQKD6 2N+De2J+9hjSFZNZVTI/KiR8WVOkHMS4gUvIKoKdZrm1w++s7HvZjoTxkLb11BMQguOa xZKs6JFEJw2ysRpeFLcgrTr5sq8wG2DZbtx1XPA0vV0yCY7HI4MBCwjVR7YLoNLNIzho Y27Q== 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=RSo5jc4tPJL6rYFlRfBGZUHOq3ijgIGUyTx6n7MmatE=; b=CiIQ+EvLYH0+S3YC9SpRKduTYAg/VHDXdxEFkghdgsAaUcSeZPuVvMDueNrLcH+ni0 DoYZM7y2DZbd3lEvZLaZ+8stxkUJrwv2nYnFZuHyBY+jlHvxdJhxXy1xO7SfvjG7RGYL oD/H3SQiXATjuIHUXLvchmb1xU5CxvzvIw3sOta4MajQzQ4iIeh4h6DkuCuc4uhi353q idY1ZnjNXwXeYVsCOJ1wcGUPen12B39vQVIJY464CvKxq5YDfs98fe66eLN+mPIsxXEr W6ypNH0BfO2F+lMPkWyanhgz/JfiH7YEo1wSOz7nuJlD96BcNDn29einfHUXbi/ACJSJ hJvw== X-Gm-Message-State: AODbwcCLRJAV74HM1bxPuLp/Lp6nMKstEsURLsb6plgDhfKARwKAE894 +vdFJOCbieDkG2u8rgQWF1KfALqgeyPY X-Received: by 10.37.216.211 with SMTP id p202mr803268ybg.167.1495787930266; Fri, 26 May 2017 01:38:50 -0700 (PDT) MIME-Version: 1.0 Received: by 10.37.184.6 with HTTP; Fri, 26 May 2017 01:38:29 -0700 (PDT) In-Reply-To: <8de32ec3-f6ab-7c86-a270-7f7ccbe24d20@gmail.com> References: <8de32ec3-f6ab-7c86-a270-7f7ccbe24d20@gmail.com> From: Philippe Veber Date: Fri, 26 May 2017 10:38:29 +0200 Message-ID: To: Matej Kosik <5764c029b688c1c0d24a2e97cd764f@gmail.com> Cc: caml users Content-Type: multipart/alternative; boundary="94eb2c062c6c3e365d0550694489" X-Validation-by: philippe.veber@gmail.com Subject: Re: [Caml-list] a question about Ocaml semantics --94eb2c062c6c3e365d0550694489 Content-Type: text/plain; charset="UTF-8" Hi Matej, I'm no expert, but I'm pretty sure the problem here is related to the value restriction [0]. If you change the last line to: # let _ = f { enter = fun x -> (+) 1 x } ;; - : int = 3 there is no typing error anymore. Note that with ocaml 4.04.0 and 4.04.1, your original definition is accepted. hope this helps, Philippe. [0] https://caml.inria.fr/pub/papers/garrigue-value_restriction-fiwflp04.pdf 2017-05-26 10:08 GMT+02:00 Matej Kosik < 5764c029b688c1c0d24a2e97cd764f@gmail.com>: > Hi, > > There's an Ocaml language feature I do not understand. > > E.g. in this example: > > type 'a phantom = int > type t = { enter : 'a. 'a phantom -> int } > let f g = g.enter 2 > let _ = f { enter = fun x -> 1 + x } (* ok *) > let _ = f { enter = (+) 1 } (* fails to typecheck *) > > I don't get why, if we have: > > type 'a phantom = int > > i.e. "'a phantom" is defined as an alias of "int", > how is it possible that the following types: > > { enter : 'a. 'a phantom -> int } > > is not equal to > > { enter : 'a. int -> int } > > I've tried to find a corresponding section in the Reference Manual, but I > failed. > Where is this explained? > > -- > 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 > --94eb2c062c6c3e365d0550694489 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Hi Matej,

I'm no expert, but I'm prett= y sure the problem here is related to the value restriction [0]. If you cha= nge the last line to:

# let _ =3D f { enter =3D fun x -> (+) 1 x } ;;
- : int =3D 3

there is no typing error anymore. Note that with ocaml = 4.04.0 and 4.04.1, your original definition is accepted.

= hope this helps,

2017-05-26 10:08 GMT+02:00 Matej Kosik <<= a href=3D"mailto:5764c029b688c1c0d24a2e97cd764f@gmail.com" target=3D"_blank= ">5764c029b688c1c0d24a2e97cd764f@gmail.com>:
Hi,

There's an Ocaml language feature I do not understand.

E.g. in this example:

=C2=A0 type 'a phantom =3D int
=C2=A0 type t =3D { enter : 'a. 'a phantom -> int }
=C2=A0 let f g =3D g.enter 2
=C2=A0 let _ =3D f { enter =3D fun x -> 1 + x } (* ok *)
=C2=A0 let _ =3D f { enter =3D (+) 1 }=C2=A0 =C2=A0 =C2=A0 =C2=A0 =C2=A0 (*= fails to typecheck *)

I don't get why, if we have:

=C2=A0 type 'a phantom =3D int

i.e. "'a phantom" is defined as an alias of "int",<= br> how is it possible that the following types:

=C2=A0 { enter : 'a. 'a phantom -> int }

is not equal to

=C2=A0 { enter : 'a. int -> int }

I've tried to find a corresponding section in the Reference Manual, but= I failed.
Where is this explained?

--
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

--94eb2c062c6c3e365d0550694489--