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 6C8A58239C for ; Sun, 4 Feb 2018 02:27:11 +0100 (CET) Authentication-Results: mail3-smtp-sop.national.inria.fr; spf=None smtp.pra=garrigue@math.nagoya-u.ac.jp; spf=None smtp.mailfrom=garrigue@math.nagoya-u.ac.jp; spf=None smtp.helo=postmaster@ms.math.nagoya-u.ac.jp Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=pra; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of garrigue@math.nagoya-u.ac.jp) identity=mailfrom; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="garrigue@math.nagoya-u.ac.jp"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ms.math.nagoya-u.ac.jp) identity=helo; client-ip=133.6.130.11; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="garrigue@math.nagoya-u.ac.jp"; x-sender="postmaster@ms.math.nagoya-u.ac.jp"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3Au3SKRxO1q1LQS4+XUOEl6mtUPXoX/o7sNwtQ0KIM?= =?us-ascii?q?zox0Iv//rarrMEGX3/hxlliBBdydt6odzbKO+4nbGkU4qa6bt34DdJEeHzQksu?= =?us-ascii?q?4x2zIaPcieFEfgJ+TrZSFpVO5LVVti4m3peRMNQJW2aFLduGC94iAPERvjKwV1?= =?us-ascii?q?Ov71GonPhMiryuy+4ZLebxlViDanfb9+MAi9oBnMuMURnYZsMLs6xAHTontPde?= =?us-ascii?q?RWxGdoKkyWkh3h+Mq+/4Nt/jpJtf45+MFOTav1f6IjTbxFFzsmKHw65NfqtRbY?= =?us-ascii?q?UwSC4GYXX3gMnRpJBwjF6wz6Xov0vyDnuOdxxDWWMMvrRr0vRz+s87lkRwPpiC?= =?us-ascii?q?cfNj427mfXitBrjKlGpB6tvgFzz5LIbI2QMvd1Y6HTcs4ARWdZQsleWDFPDIO+?= =?us-ascii?q?YIUBAOQPPuhYoZf6qVYVsRu+HAysCP/vyjNUhHL727Ax3eQ7EQHB2QwtB9YAv2?= =?us-ascii?q?7Io9XsKacdT/u1x7TJwzrZdfNWwzb96IfVch8/vPqBWr1wftDLyUk1FgPFgUiQ?= =?us-ascii?q?ppL+MjOQzOsNr2ib4/BmVe21hG4nrAFwrSK2yscxkIXGnJ4axkrG9SVh2Ys4I8?= =?us-ascii?q?CzRk1jYdO8DZdduS+XO5F3T884Xm1ltjo2xqcbtZKmZCQHyJcqywTCZ/GHcIWE?= =?us-ascii?q?+A/vWPiSLDtimX5oeLCyihCv+ka60OL8TNO70FNSoypFjNbMsncN2gTW6sicUP?= =?us-ascii?q?d9+12u2SqP1wzJ7OFLO080la3bKpE727Iwi4Afvl7fESPsmkX2lLeadkQi+ue2?= =?us-ascii?q?9+Tqeqjqq5GSOoNuiwzyKLkil8KjDegiLwQCQnCX+eGm273i+U35Tq9Kjvozkq?= =?us-ascii?q?TBv5DVP94bprS4Aw9az4Ys9Q2yDzK839QEnXkLNlRFdwiIj4juO1DBOun0Deql?= =?us-ascii?q?j1u2jDhn3fLGPqX5DpXXMnfDiKvhfap660NE1AU819Vf55ZNBrEFIfLzQVPxuc?= =?us-ascii?q?fDDh45Ngy02/zoBM981oMYQ2KPA7WWPLncsV+StaoTJLywY4UE8BXwL+Mo9ra6?= =?us-ascii?q?kXgziBkecK2y0Io/Z3WxH/AgKEKcNynCmNAEREUDtRMjQfeip1SYSz9cenv6C6?= =?us-ascii?q?01/Cs6B5+rJYLKWoDrhrWO2zayW4AQb2sACEjaQiSgTJmNR/pZMHHaGcRmiDFR?= =?us-ascii?q?EOH5E9ZwhyHrjxfzzv9cFsSR/yQZsZz5090vvr/WnA0yszp9AMOM2iSQCWh/2G?= =?us-ascii?q?EQFWdvgPJP5Hdlw1LG6pBWxuRCHIYKtfZATgd8M5fTyP1zTs20UwmHfM/bEA/7?= =?us-ascii?q?EOXjOik4S5cK+/FLY0t5HI/+3BXYmS+jH79TkbWEA409t7+a1nO3Jd4vk3s=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BjAAA7YHZalwuCBoVbGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYQ6bSiDZYsYjzmZYAEJhTsCglEGBTQUAQEBAQEBAQEBAQESAQEBAQE?= =?us-ascii?q?IFgZXgjgkAYJHAQUjHQEBNwEPCxgCAiYCAlcGike9A26CJ4MKAQEFgW+Caxxpg?= =?us-ascii?q?gYBAQEBAQEBAwEBAQEBAQEBARcIgQ+DW4VUKYMFhSKDFzGCNIg9B4sakEyVcYw?= =?us-ascii?q?3iACUKYNNgTw2gXJNOD0qAYIbP4IHH4IhaYwtAQEB?= X-IPAS-Result: =?us-ascii?q?A0BjAAA7YHZalwuCBoVbGgEBAQEBAgEBAQEIAQEBAYQ6bSi?= =?us-ascii?q?DZYsYjzmZYAEJhTsCglEGBTQUAQEBAQEBAQEBAQESAQEBAQEIFgZXgjgkAYJHA?= =?us-ascii?q?QUjHQEBNwEPCxgCAiYCAlcGike9A26CJ4MKAQEFgW+CaxxpggYBAQEBAQEBAwE?= =?us-ascii?q?BAQEBAQEBARcIgQ+DW4VUKYMFhSKDFzGCNIg9B4sakEyVcYw3iACUKYNNgTw2g?= =?us-ascii?q?XJNOD0qAYIbP4IHH4IhaYwtAQEB?= X-IronPort-AV: E=Sophos;i="5.46,457,1511823600"; d="scan'208";a="253533791" Received: from bsd20.math.nagoya-u.ac.jp (HELO ms.math.nagoya-u.ac.jp) ([133.6.130.11]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/DHE-RSA-AES256-GCM-SHA384; 04 Feb 2018 02:27:09 +0100 Received: from [192.168.0.13] (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) (using TLSv1.2 with cipher ECDHE-RSA-AES256-GCM-SHA384 (256/256 bits)) (No client certificate requested) by ms.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 88BF35C4A3D; Sun, 4 Feb 2018 10:27:05 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1517707625; bh=2vRSn4vVgJF2oY5nf14YKELPVlMlnKZUCdHKMYcAfao=; h=Subject:From:In-Reply-To:Date:Cc:References:To; b=U9tgXTu5IxemhkQXva4JKP/DMrf0Su5cF8kQACWM0phcNGmIBl8eZZlaCXpKk+aJo YrKgWZxL9AiDyMZACZ1gXBepGjhylOP3MndGnOY1cSnuj/frnK/y4LBvMCuGW2ME+C OUSjBrj0YuZyGeGpxghXEWCmSpeMtGfLRDa/R2SQ= Content-Type: text/plain; charset=utf-8 Mime-Version: 1.0 (Mac OS X Mail 11.2 \(3445.5.20\)) From: Jacques Garrigue In-Reply-To: <2e9462f5-4042-230f-104b-943f1e2ebe76@gmail.com> Date: Sun, 4 Feb 2018 10:27:03 +0900 Cc: Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: <2137ABD0-E59E-418D-9C6F-948BAF16CD65@math.nagoya-u.ac.jp> References: <20180123145453.GA1916@Magus.localnet> <4C24893D-6053-4F0D-BFDD-DF76172E64F9@math.nagoya-u.ac.jp> <2e9462f5-4042-230f-104b-943f1e2ebe76@gmail.com> To: Toby Kelsey X-Mailer: Apple Mail (2.3445.5.20) X-Greylist: Sender succeeded SMTP AUTH, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Sun, 04 Feb 2018 10:27:05 +0900 (JST) X-Virus-Scanned: clamav-milter 0.99.2 at bsdserver20 X-Virus-Status: Clean X-Spam-Checker-Version: SpamAssassin 3.4.1 (2015-04-28) on bsdserver20.math.nagoya-u.ac.jp Subject: Re: [Caml-list] Are record types generative? On 2018/02/03 08:07, Toby Kelsey wrote: >=20 > On 24/01/18 08:43, Jacques Garrigue wrote: >> I.e., types can be used to optimize a program, but they do not change it= s semantics. >> It=E2=80=99s true of so-called =E2=80=9Coverloaded=E2=80=9D record label= s, it=E2=80=99s true of a labeled and default arguments >> (which use type information for compilation, but not semantics), it=E2= =80=99s true of objects, >> it=E2=80=99s true of GADT pattern-matching (again optimized), etc=E2=80= =A6 >=20 > type foo =3D { x : int } > type bar =3D { x : string } >=20 > let f r =3D r.x (* OK: uses bar *) > let f r =3D (r:foo).x (* OK: uses foo *) > let f r =3D (r.x : int) (* type error - wrong type inferred *) >=20 >=20 > Aren't the semantics different? 'f' has different types in the first two = definitions, And why does type inference fail for the last example? By semantics, I mean runtime semantics (i.e. the evaluation of a program). The first two functions both return the contents of the field x of their ar= gument. The problem with the 3rd function is not semantics but incompleteness of ty= pe inference in presence of label overloading. Jacques=