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 EE97D82355 for ; Wed, 24 Jan 2018 09:43:26 +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=3AUNkpABcww9NQ1Gba5DIMTCEBlGMj4u6mDksu8pMi?= =?us-ascii?q?zoh2WeGdxcS6YB7h7PlgxGXEQZ/co6odzbaO6ua4ASQp2tWoiDg6aptCVhsI24?= =?us-ascii?q?09vjcLJ4q7M3D9N+PgdCcgHc5PBxdP9nC/NlVJSo6lPwWB6nK94iQPFRrhKAF7?= =?us-ascii?q?Ovr6GpLIj8Swyuu+54Dfbx9HiTahfL9+Ngm6oRnMvcQKnIVuLbo8xAHUqXVSYe?= =?us-ascii?q?RWwm1oJVOXnxni48q74YBu/SdNtf8/7sBMSar1cbg2QrxeFzQmLns65Nb3uhnZ?= =?us-ascii?q?TAuA/WUTX2MLmRdVGQfF7RX6XpDssivms+d2xSeXMdHqQb0yRD+v9LlgRgP2hy?= =?us-ascii?q?gbNj456GDXhdJ2jKJHuxKquhhzz5fJbI2JKPZye6XQds4YS2VcRMZcTzBODYyh?= =?us-ascii?q?YYUPDeUPM+lWoYrzp1UQqhWzHhWsBPrqyjNUhn/6wa833uI8Gg/GxgwgGNcOvW?= =?us-ascii?q?zQotrvKKgSSP21w7fTzT7ebv1Zwy396JLJchAuvPGDQ697fM3eyUY1DQPFlFSQ?= =?us-ascii?q?qYP4PzyLzekNtnKU7/ZgVe61jW4osQ5xoj+vx8g2k4XJm5gZxUrY+iljwoY1Pc?= =?us-ascii?q?S1RUhmatCnCJtdrzyWOoV4T884Qmxkojs2x7MatZKhYSQG1ZIqzAPFZfOdaYiH?= =?us-ascii?q?+BfjWf6RIThmgHJlf6qyhxOp8US6z+3zTNW00FZQoipDiNbMuXcN1hzJ5cSeV/?= =?us-ascii?q?tx5F2u1iqV2wDR8uFIOUE0lazFJJ492rM8i5QevErZEiL3gkn6kaGbelk+9uS1?= =?us-ascii?q?9ujrerDmqYWdN49whAH+KKMumsmnDOQ3KAcORXKb+eWz1L3+40L0W7BKgecqkq?= =?us-ascii?q?nZqpzaI94UpqG+Aw5VyIkv8gu/Ay2839sEh3UHLkpFdAqdj4f1I1HOPOz4DfCn?= =?us-ascii?q?jluwijhrwvTGMqTlApXMNXjDjKzsfa196k5Z0Ao818pT55NSCrEbIfL8QFX9tN?= =?us-ascii?q?LCDkxxDwvh6ObqFJ1Yy5kCWXPHVqqEKr/SoBmD5u8zC+aJbY4R/j36Lq52yeTp?= =?us-ascii?q?iCobkFQEYKSylbQecmq5EelraxGWaGD2g9gcHE8PtxY+Curjh1qTWHtOIX+5Ga?= =?us-ascii?q?AksGJoQLm6BJvOE9j+yIeK2z22S9gPPjgfWwK8VEzwfoDBYM8iLSebI8tviDsB?= =?us-ascii?q?D+HzToY91VeovQD92rMiM6zd8WsarcC7jYQn16jojRg3sAdMIYGFyWjXFjNxl3?= =?us-ascii?q?8IATk/06duqAlgjF6Il6pg0aQBSI5joshRWwJ/Dqbyiux3D9eoBlDEZZGMQUqm?= =?us-ascii?q?BNOvDjYgR5cshdYFJURlSY2v?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0BvAAACRmhalwuCBoVeGgEBAQEBAgEBA?= =?us-ascii?q?QEIAQEBAYUcJ4NdixiPTSeJD5BGAQmFOwKFEgYFNBQBAQEBAQEBAQEBARIBAQE?= =?us-ascii?q?BAQgWBleCOCQBgkYBAQEDASMEGQEBNwEECwsYAgImAgIhNgYTFIoJAw0Hsmtug?= =?us-ascii?q?W06gwoBAQWEMQ0sHII9AQEBAQEBAQMBAQEBAQEBARgIgQ+DPIVUKQyCeYJrRAS?= =?us-ascii?q?Bb4JaPTGCNIg2B4sThkCJPj2QW4UGlCSOHoVtg0uBPDaBck04PSoBgX8/ggYfg?= =?us-ascii?q?gIyN44gAQEB?= X-IPAS-Result: =?us-ascii?q?A0BvAAACRmhalwuCBoVeGgEBAQEBAgEBAQEIAQEBAYUcJ4N?= =?us-ascii?q?dixiPTSeJD5BGAQmFOwKFEgYFNBQBAQEBAQEBAQEBARIBAQEBAQgWBleCOCQBg?= =?us-ascii?q?kYBAQEDASMEGQEBNwEECwsYAgImAgIhNgYTFIoJAw0HsmtugW06gwoBAQWEMQ0?= =?us-ascii?q?sHII9AQEBAQEBAQMBAQEBAQEBARgIgQ+DPIVUKQyCeYJrRASBb4JaPTGCNIg2B?= =?us-ascii?q?4sThkCJPj2QW4UGlCSOHoVtg0uBPDaBck04PSoBgX8/ggYfggIyN44gAQEB?= X-IronPort-AV: E=Sophos;i="5.46,406,1511823600"; d="scan'208";a="252286972" 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; 24 Jan 2018 09:43:24 +0100 Received: from garrigue-mini.math.nagoya-u.ac.jp (garrigue-mini.math.nagoya-u.ac.jp [172.16.30.37]) (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 86DDC66C53C; Wed, 24 Jan 2018 17:43:20 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/simple; d=math.nagoya-u.ac.jp; s=20160220; t=1516783400; bh=ZRRtHxqGIW0/gTQhs1Il3g6zk8r1yhyCeeOqbpVb0dQ=; h=Subject:From:In-Reply-To:Date:Cc:References:To; b=bCb/Az91bCfYAyUf9T2EXCdlH7QlIciFEICTcFELP+rSxzCuNdVFwYuplI/ooHaLc COuZPUxa0FPId0tYRFc51AoKRIwYNzoAW9Yl1JMwukL8K5/esFVMjquUQoY1neKFtQ L4wL0GOQJw7XSQOtnTKQf8ACMBFnRKZxYwctZ6mY= 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: Date: Wed, 24 Jan 2018 17:43:20 +0900 Cc: Jeremy Yallop , Oleg Kiselyov , Mailing List OCaml Content-Transfer-Encoding: quoted-printable Message-Id: <4C24893D-6053-4F0D-BFDD-DF76172E64F9@math.nagoya-u.ac.jp> References: <20180123145453.GA1916@Magus.localnet> To: Chet Murthy X-Mailer: Apple Mail (2.3445.5.20) X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-4.6.2 (ms.math.nagoya-u.ac.jp [0.0.0.0]); Wed, 24 Jan 2018 17:43:20 +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/01/24 10:05, Chet Murthy wrote: >=20 > On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop wrote: > IHere's a closely > related property that's much harder to break: does adding annotations > leave the run-time behaviour of a program unchanged? There are far > fewer programs that violate that property, I think. >=20 > I'm no longer a type-theorist, so I don't have the knowledge to answer, b= ut: >=20 > It was a critically important property of *all* the original MLs (and of = the theoretical development of ML) that a well-type ML program P could be "= type-erased" to an untyped program TE(P); then when P -eval-> V, and TE(P) = -eval-> V', TE(V) =3D=3D V'. Where's I'm abusing notation, b/c "-eval->" m= eans in the first case "evaluation on typed programs" and in the second, "e= valuation on untyped programs" which might be entirely different things. >=20 > This was the (famous amongst that admittedly tiny community) "commuting r= ectangles type erasure property=E2=80=9D. This property is still true in OCaml (minus Obj.magic, but Obj.magic is not= valid OCaml :-). I.e., types can be used to optimize a program, but they do not change its s= emantics. It=E2=80=99s true of so-called =E2=80=9Coverloaded=E2=80=9D record labels, = 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 > A -concrete- effect of this property in MLs (again, I'm no longer a type-= theorist, so I might be getting this wrong) is ML-family languages don't su= pport reflection, and when they support object-orientation, they don't supp= ort "instanceof" (e.g. like Java's). because these require that compile-ti= me type-information be present at runtime. Indeed, as soon as we add type classes, type witnesses or (type-selected) i= mplicit arguments, this property is lost. > For those who think this is a bad design choice, I can only say that as a= systems-jock, I appreciate a language that is -so- high-level, and -yet- c= an easily be programmed in such a way that I can understand the runtime beh= aviour in terms of a C-like runtime model. By contrast, to understand Java= *for real* one must have enormously detailed knowledge of the JVM -- the p= articular JVM implementation -- one is using. Indeed. Jacques=