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 1A2F9820A1 for ; Sun, 11 Aug 2013 09:53:43 +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: Al4EAKJCB1KLEwExaWdsb2JhbABZDsJdgRgWDg0FBhIUBSOCJAEBAQMBJxkBATcBBAsLRlcGE4gKBgSlEYRHAQWMeQaOf4EJMweDG3asFUCBZg X-IPAS-Result: Al4EAKJCB1KLEwExaWdsb2JhbABZDsJdgRgWDg0FBhIUBSOCJAEBAQMBJxkBATcBBAsLRlcGE4gKBgSlEYRHAQWMeQaOf4EJMweDG3asFUCBZg X-IronPort-AV: E=Sophos;i="4.89,855,1367964000"; d="scan'208";a="23701257" Received: from hera.mpi-klsb.mpg.de ([139.19.1.49]) by mail3-smtp-sop.national.inria.fr with ESMTP/TLS/AES256-SHA; 11 Aug 2013 09:53:42 +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=gXn5lcrgSkL8cZwQXmlsp9cpQmZxjpiLxkbW91IYNNQ=; b=cGoL5FkYjAXN9xae+VpJyB6Icc8EMznh/SQVz0XjAM+nqBi+3xGM3KrOFNhp9ngLyPc8HFY9uYX3xeeVI23e+UxD0Dt6OfxzeMVGkkbmJT8JxlB83dsA5GkJ/AQih5i5eGZu2MJiBKPENbmXszELdysiMGOIT+XLaSYJBv9jGzA=; Received: from srv-00-126.mpi-klsb.mpg.de ([139.19.1.29]:59518 helo=zak.mpi-klsb.mpg.de) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1V8QT4-0003HC-Om; Sun, 11 Aug 2013 09:53:40 +0200 Received: from mnch-5d85e21a.pool.mediaways.net ([93.133.226.26]:53964 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 1V8QT4-00066V-9z; Sun, 11 Aug 2013 09:53:38 +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 09:53:48 +0200 Cc: Caml List Content-Transfer-Encoding: quoted-printable Message-Id: <1407E74D-EDC8-4638-8917-4CAC80B4C682@mpi-sws.org> References: 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 03:55 , David Sheets wrote: > What issue prevents functions over first-class modules from forgetting > the first-class modules' type constraints? >=20 > That is, given: >=20 > ############### >=20 > module type D =3D sig > type t >=20 > val x : t > val f : t -> int > end >=20 > module type C =3D sig > val q : int > end >=20 > module F(X : D) : C =3D struct > let q =3D X.(f x) > end >=20 > let f x =3D > let module X =3D (val x : D) in > let module Q =3D struct > let q =3D X.(f x) > end in > (module Q : C) >=20 > let x =3D > let module X =3D struct > type t =3D int >=20 > let x =3D 2 > let f x =3D x * 3 > end in > (module X : D with type t =3D int) >=20 > ;; > let module X =3D (val x : D with type t =3D int) in > let module M =3D F(X) in > (* let x =3D (module (val x : D with type t =3D int) : D) in*) > let module M' =3D (val f x : C) in >=20 > Printf.printf "M.q is %d\n%!" M.q; > Printf.printf "M'.q is %d\n%!" M'.q; > () >=20 > ############### >=20 > Why must I uncomment (* let x =3D (module (val x : D with type t =3D int) > : D) in*) to compile? >=20 > 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? There is no implicit subtyping in OCaml's core language. The reason for tha= t is not code generation, but type inference. For example, what type should= the following function be given if the subtyping you ask for could apply? let g x =3D let module X =3D (val x : D) in X.(f x) That said, as usual in OCaml, you can force subtyping explicitly. That is, = you are able to just say let module M' =3D (val f (x :> (module D)) : C) in =85 in your example. (Explicit subtyping on package types is still very limited= , though, i.e. only allows forgetting type equations on the same named sign= ature.) /Andreas