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 10B08820A1 for ; Mon, 12 Aug 2013 15:04:41 +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.132; 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.132; 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-32.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.132; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="lpw25@cam.ac.uk"; x-sender="postmaster@ppsw-32.csi.cam.ac.uk"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Am8CABvcCFKDbwiElGdsb2JhbABawl+BGhYOAQEBAQcNCQkUBSOCJAEBAQMBJxM/BQsLISUPAQRJiB0GBK4GiAcWkCUHhBEDngyORQ X-IPAS-Result: Am8CABvcCFKDbwiElGdsb2JhbABawl+BGhYOAQEBAQcNCQkUBSOCJAEBAQMBJxM/BQsLISUPAQRJiB0GBK4GiAcWkCUHhBEDngyORQ X-IronPort-AV: E=Sophos;i="4.89,862,1367964000"; d="scan'208";a="23773308" Received: from ppsw-32.csi.cam.ac.uk ([131.111.8.132]) by mail3-smtp-sop.national.inria.fr with ESMTP; 12 Aug 2013 15:04:39 +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=35347 helo=netbook) by ppsw-32.csi.cam.ac.uk (smtp.hermes.cam.ac.uk [131.111.8.156]:587) with esmtpsa (PLAIN:lpw25) (TLSv1.2:DHE-RSA-AES128-SHA:128) id 1V8rnY-0001mv-2S (Exim 4.80_167-5a66dd3) (return-path ); Mon, 12 Aug 2013 14:04:37 +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> 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 14:06:51 +0100 In-Reply-To: <5208D1EF.5050302@mpi-sws.org> (Andreas Rossberg's message of "Mon, 12 Aug 2013 14:15:43 +0200") Message-ID: <86bo53njmc.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 > > 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. Even if they were mappings from paths, paths are still simple labels. The with-constraints in package types map to types not type constructors, as evidenced by the existence of types like: (module D with type t = 'a) -> 'a > Moreover, the domain of type paths is bounded by > what actually occurs in the signature. I don't think that row polymorphism has particular difficulty with such bounding. Consider the type: [< `Foo of int | `Bar of float > `Foo] this type contains a row variable (well something very similar to a row variable) that is quite constrained in how it can be instanciated. This essentially involves to a simple kind system that is hidden from the programmer. I think a similar approach would be fairly easy for with-constraints, each module type would basically entail the existance of a kind of row variable. > (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; .. > > More importantly, unlike for rows, not listing a type in a constraint doesn't mean that it's absent. It means that it is > kept abstract. That's quite different, and it would require some notion of implicit existential type introduction based > on the instantiation, for which I have no idea how it should work. Some form of skolemisation perhaps? How does that > integrate with the rest of core typing and inference? Type inference with existentials is known to be very tricky. I don't think this is correct. Not listing a "with-constraint" on a package type *does* mean that the "with-constraint" is absent. Certainly, unpacking a first-class module introduces an abstract type if there is no "with-constraint" on the module type that it is being unpacked with. But the module type that it is unpacked under, and the package type that it has are *not* the same thing. To be clear, I am only proposing the existence of row types for first-class modules not for module types in general. So the following code: let module M = (val x : S) in .. would give module M the module type `S`, but unify the type of `x` with `(module S with ..)`. Similarly, let module M = (val x : S with type t = int) in .. would give module M the module type `S with type t = int`, and unify the type of `x` with `(module S with type t = int and ..)`. But the following would be invalid: let module M = (val x : S with type t = int and ..) in .. > I also wouldn't know how exactly the row idea ties in with signature matching. What does (S with ..) < S mean? The only > interpretation I can see is by expanding ".." into a list of equations for all types abstract in S -- but that would > notably _not_ be a row-polymorphic interpretation. As I said above, I am only proposing the row types for the package types, not for actual module types. `(S with ..) < S` could not arise (which is good because I agree that it is nonsense). > Hope those are enough open questions for now. :) Thank you for the list :). Obviously I have only outlined why I don't think those questions would be difficult to address. To be sure that it would work someone would need to have a more formal look at giving it a static semantics. But I still don't see any reason why we could not use row-polymorphism for the with-constraints of package types. Regards, Leo