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 AD34F820A1 for ; Sun, 11 Aug 2013 16:56:17 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.149; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.149; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of postmaster@ppsw-42.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.149; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-42.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: ApYBACelB1KDbwiVnGdsb2JhbABZwmuBLQ4BAQEBAQYNCQkUKIIkAQEEAScTOAcQCyElDwEESYgdBgStVYgHFpAlB4QRA54MjkU X-IPAS-Result: ApYBACelB1KDbwiVnGdsb2JhbABZwmuBLQ4BAQEBAQYNCQkUKIIkAQEEAScTOAcQCyElDwEESYgdBgStVYgHFpAlB4QRA54MjkU X-IronPort-AV: E=Sophos;i="4.89,856,1367964000"; d="scan'208";a="23714400" Received: from ppsw-mx-f.csi.cam.ac.uk (HELO ppsw-42.csi.cam.ac.uk) ([131.111.8.149]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 Aug 2013 16:56:17 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from [31.55.118.129] (port=41865 helo=netbook) by ppsw-42.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.159]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1V8X44-0003Kj-6b (Exim 4.80_167-5a66dd3) (return-path ); Sun, 11 Aug 2013 15:56:16 +0100 From: Leo White To: Andreas Rossberg Cc: David Sheets , Caml List References: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> <9D61A8E2-D0B4-452A-B372-401E499423AE@mpi-sws.org> X-Face: "XWxb[u_Z\PA_Y?9@|IA!!+jTb(/290-*ea/Un$I0B98.$n%eL.;2w*,z]WR#T:,p[ NBd++M7l]#7zj7!{~iw $W-"/=|dVjhT[D{4~gE}gK<2`.6fs!;uqqud]vs2N/3^m7{aS1V, Date: Sun, 11 Aug 2013 15:58:34 +0100 In-Reply-To: <9D61A8E2-D0B4-452A-B372-401E499423AE@mpi-sws.org> (Andreas Rossberg's message of "Sun, 11 Aug 2013 16:32:33 +0200") Message-ID: <86bo549sv9.fsf@cam.ac.uk> User-Agent: Gnus/5.13 (Gnus v5.13) Emacs/23.4 (gnu/linux) MIME-Version: 1.0 Content-Type: text/plain; charset=us-ascii Subject: Re: [Caml-list] First-class Functor Forgetting for Free >>> There is no implicit subtyping in OCaml's core language. The reason for that is not code generation, but type inference. For example, what type should the following function be given if the subtyping you ask for could apply? >>> >>> let g x = let module X = (val x : D) in X.(f x) >> >> Something like val g : [< (module D)] or simply val g : (module D) >> where the type constraint relation is implicit seems reasonable. I >> don't know if you consider polymorphic variant types as part of the >> core language (or perhaps they aren't implicit because they propagate >> inequalities?). > > I don't think type inference for polymorphic variants works the way you think it does. Inference for both variants and objects is based on row polymorphism, not subtyping. A type like [< A] is actually a polymorphic type with a hidden type variable, not a subtype bound, even though the surface syntax intentionally hides that fact (which isn't always helpful). Module signatures are totally different beasts, where matching _is_ a form of subtyping. I think David is suggesting that "with-constraints" on first-class modules could be handled with row polymorphism, and I don't know of any reason why they couldn't. It would certainly be a more flexible way to type them. So, let g x = let module X = (val x : D) in X.(f x) would have a type: (module D with ..) -> int and something like: module type S = sig type t type s val x: t val y: s end let h (module X : S) = X.x could have type: (module S with type t = 'a and ..) -> 'a (which I also think should be expressable as "(module X : S) -> X.t" ) Regards, Leo