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 0EDF6820A1 for ; Mon, 12 Aug 2013 17:14:58 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=pra; client-ip=131.111.8.149; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of lpw25@cam.ac.uk) identity=mailfrom; client-ip=131.111.8.149; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="lpw25@cam.ac.uk"; x-conformance=sidf_compatible Received-SPF: None (mail2-smtp-roc.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=mail2-smtp-roc.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: Au4BAIz7CFKDbwiVnGdsb2JhbABbwl+BLw4BAQEBAQYNCQkUKIIkAQEEATo/BQsLGAklDwEESROICgYErkqIBxaQJQeEEQOUDYl/jkU X-IPAS-Result: Au4BAIz7CFKDbwiVnGdsb2JhbABbwl+BLw4BAQEBAQYNCQkUKIIkAQEEATo/BQsLGAklDwEESROICgYErkqIBxaQJQeEEQOUDYl/jkU X-IronPort-AV: E=Sophos;i="4.89,862,1367964000"; d="scan'208";a="29154015" Received: from ppsw-mx-f.csi.cam.ac.uk (HELO ppsw-42.csi.cam.ac.uk) ([131.111.8.149]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Aug 2013 17:14:57 +0200 X-Cam-AntiVirus: no malware found X-Cam-ScannerInfo: http://www.cam.ac.uk/cs/email/scanner/ Received: from [109.144.151.170] (port=40527 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 1V8tpg-0005xc-8E (Exim 4.80_167-5a66dd3) (return-path ); Mon, 12 Aug 2013 16:14:56 +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> <86bo549sv9.fsf@cam.ac.uk> <5208C0A7.2040906@mpi-sws.org> <86haevnnr5.fsf@cam.ac.uk> <5208D1EF.5050302@mpi-sws.org> <86bo53njmc.fsf@cam.ac.uk> <5208EE0D.3000507@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: Mon, 12 Aug 2013 16:17:15 +0100 In-Reply-To: <5208EE0D.3000507@mpi-sws.org> (Andreas Rossberg's message of "Mon, 12 Aug 2013 16:15:41 +0200") Message-ID: <867gfrndl0.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 Andreas Rossberg writes: > On 08/12/2013 03:06 PM, Leo White wrote: >>> >>> With constraints generally map _type paths_ to _type constructors_. >> >> OCaml doesn't allow deep with-constraints (e.g. with type M.t = foo) so >> they are actually mappings from names. > > That's not correct. It has been supported since 4.0 (IIRC). > Somehow I managed to miss that change. It should probably be added to the manual. >>> (Mind you, OCaml doesn't currently allow revealing type constructors in package types, but that is a limitation >>> that seems much more important to lift than what we are discussing here.) >> >> Allowing type constructors to be revealed by package types would >> complicate things, but I don't think it would be hard to >> accomodate. There is a fairly obvious analogy between: >> >> (module S with type 'a t = 'a list and ..) >> >> and >> >> < t: 'a. 'a list; .. > > > No, that's not the same at all. One is a quantified type, the other a parameterised type (constructor). When you allow > higher-order type variables, you get into the business of higher-order unification, which is complicated, and > undecidable in the general case. You'd need to investigate very carefully what restrictions to impose to avoid being > pulled down that rabbit hole. I think The required type-checking is quite similar for these two cases, although the comparison is possibly not that useful. Note that I have not suggested adding any higher-order type variables. This is besides the point anyway, as this problem is entirely orthogonal to the addition of row polymorphism. If you want to allow revealing type constructors in package types then you need to solve this issue. For example, type-checking this: let f (x: (module S with type 'a t = 'a foo * 'b)) (y: (module S with type 'a t = 'a bar * int)) = [x; y];; requires you to know how to unify: module S with type 'a t = 'a foo * 'b with module S with type 'a t = 'a bar * int > > OK, I see. But all that would make package typing even more ad-hoc, and divorce its semantics from that of proper > signatures and signature matching even more. I disagree. The point of a package type is to ensure that the module type that the package was packed with matches the module type that the package is unpacked with. There is no reason to assume that this is best done by a carbon copy of the module types. Row polymorphism would make first-class modules significantly less awkward to use (in the same way that it makes objects significantly less awkward to use). If anything it would be less ad-hoc than the current system, which uses forward type propagation to try to infer the correct with-constraints for a package expression. > That's the opposite of the direction I'd like the package feature to go. It > would be fairly hostile to future generalisations of packages. Again, I disagree. I see no reason that it would be hostile to future generalisations. Do you have anything particular in mind? > So, yes, perhaps you could make something work along the lines you sketch, assuming enough restrictions are in > place. But the price seems way too high for the minor convenience it provides. Wouldn't you agree? I don't think that any restrictions are needed, so obviously I don't agree that there is a high price. Regards, Leo