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 E86C6820A2 for ; Mon, 12 Aug 2013 18:45:06 +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.132; 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.132; 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-32.csi.cam.ac.uk) identity=helo; client-ip=131.111.8.132; receiver=mail2-smtp-roc.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: Am8CAKgQCVKDbwiElGdsb2JhbABbwl+BGhYOAQEBAQkLCQkUBSOCJAEBAQMBOj8FCwshJQ8BBEmIHQYErl2IBxaQJQeEEQOUDYl/jkU X-IPAS-Result: Am8CAKgQCVKDbwiElGdsb2JhbABbwl+BGhYOAQEBAQkLCQkUBSOCJAEBAQMBOj8FCwshJQ8BBEmIHQYErl2IBxaQJQeEEQOUDYl/jkU X-IronPort-AV: E=Sophos;i="4.89,863,1367964000"; d="scan'208";a="29161951" Received: from ppsw-32.csi.cam.ac.uk ([131.111.8.132]) by mail2-smtp-roc.national.inria.fr with ESMTP; 12 Aug 2013 18:45:06 +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=35662 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 1V8vE4-00049w-1G (Exim 4.80_167-5a66dd3) (return-path ); Mon, 12 Aug 2013 17:45:06 +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> <867gfrndl0.fsf@cam.ac.uk> <52090871.8090400@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 17:46:31 +0100 In-Reply-To: <52090871.8090400@mpi-sws.org> (Andreas Rossberg's message of "Mon, 12 Aug 2013 18:08:17 +0200") Message-ID: <861u5yoo0o.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 > Your row variables will inevitably be higher-order, AFAICS. > I don't think they will be. To be higher order wouldn't they need to have parameters? I don't see how they could end up with parameters. Looked at another way, package types are essentially a pair of a module type and a set of with-constraints. The row variables would simply stand for these same sets of with-constraints. Just as the package type is not higher order neither would the row variables be. > > I don't think that there would be any higher-order unification involved in this example, because you'd only unify the > RHSs, which are ground, and all unification variables would still be ground as well. I'm less convinced that the same > can be assumed about unification with row variables for constraints (although it could be). > I don't see how row variables could possibly affect this. > > I disagree completely. Packages wrap modules, so package types _are_ module types. The point of package types is to > embed module types into the core type system, not to create a parallel module type system. I think it would be a real > bad idea to invent a separate typing mechanism for this purpose, since that is bound to create complexity, friction, and > confusion. > I also disagree completely. Packages wrap modules, so package types _wrap_ module types. The core type system provides mechanisms that are not available in the module type system. We should not rule out using these mechanisms with package types to make then easier to use. Embeding module types into the core type system should mean allowing the mechanisms provided by the core type system to operate on module types, not just allowing the core type system to treat module types as black-boxes that can be passed around and given back to the module system. Regards, Leo