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 C5697820A1 for ; Sun, 11 Aug 2013 16:32:26 +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: AhYEALWfB1KLEwExaWdsb2JhbABZDsJdgS0ODQUGCQkUBSOCJAEBAQMBQAEBMAcBBAsLGC5XBhOICgYEpCmERwEFjHIGjn+BCTMHgxt2lBCYBUCBZg X-IPAS-Result: AhYEALWfB1KLEwExaWdsb2JhbABZDsJdgS0ODQUGCQkUBSOCJAEBAQMBQAEBMAcBBAsLGC5XBhOICgYEpCmERwEFjHIGjn+BCTMHgxt2lBCYBUCBZg X-IronPort-AV: E=Sophos;i="4.89,856,1367964000"; d="scan'208";a="23713842" Received: from infao0809.mpi-klsb.mpg.de (HELO hera.mpi-klsb.mpg.de) ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 11 Aug 2013 16:32:26 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=To:References:Message-Id:Content-Transfer-Encoding:Cc:Date:In-Reply-To:From:Content-Type:Mime-Version:Subject; bh=uXuUegUvgYeVO/OedkpB1vtG30tdVtvLTqOk3taY2cI=; b=RJpDS4DqQpr/iAM1RVWKlMkVBTulTLgG5E3auADLKq7xd42YB1NfvumDlc9fJVjq5zqq3QlQZ/yKY+dYCOWl6OL/pvqBp/XCv+qB9V7XuYCBP9o1+mFfrI5pwP3QPrnvLAKAaS6hBZCUCfuHI8OIpgf7AInsAXoBIo10N5nfR1k=; Received: from srv-00-126.mpi-klsb.mpg.de ([139.19.1.29]:35733 helo=zak.mpi-klsb.mpg.de) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8Wgx-0005vL-8o; Sun, 11 Aug 2013 16:32:25 +0200 Received: from mnch-5d85e21a.pool.mediaways.net ([93.133.226.26]:58489 helo=[192.168.178.50]) by zak.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.72) id 1V8Wgw-0002Zv-RC; Sun, 11 Aug 2013 16:32:22 +0200 Mime-Version: 1.0 (Mac OS X Mail 6.2 \(1499\)) Content-Type: text/plain; charset=windows-1252 From: Andreas Rossberg In-Reply-To: Date: Sun, 11 Aug 2013 16:32:33 +0200 Cc: Caml List Content-Transfer-Encoding: quoted-printable Message-Id: <9D61A8E2-D0B4-452A-B372-401E499423AE@mpi-sws.org> References: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> To: David Sheets X-Mailer: Apple Mail (2.1499) X-MPI-Local-Sender: true Subject: Re: [Caml-list] First-class Functor Forgetting for Free On Aug 11, 2013, at 15:29 , David Sheets wrote: > On Sun, Aug 11, 2013 at 8:53 AM, Andreas Rossberg = wrote: >> On Aug 11, 2013, at 03:55 , David Sheets wrote: >>> I understand why structural subtyping requires a module cast but I >>> don't see why type relaxation would. >>> I looked at the generated assembly and this line seems to disappear. >>>=20 >>> Why is it needed? >>=20 >> There is no implicit subtyping in OCaml's core language. The reason for = that is not code generation, but type inference. For example, what type sho= uld the following function be given if the subtyping you ask for could appl= y? >>=20 >> let g x =3D let module X =3D (val x : D) in X.(f x) >=20 > Something like val g : [< (module D)] or simply val g : (module D) > where the type constraint relation is implicit seems reasonable. I > don't know if you consider polymorphic variant types as part of the > core language (or perhaps they aren't implicit because they propagate > inequalities?). I don't think type inference for polymorphic variants works the way you thi= nk it does. Inference for both variants and objects is based on row polymor= phism, not subtyping. A type like [< A] is actually a polymorphic type with= a hidden type variable, not a subtype bound, even though the surface synta= x intentionally hides that fact (which isn't always helpful). Module signat= ures are totally different beasts, where matching _is_ a form of subtyping. > I guess the module system isn't part of the core as it does implicit > structural subtyping. This makes the embedding of the module type > system into the value type system surprising. Essentially, the fundamental technical differences (and different trade-off= s) between core and module typing are the reason why you need the stratific= ation between core and modules and the explicit embedding at all. If type i= nference modulo signature matching worked, modules probably wouldn't need t= o be a separate language layer. But there are fundamental limitations preve= nting that, e.g. completeness and decidability concerns. >> That said, as usual in OCaml, you can force subtyping explicitly. That i= s, you are able to just say >>=20 >> let module M' =3D (val f (x :> (module D)) : C) in =85 >=20 > Good to know! I looked briefly and did not see this mentioned in the manu= al. >=20 >> in your example. (Explicit subtyping on package types is still very limi= ted, though, i.e. only allows forgetting type equations on the same named s= ignature.) >=20 > This seems somewhat strange. Why are aliases not followed? Typing of first-class modules in OCaml essentially reinterprets signature b= indings as nominal type definitions, in order to side-step a number of tech= nical implications that would arise with a more structural interpretation. = Arguably, that's a bit of a hack (I hope that I don't offend anybody :) ). = Unfortunately, it is not easy to be substantially more flexible without mod= ifications to the innards of the module type system. /Andreas