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 F0CF182355 for ; Tue, 23 Jan 2018 22:36:40 +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=3AJqi91h3T33nvvjT5smDT+DRfVm0co7zxezQtwd8Z?= =?us-ascii?q?se0TLfad9pjvdHbS+e9qxAeQG9mDsrQc06L/iOPJYSQ4+5GPsXQPItRndiQuro?= =?us-ascii?q?EopTEmG9OPEkbhLfTnPGQQFcVGU0J5rTngaRAGUMnxaEfPrXKs8DUcBgvwNRZv?= =?us-ascii?q?JuTyB4Xek9m72/q99pHPfglEniaxba9vJxiqsAvdsdUbj5F/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+ksDwHG0xI8H9kTt3?= =?us-ascii?q?rUsc/1NLsSUeG10aLFyjDDb+5M2Tfh6IjJcgotru2MXb1ubcrc0kYvFwbfgVWR?= =?us-ascii?q?rYzpJS+a1uMIs2WC6edrSOGhi3Y/pg1vvjSiwt0gh4rJi44P11zJ8Tt1zJwoKd?= =?us-ascii?q?C6TEN2Z8OvHoFKuCGALYR2R9svQ2F2tyY+zb0LoZu7czILyJQj3hLfc/KHf5SR?= =?us-ascii?q?7hLtSeqcIzN1iGhqeLK4gBay/kygxfPmWsao11ZKqzJJktjKtn8Tyxze8taLRu?= =?us-ascii?q?d580u72juC1xrf5vxALEwqj6bXNpwsz7oompoWq0vDHyv2mEvsjK+Rc0Up4u2o?= =?us-ascii?q?6/n9YrX6pp+dN5V4hR3+MqswhsyyGus4Mg0UUGia/eSwzqHs/Ur8QLlSlP05jr?= =?us-ascii?q?HZsIzGJcQcvqO2HxVa0oMn6xqmCzem0c8YnWUcIVJeeBOHipDpNEvULPD5C/e/?= =?us-ascii?q?mVWsny1xy/DIJL2ySqnKe1rOirrkbP5M4kpYzxJ7mcFW45ZTEpkOJfvyXgn6s9?= =?us-ascii?q?mOXTEjNAnh6ObqFJ1Yy5kCWXPHVqqEKr/SoBmD5u8zC+aJbY4R/j36Lq52tLbV?= =?us-ascii?q?kXYllApFLuGS1pwNZSX9R6w+ehTLUT/Xmt4EVFwykE87Re3uhkeFVGcKNXm3Vq?= =?us-ascii?q?M4oDo8DdD/VNuRdsWWmLWEmRyDMNhOfGkfUwKDFH7pc8OPXPJeMHvPcP8kqSQN?= =?us-ascii?q?UP2ac6Fk1Ryqs1Wkmb9uL+6R4iNA8Jy6i4kz6OrUmhU/szdzCpbF3g=3D=3D?= X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: =?us-ascii?q?A0C1BABcqmdahrPAVdFeHAEBAQQBAQoBA?= =?us-ascii?q?YUcFBMHg1aBOZdQggKEAZNSggIKhTsChG8HGQcENBQBAQEBAQEBAQEBARIBAQE?= =?us-ascii?q?ICwsIKC+COCQBgkYBAQEDASMEGQEbHQEDAQsGBQQHDSoCAiEBAREBBQEcBhOKH?= =?us-ascii?q?AEDDQimYECME4FtGAUBHIMLBYNmChknDVmCJAEBAQEBBQEBAQEBAQEZAgYShDm?= =?us-ascii?q?CFYM/gy6Ca0QEgVeDL4JlBYp0iFVgjxg9kFiFBXSTL44aiSIUBSCBFzaBcjMaI?= =?us-ascii?q?1IygXiCRQ8QDIIIIDeOGgEBAQ?= X-IPAS-Result: =?us-ascii?q?A0C1BABcqmdahrPAVdFeHAEBAQQBAQoBAYUcFBMHg1aBOZd?= =?us-ascii?q?QggKEAZNSggIKhTsChG8HGQcENBQBAQEBAQEBAQEBARIBAQEICwsIKC+COCQBg?= =?us-ascii?q?kYBAQEDASMEGQEbHQEDAQsGBQQHDSoCAiEBAREBBQEcBhOKHAEDDQimYECME4F?= =?us-ascii?q?tGAUBHIMLBYNmChknDVmCJAEBAQEBBQEBAQEBAQEZAgYShDmCFYM/gy6Ca0QEg?= =?us-ascii?q?VeDL4JlBYp0iFVgjxg9kFiFBXSTL44aiSIUBSCBFzaBcjMaI1IygXiCRQ8QDII?= =?us-ascii?q?IIDeOGgEBAQ?= X-IronPort-AV: E=Sophos;i="5.46,403,1511823600"; d="scan'208,217";a="310360263" Received: from mail-pf0-f179.google.com ([209.85.192.179]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES128-GCM-SHA256; 23 Jan 2018 22:36:39 +0100 Received: by mail-pf0-f179.google.com with SMTP id p1so1353382pfh.4 for ; Tue, 23 Jan 2018 13:36:39 -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=Ngpb2FIga6QwhVi5wva2Wmev8if7xWM+/y3sgWqTGT4=; b=NInogawQ/DpciURZbq2IuHzeJSdZL8nF+1ZtqXo2pameF9AZu55oNo07gJaiJsR335 Nb1QBnf4SoWsBRQYQWUCrgQYpAykVAL3oSFHfi61WYSE5fJagFcZcOPIYIbbqxxaWBNy tuyMrpwinngZ6kp5+Spd8LhcakhrO9X4g2D7BBuNsOyqigGCEfGpLdfSvN+4Nv8Fep4G G2E6gEs+CjMtDI1RUOYtby7H6TT3V3UetFUOXk+jPLOkF/99GEHKTvtA+1OvLwhC7C3O XvTjED9LECIBmRPgHSJyo7NfGaUvl/EJ7PjOy7Wt0iLHIcZrqoEgh8idb5+1HAHRWeHc FBzg== 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=Ngpb2FIga6QwhVi5wva2Wmev8if7xWM+/y3sgWqTGT4=; b=N2JLIETKgYu07uZhr5uuPof5XNzNGwUxTokRimDQZG5jB8CUpE63mTvUpm6L0KiXcO 24YewSx8ngnp+gSGKuPiUqFcIGeD+v90JnJTtPnEnIzM3UmudKNkMF50cL1NaxZJVzAJ zwZReWASCgHEv0MEpwHAUPOH65JiE+K7JakxPeMGjYoF3rM+CyvYKx8nb4xnwbsHVVkM 9WvAG7kRgrht2iqBC7kT8T3yplpvVod+mCSPzZci5YkgBcWiL9poIIuoKtMhwsWJxaUr qra/lI/HFeKZkjwMtJcHETipvdQmbO+KABj6WhfPCESYCLyLXl0FZO6telVenvTYq5pf QmdQ== X-Gm-Message-State: AKwxyte5LhAs31lwq91OBhW96IC4H9UxtHb4kUkkg+BXLwMKP2m+pb9G 5uGh1oKazOI5aCKFYc/RN8G2NzJSC2zppHgYWGA= X-Google-Smtp-Source: AH8x225q8T4iEZpy73ssPXML2A4ycbWr0itCXqDaMZS5U0nbsIWW6F8T2tzaY+7Ui7WeU/6MMHTo7YI3KocRDTfZ7jI= X-Received: by 10.101.87.132 with SMTP id b4mr9338942pgr.332.1516743397748; Tue, 23 Jan 2018 13:36:37 -0800 (PST) MIME-Version: 1.0 Received: by 10.100.163.169 with HTTP; Tue, 23 Jan 2018 13:36:37 -0800 (PST) In-Reply-To: References: <20180123145453.GA1916@Magus.localnet> From: Chet Murthy Date: Tue, 23 Jan 2018 13:36:37 -0800 Message-ID: To: Jeremy Yallop Cc: Oleg , Caml List Content-Type: multipart/alternative; boundary="089e082303b07035bd0563785705" Subject: Re: [Caml-list] Are record types generative? --089e082303b07035bd0563785705 Content-Type: text/plain; charset="UTF-8" Heh. I was careful to say "caml", not "ocaml". I'm aware that polymorphic variants, objects, and (heh, I forgot) labels all violate the rule. And of course, modules do. Like I said: *caml* has this property. Certainly caml-light, circa 1993 did, IIRC. I remember having a nice discussion with Pierre Weis, where I asked him why record-labels were generative, and he pointed this out to me. --chet-- On Tue, Jan 23, 2018 at 12:35 PM, Jeremy Yallop wrote: > On 23 January 2018 at 17:39, Chet Murthy wrote: > > That is, when you write a caml program and it fails to type-check, you > can't make it type-check by adding "enough" type-annotations. > > This hasn't been the case for a long time (perhaps ever), and it's > becoming less true with each release. For example, all of the > following programs pass type checking as written, but are rejected if > the annotations are removed: > > (* 1 *) let f (g : x:int -> y:int -> int) x y = (g ~x ~y, g ~y ~x) > (* 2 *) let rec f : 'a. 'a -> unit = fun x -> ignore (f 3, f "four") > (* 3 *) let f : [`A] -> unit = function `A -> () | _ -> . > (* 4 *) module type S = module type of struct let r : int list > ref = ref [] end > (* 5 *) let f (o : unit>) = (o#m (), o#m 2) > (* 6 *) let f z = let rec x = [| y; z |] and y : int = z in x > (* 7 *) let x : _ format6 = "%d" in Printf.sprintf x > (* 8 *) type a = A | B type b = A let x = (A : a) = B > (* 9 *) let f : (module S) = (module struct end) > (* 10 *) module rec M : module type of struct let f : int -> int = > assert false end = struct let f = M.f end > --089e082303b07035bd0563785705 Content-Type: text/html; charset="UTF-8" Content-Transfer-Encoding: quoted-printable
Heh. I was careful to say "caml", not "ocam= l".=C2=A0 =C2=A0I'm aware that polymorphic variants, objects, and = (heh, I forgot) labels all violate the rule. And of course, modules do.
Like I said: *caml* has this property.=C2=A0 Certainly caml= -light, circa 1993 did, IIRC.

I remember having a = nice discussion with Pierre Weis, where I asked him why record-labels were = generative, and he pointed this out to me.

--chet-= -


On Tue, Jan 23, 2018 at 12:35 PM, Jeremy Yallop <yallop@gmail.co= m> wrote:
= On 23 January 2018 at 17:39, Chet Murthy <murthy.chet@gmail.com> wrote:
> That is, when you write a caml program and it fails to type-check, you= can't make it type-check by adding "enough" type-annotations= .

This hasn't been the case for a long time (perhaps ever), and it= 's
becoming less true with each release.=C2=A0 For example, all of the
following programs pass type checking as written, but are rejected if
the annotations are removed:

=C2=A0 =C2=A0(* 1 *)=C2=A0 =C2=A0let f (g : x:int -> y:int -> int) x = y =3D (g ~x ~y, g ~y ~x)
=C2=A0 =C2=A0(* 2 *)=C2=A0 =C2=A0let rec f : 'a. 'a -> unit =3D = fun x -> ignore (f 3, f "four")
=C2=A0 =C2=A0(* 3 *)=C2=A0 =C2=A0let f : [`A] -> unit =3D function `A -&= gt; () | _ -> .
=C2=A0 =C2=A0(* 4 *)=C2=A0 =C2=A0module type S =3D module type of struct le= t r : int list
ref =3D ref [] end
=C2=A0 =C2=A0(* 5 *)=C2=A0 =C2=A0let f (o : <m:'a.'a -> unit&= gt;) =3D (o#m (), o#m 2)
=C2=A0 =C2=A0(* 6 *)=C2=A0 =C2=A0let f z =3D let rec x =3D [| y; z |] and y= : int =3D z in x
=C2=A0 =C2=A0(* 7 *)=C2=A0 =C2=A0let x : _ format6 =3D "%d" in Pr= intf.sprintf x
=C2=A0 =C2=A0(* 8 *)=C2=A0 =C2=A0type a =3D A | B=C2=A0 =C2=A0type b =3D A= =C2=A0 =C2=A0let x =3D (A : a) =3D B
=C2=A0 =C2=A0(* 9 *)=C2=A0 =C2=A0let f : (module S) =3D (module struct end)=
=C2=A0 =C2=A0(* 10 *) module rec M : module type of struct let f : int ->= ; int =3D
assert false end =3D struct let f =3D M.f end

--089e082303b07035bd0563785705--