From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id q1MNHxYn017701 for ; Thu, 23 Feb 2012 00:17:59 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ap0EAKp2RU+FBoIF/2dsb2JhbAA7CbNbgXMBAQQBOgYDATUBAQMLCxgcElcGiBSlOIQwjk0BBolfg1EICwMPDQISEgUDAoUmgzNjiFGMa5J8 X-IronPort-AV: E=Sophos;i="4.73,466,1325458800"; d="scan'208";a="145516895" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail1-smtp-roc.national.inria.fr with ESMTP; 23 Feb 2012 00:17:53 +0100 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 064DD6298; Thu, 23 Feb 2012 08:17:51 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172.math.nagoya-u.ac.jp [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id B9CDC3A13; Thu, 23 Feb 2012 08:17:50 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to; s=alpha; bh=u7aFeFvvI7FnGsM0sL+3Xjffvrw=; b=swOPwaoq5/TpOXoIhnUpmSg48aFv vox+zMV6qW6FUXroboj64nHpijifzcK88gNgkG4jpS+DI9gkSeue0d3bwVTXTYRo Y9Lu7IOD2AfCMVVs1uBVpKcGRUfv6z3mIc85CtGSHBqxDXyyvzqGwesHMfLb7nf/ ir8v7SaluoLkuKM= DomainKey-Signature: a=rsa-sha1; h=Received:Subject:Mime-Version:Content-Type:From:In-Reply-To:Date:Cc:Content-Transfer-Encoding:Message-Id:References:To:X-Mailer; b=EZLBQplVb06Wmgb4D3b6yopQULnfrQQP8jSsduDlxOr1cIigAaRdLEY30M7rkDN3IKjjBheTpujmYL1rphs63Sn/Acerdpm7FwsC8xfewSiTEEzbKroSpRVTauivBEA6tY/U+kRE1g3wyaDPnY71vDzHJzFS9yCV/NNery/WCq0=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTPSA id 7CBBF3998; Thu, 23 Feb 2012 08:17:50 +0900 (JST) Mime-Version: 1.0 (Apple Message framework v1084) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <5C609F89-8739-4280-A6D9-3F78C451E0C1@mpi-sws.org> Date: Thu, 23 Feb 2012 08:17:49 +0900 Cc: Gabriel Scherer , caml List Message-Id: <823246DB-16D0-45CB-953A-3283CA077869@math.nagoya-u.ac.jp> References: <5C609F89-8739-4280-A6D9-3F78C451E0C1@mpi-sws.org> To: Andreas Rossberg X-Mailer: Apple Mail (2.1084) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id q1MNHxYn017701 Subject: Re: [Caml-list] Re: "module type of" on sub-module of functor result On 2012/02/23, at 3:49, Andreas Rossberg wrote: > On Feb 22, 2012, at 18.24 h, Gabriel Scherer wrote: >>> [A(B)] and [A.B] are syntacticly valid module_expr's but >>> [A(B).C] isn't. Is this because of an inherent limitation in the >>> module system? >> >> I believe so. When you apply a functor, you may get fresh types as a >> result -- the generative (abstract, algebraic) types of the functor >> image. If you write `module M = A(B)`, the fresh types have a clear >> identity: M.t, M.q etc; similarly if you pass A(B) to a functor with >> formal parameter X, it is X.t, X.q etc. But if you write `module M = >> A(B).C`, there is no syntactic way to name the fresh types generated >> by the functor application; in particular, naming them A(B).t would be >> incorrect -- because you could mix types of different applications. >> >> For example, what would be the signature of A(B).C with: >> >> module B = struct end >> module A(X : sig end) = struct >> type t >> module C = struct type q = t end >> end >> >> ? > > Are you perhaps thinking of SML-style generative functors here? Because with Ocaml's applicative functors F(A) in fact always returns the same abstract types, and you _can_ actually refer to types via the notation F(A).t ;-) This is not strictly correct, because of the possibility of avoidance. I.e. you are allowed to apply a functor to a structure rather than a path, and in that case the behavior of the functor becomes generative, so the problem described by Gabriel really applies in that case. Going back to the question of "module type of", it is currently implemented by typing the module expression in the usual way. So extending it to a stronger form of module expression would require changing that, and introduce extra complexity. Doable, but don't hold your breath... Jacques Garrigue