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 67BCC820A1 for ; Mon, 12 Aug 2013 16:15:51 +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: AkkCAEHtCFKLEwExgGdsb2JhbABaDsJRgS8OAQELBwQJCRQFI4IkAQEBAwEnEQgBATYBAQQLCw4KCRYPCQMCAQIBIwUdBg0BBwEBiAYGmSGLDIRHAQWNPQaQOweEEZQQiX+OBkA X-IPAS-Result: AkkCAEHtCFKLEwExgGdsb2JhbABaDsJRgS8OAQELBwQJCRQFI4IkAQEBAwEnEQgBATYBAQQLCw4KCRYPCQMCAQIBIwUdBg0BBwEBiAYGmSGLDIRHAQWNPQaQOweEEZQQiX+OBkA X-IronPort-AV: E=Sophos;i="4.89,862,1367964000"; d="scan'208";a="29148513" Received: from hera.mpi-sb.mpg.de (HELO hera.mpi-klsb.mpg.de) ([139.19.1.49]) by mail2-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 12 Aug 2013 16:15:50 +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=2OkFhyGU2hYdjAXHADTGQS+7tEpHxBgYvQR33FLM+T0=; b=xG9BMAWw/NRGxYGYYMiQXOLAkNR4SMdz4baTICt3n1Qv+l6G56N3GX8PH7Mfzz6zcPpN+QzUY+5NKdd0gUq8D2E3MTwh9PThZeb/YSNxFNb/Xm8dnL3XftECUzcTMZ/TL02pCf3s3C9KIxEm+66v/eqS8375GQy3c+Gs8BSSTec=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:53066) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8suM-0001ZA-U8; Mon, 12 Aug 2013 16:15:48 +0200 Received: from [74.125.57.233] (port=47967 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 1V8suM-0004Bb-G7; Mon, 12 Aug 2013 16:15:42 +0200 Message-ID: <5208EE0D.3000507@mpi-sws.org> Date: Mon, 12 Aug 2013 16:15:41 +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> In-Reply-To: <86bo53njmc.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 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). > Even if they were mappings from > paths, paths are still simple labels. Only if you squint real hard, IMHO. > 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. I've heard things like "fairly easy" far too often in contexts like this. ;) >> (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. > 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 .. 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. 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. 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? /Andreas