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 0F6D6820A1 for ; Mon, 12 Aug 2013 18:08:23 +0200 (CEST) Received-SPF: None (mail2-smtp-roc.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail2-smtp-roc.national.inria.fr: domain of rossberg@mpi-sws.org designates 139.19.1.49 as permitted sender) identity=mailfrom; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; 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@hera.mpi-klsb.mpg.de) identity=helo; client-ip=139.19.1.49; receiver=mail2-smtp-roc.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="postmaster@hera.mpi-klsb.mpg.de"; x-conformance=sidf_compatible X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnoCAD8HCVKLEwExgGdsb2JhbABbDsJRgRkWDgEBCwcECQkUBSOCJAEBAQMBOAgBATYBAQQLCw4KCRYPCQMCAQIBIwUdBg0BBQIBAYgGBplGiwyERwEFjUMGkDsHhBGUEIl/jgZA X-IPAS-Result: AnoCAD8HCVKLEwExgGdsb2JhbABbDsJRgRkWDgEBCwcECQkUBSOCJAEBAQMBOAgBATYBAQQLCw4KCRYPCQMCAQIBIwUdBg0BBQIBAYgGBplGiwyERwEFjUMGkDsHhBGUEIl/jgZA X-IronPort-AV: E=Sophos;i="4.89,863,1367964000"; d="scan'208";a="29158768" Received: from hera.mpi-klsb.mpg.de ([139.19.1.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 12 Aug 2013 18:08:22 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=Content-Transfer-Encoding:Content-Type:In-Reply-To:References:Subject:CC:To:MIME-Version:From:Date:Message-ID; bh=yVbtOtNK2ECf/Y3mRixDfd2n6bngkHXx+dg08vTY2ws=; b=RnnG9MK1nU89PUEhX7XRJAwVQyOxEGa8lchRuQR2hpkIK6xRv8zfyTA1x77ZrF2fjfXTvc7lvgmu0xgA7oQHBtsS6n4hs3p51bndoGZdpGQR5FROA0AM5RhfPUB45ro07Z9/jFZG4bKfloK7/6yOJrZoHbfiiQjAPhBOdHFbzgo=; Received: from srv-00-126.mpi-klsb.mpg.de ([139.19.1.29]:55119 helo=zak.mpi-klsb.mpg.de) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8ufK-0003Cd-Bf; Mon, 12 Aug 2013 18:08:20 +0200 Received: from [74.125.57.233] (port=2645 helo=bozo.muc.corp.google.com) by zak.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:DHE_RSA_AES_256_CBC_SHA1:32) (Exim 4.72) id 1V8ufJ-0005In-TK; Mon, 12 Aug 2013 18:08:17 +0200 Message-ID: <52090871.8090400@mpi-sws.org> Date: Mon, 12 Aug 2013 18:08:17 +0200 From: Andreas Rossberg User-Agent: Mozilla/5.0 (X11; Linux x86_64; rv:17.0) Gecko/20130804 Thunderbird/17.0.8 MIME-Version: 1.0 To: Leo White 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> In-Reply-To: <867gfrndl0.fsf@cam.ac.uk> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-MPI-Local-Sender: true Subject: Re: [Caml-list] First-class Functor Forgetting for Free On 08/12/2013 05:17 PM, Leo White wrote: > Andreas Rossberg writes: >> On 08/12/2013 03:06 PM, Leo White wrote: >>>> (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. I'm not sure what you mean, impredicativity and higher-orderness are different dimensions in the type system space, with different properties. Your row variables will inevitably be higher-order, AFAICS. > 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 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). That said, I wasn't aware that OCaml actually allows unification variables in package constraints. I am not sure that's a wise design choice. It's a way of painting yourself into a corner with the type system, because it could make the generalisation to a more complete signature language for package types hard or impossible. Moreover, I'm not aware of any work investigating the formal implications it has. All you _should_ need to check when unifying package types is that both denote equivalent signatures (i.e., mutual subtypes). I strongly believe that you do not want unification to be required for matching type components. (With local modules, it may be needed for matching value components, but that is fine.) >> 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. 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. > 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? Well, obviously, anything you can express with module signatures should be possible in package types. Ideally, the syntax would just be (module ), reusing the expressiveness you already have, and with a consistent semantics. >> 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. You assume the current syntax, which already is highly restricted. Also, the price involves the added complexity, too. Seems quite significant to me. ;) /Andreas