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 4E17B820A1 for ; Mon, 12 Aug 2013 14:15:52 +0200 (CEST) Received-SPF: None (mail3-smtp-sop.national.inria.fr: no sender authenticity information available from domain of rossberg@mpi-sws.org) identity=pra; client-ip=139.19.1.49; receiver=mail3-smtp-sop.national.inria.fr; envelope-from="rossberg@mpi-sws.org"; x-sender="rossberg@mpi-sws.org"; x-conformance=sidf_compatible Received-SPF: Pass (mail3-smtp-sop.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=mail3-smtp-sop.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 (mail3-smtp-sop.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=mail3-smtp-sop.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: AnoCAF3RCFKLEwExgGdsb2JhbABaDsJRgRoWDgEBCwcECQkUBSOCJAEBAQQnEQgBATYBAQ8LDgoJFg8JAwIBAgEjBR0GDQEHAQGIDJhxiwyERwEFjTQGkDsHhBGeD44GQA X-IPAS-Result: AnoCAF3RCFKLEwExgGdsb2JhbABaDsJRgRoWDgEBCwcECQkUBSOCJAEBAQQnEQgBATYBAQ8LDgoJFg8JAwIBAgEjBR0GDQEHAQGIDJhxiwyERwEFjTQGkDsHhBGeD44GQA X-IronPort-AV: E=Sophos;i="4.89,862,1367964000"; d="scan'208";a="23769071" Received: from hera.mpi-klsb.mpg.de ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 12 Aug 2013 14:15:49 +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=F3bQYUOO/LWbLgWzIsmw6jQU1unpnRg5TD7x+XBTGVA=; b=dOGBLT020BhJ0he7guGL73LpRmQXHxeCdTmdyJXfSAqzct+I3E7/73jAkvdEa6Cb1k4mO5hnafVQNsiL2d2sMmBinkFyacQjzmtsqIodD3AeqDDdctxM4RQTORPFhSG2bswTAjxXfGHpGA1m7rUzTrfiY44+Y0DfmZzxIU1Gv9c=; Received: from zak.mpi-klsb.mpg.de ([139.19.1.29]:51396) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8r2G-0005UK-E9; Mon, 12 Aug 2013 14:15:46 +0200 Received: from [74.125.57.233] (port=7351 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 1V8r2F-00085W-VZ; Mon, 12 Aug 2013 14:15:44 +0200 Message-ID: <5208D1EF.5050302@mpi-sws.org> Date: Mon, 12 Aug 2013 14:15:43 +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> In-Reply-To: <86haevnnr5.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 01:37 PM, Leo White wrote: >>> So, >>> >>> let g x = let module X = (val x : D) in X.(f x) >>> >>> would have a type: >>> >>> (module D with ..) -> int >> >> This certainly is a nice suggestive syntax, but it is assuming an underlying semantic similarity that does not >> exist. Semantically, the type sharing equations on signatures have very little in common with rows, and I have a hard >> time imagining what interpreting the above as a row would even mean or how it would fit in with either core or module >> typing. > > I don't see what is hard to imagine. The row variable represents > possible extra with-constraints. The type above can be unified with any > package type with signature D. > > With-constraints are essentially sets of label and type pairs, row > polymorphism provides a mechanism for typing sets of label and type > pairs. I don't see where they differ "semantically". With constraints generally map _type paths_ to _type constructors_. Moreover, the domain of type paths is bounded by what actually occurs in the signature. That already sets them apart from rows on a basic syntactic and semantic level. (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.) 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 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. Hope those are enough open questions for now. :) /Andreas