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 mail2-relais-roc.national.inria.fr (mail2-relais-roc.national.inria.fr [192.134.164.83]) by sympa.inria.fr (Postfix) with ESMTPS id 8BF7D82355 for ; Wed, 24 Jan 2018 02:05:34 +0100 (CET) Authentication-Results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=murthy.chet@gmail.com; spf=Pass smtp.mailfrom=murthy.chet@gmail.com; spf=None smtp.helo=postmaster@mail-pf0-f179.google.com Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of murthy.chet@gmail.com) identity=pra; client-ip=209.85.192.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="murthy.chet@gmail.com"; x-sender="murthy.chet@gmail.com"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of murthy.chet@gmail.com designates 209.85.192.179 as permitted sender) identity=mailfrom; client-ip=209.85.192.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="murthy.chet@gmail.com"; x-sender="murthy.chet@gmail.com"; x-conformance=sidf_compatible; x-record-type="v=spf1" Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of postmaster@mail-pf0-f179.google.com) identity=helo; client-ip=209.85.192.179; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="murthy.chet@gmail.com"; x-sender="postmaster@mail-pf0-f179.google.com"; x-conformance=sidf_compatible IronPort-PHdr: =?us-ascii?q?9a23=3ATNZywxHZn7Mpj49m6OOJHp1GYnF86YWxBRYc798d?= =?us-ascii?q?s5kLTJ78osuwAkXT6L1XgUPTWs2DsrQY07OQ6/iocFdDyK7JiGoFfp1IWk1Nou?= =?us-ascii?q?QttCtkPvS4D1bmJuXhdS0wEZcKflZk+3amLRodQ56mNBXdrXKo8DEdBAj0OxZr?= =?us-ascii?q?KeTpAI7SiNm82/yv95HJbAhEmCexbaluIBmqsA7cqtQYjYx+J6gr1xDHuGFIe+?= =?us-ascii?q?NYxWNpIVKcgRPx7dqu8ZBg7ipdpesv+9ZPXqvmcas4S6dYDCk9PGAu+MLrrxjD?= =?us-ascii?q?QhCR6XYaT24bjwBHAwnB7BH9Q5fxri73vfdz1SWGIcH7S60/VC+85Kl3VhDnlC?= =?us-ascii?q?YHNyY48G7JjMxwkLlbqw+lqxBm3oLYfJ2ZOP94c6jAf90VWHBBU95TWCxPAo2y?= =?us-ascii?q?YYgBAfcfM+lEtITyvUcCoAGkCAWwGO/iyDlFjWL2060g1OQhFBnL0RIgH90QrH?= =?us-ascii?q?TfsdL7NLoIUeCpzKnJzSjIYvRT2Tfg8ojIbhAhoPGWUb1sccre11UvGhjKjlWV?= =?us-ascii?q?s4PlPjeV2v4RvGic6uptTOSigHMkpQFpujWj2Nsgh43Tio8Wyl3I7zh1zYIrKd?= =?us-ascii?q?GiVUJ2Y9qpHZ1NvC+ALYR2WNktQ2RwtSY61LIGvZm7cTAPyJs9xh7fb+WLc5CG?= =?us-ascii?q?4h7/TeqRLyp0iXBhdb6liBay9k+gyuL4VsaqylpFsi1FktzUunAM0Rzc9NSHR+?= =?us-ascii?q?Nj8ku93TuDzQPe5+FeLUwpkafXNYQtzqMym5cXqUjDGzX5mETyjK+YbEUk/e2o?= =?us-ascii?q?5vziYrX7vJ+cK490iwHkPqsymsywH/g4PxMBX2ie4+u81bnj8VflT7VNi/06ir?= =?us-ascii?q?PZv4zCJcQHuq65BBdY3Zo55Ba6CzeqydAYnXgcLFJZYx+HlIjoO1TWIP/iF/u/?= =?us-ascii?q?glKskC1qx//cJLHhDI/NfTD/l+LDcKxw7l8U+QM3yddHr8ZFA7UFJ+rbVUr4td?= =?us-ascii?q?ieBRg8ZV+a2eHiXf59259WfH+VHq+IePfXrEWU5vNpKOmBeKcavT/8L74u4Pu4?= =?us-ascii?q?3ixxokMUYaT8hchfU3u/BPkzZhzBOSO90OdEKn8Du08FdMKvjVSDVTBJYHPrBv?= =?us-ascii?q?Az4zg6DMStCoKRH9nx0ozE5z+yG9htXk4DEkqFSC66eICNWvNKYyWXcJc4z240?= =?us-ascii?q?EIO5Qopk7imA8Q/3z709cLjR8ywc8IrtjJ17vrKC0x418jNwAoKW1GTfF2w=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0CzBACc2mdahrPAVdFeHAEBAQQBAQoBA?= =?us-ascii?q?YUcFBMHg1aBOZdQggKEAZVUCoU7AoRvBxkHBDQUAQEBAQEBAQEBAQESAQEBCAs?= =?us-ascii?q?LCCgvgjgkAYJHAQUjBBkBGx0BAwwGBQQHDSoCAiEBAREBBQEcBhMUiggBAxWmY?= =?us-ascii?q?UCME4FtGAUBHIMLBYNqChknDVmCLAEBAQEBBQEBAQEBAQEZAgYShDmCFYZtgmt?= =?us-ascii?q?EBIUGgmUFk0mPeD2QWIUFdJMvjhqJIhQFIIEXNoFyMxojUjKBeIJFH4IUIDeOG?= =?us-ascii?q?gEBAQ?= X-IPAS-Result: =?us-ascii?q?A0CzBACc2mdahrPAVdFeHAEBAQQBAQoBAYUcFBMHg1aBOZd?= =?us-ascii?q?QggKEAZVUCoU7AoRvBxkHBDQUAQEBAQEBAQEBAQESAQEBCAsLCCgvgjgkAYJHA?= =?us-ascii?q?QUjBBkBGx0BAwwGBQQHDSoCAiEBAREBBQEcBhMUiggBAxWmYUCME4FtGAUBHIM?= =?us-ascii?q?LBYNqChknDVmCLAEBAQEBBQEBAQEBAQEZAgYShDmCFYZtgmtEBIUGgmUFk0mPe?= =?us-ascii?q?D2QWIUFdJMvjhqJIhQFIIEXNoFyMxojUjKBeIJFH4IUIDeOGgEBAQ?= X-IronPort-AV: E=Sophos;i="5.46,404,1511823600"; d="scan'208,217";a="310374339" Received: from mail-pf0-f179.google.com ([209.85.192.179]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 24 Jan 2018 02:05:33 +0100 Received: by mail-pf0-f179.google.com with SMTP id 23so1733468pfp.3 for ; Tue, 23 Jan 2018 17:05:33 -0800 (PST) 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=dJkaM6IVIjTDs+j8XZYHGWupMlXrHwMyjgvBuf1L76s=; b=oqizcsij63C6NXeRVVEkR7Doh/PFv05NeCYBOCPdMUUlY3On2GLZ3KociM+KO6ucHV mCePLsCXh2gWzrnSfmX8N5SKmXFKc2ZJU+Gt4ph8mGCGhFtcgHWaXZR9D0JYa6Y+J1Q8 cr3Xct7sYRH2Zf15/dxPX3866Ze6FZSLWqiPF7eziO/LDKiY40QDcMSfZYFoyxY0XtDO G3miq7SIcXM6yv0BzXtsYYrPd0fcacwgVWPa7MuU+1e9ka6FB2JVECYwounsUzRrJslU e8EzF264DWUyDBb2w1uI+SbLnacPx4BTjXpb+eISCvZ7K9SCSTH8IaMe9mgTP0j4+fhY fOVw== 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=dJkaM6IVIjTDs+j8XZYHGWupMlXrHwMyjgvBuf1L76s=; b=mUfP53G62z8VoX3gxofBm8qDmudVD1dWD8M4ZMfX0gNyyV0isYUxH4gMKlJsOnfTpH jj80BSbY3MuCVqy1yvXa1llVfhXNlzk512E2+nLkTK3b2BKi2MiRmYo7EZCZJb+D1t5y 6XALMZ92tfqAQr4Cpo+W/DPBD5oNpK6992lWkknX/rBiHzZ80ZL6q+gH4iIb1BzLqVz+ qtJFUMQLjy4OOS3a2a9J8AuImRfIeD4C8XpnEpmkWUAAlh3o8JEcmblMreN7ugBNXTEJ 69rXAH2cNAIpCO49sa4zYXDHKiYOMIokXmRKFKgmMwpy/ZdWdy8YgNNzW7Lnj0i6n02W cbiw== X-Gm-Message-State: AKwxytc3XcRn6Bxgaw8t/sjYbYS+PYXWE+vAwp3OKgp+9yW039s3RJJs tqjZ9fCt2qot0tgRUXND+F3XvE57nH6r/NhrZjQ= X-Google-Smtp-Source: AH8x225qrWdl7NZ22BBauZ/6ffxaQNtxv6a0X3aJLDiaomh9iOy+pNQuRqnOZ6lX2Nd4KXQBPYtu4yjlFEyxQ/LbPxQ= X-Received: by 10.99.6.72 with SMTP id 69mr9403628pgg.50.1516755931392; Tue, 23 Jan 2018 17:05:31 -0800 (PST) MIME-Version: 1.0 Received: by 10.100.163.169 with HTTP; Tue, 23 Jan 2018 17:05:30 -0800 (PST) In-Reply-To: References: <20180123145453.GA1916@Magus.localnet> From: Chet Murthy Date: Tue, 23 Jan 2018 17:05:30 -0800 Message-ID: To: Jeremy Yallop Cc: Oleg , Caml List Content-Type: multipart/alternative; boundary="001a114f5ef4806f2205637b422b" Subject: Re: [Caml-list] Are record types generative? --001a114f5ef4806f2205637b422b Content-Type: text/plain; charset="UTF-8" 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. > I'm no longer a type-theorist, so I don't have the knowledge to answer, but: 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) == V'. Where's I'm abusing notation, b/c "-eval->" means in the first case "evaluation on typed programs" and in the second, "evaluation on untyped programs" which might be entirely different things. This was the (famous amongst that admittedly tiny community) "commuting rectangles type erasure property". 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 support reflection, and when they support object-orientation, they don't support "instanceof" (e.g. like Java's). because these require that compile-time type-information be present at runtime. 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- can easily be programmed in such a way that I can understand the runtime behaviour 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 particular JVM implementation -- one is using. --chet-- --001a114f5ef4806f2205637b422b Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable


On Tue, Jan 23, 2018 at 2:06 PM, Jeremy Yallop <yallop@gmail.com>= ; 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?=C2=A0 There are far
fewer programs that violate that property, I think.

I'm no longer a type-theorist, so I don't have the kn= owledge to answer, but:

It was a critically important property of *all* the origi= nal MLs (and of the theoretical development of ML) that a well-type ML prog= ram P could be "type-erased" to an untyped program TE(P); then wh= en P -eval-> V, and TE(P) -eval-> V', TE(V) =3D=3D V'.=C2=A0 = Where's I'm abusing notation, b/c "-eval->" means in t= he first case "evaluation on typed programs" and in the second, &= quot;evaluation on untyped programs" which might be entirely different= things.

This was the (famous amongst that admittedly tiny community) "commu= ting rectangles type erasure property".

A -concrete- effect of this property= in MLs (again, I'm no longer a type-theorist, so I might be getting th= is wrong) is ML-family languages don't support reflection, and when the= y support object-orientation, they don't support "instanceof"= (e.g. like Java's).=C2=A0 because these require that compile-time type= -information be present at runtime.

For those who think this is a bad design choi= ce, I can only say that as a systems-jock, I appreciate a language that is = -so- high-level, and -yet- can easily be programmed in such a way that I ca= n understand the runtime behaviour in terms of a C-like runtime model.=C2= =A0 By contrast, to understand Java *for real* one must have enormously det= ailed knowledge of the JVM -- the particular JVM implementation -- one is u= sing.

= --chet--

--001a114f5ef4806f2205637b422b--