From mboxrd@z Thu Jan 1 00:00:00 1970 Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by walapai.inria.fr (8.13.6/8.13.6) with ESMTP id p0K1hrvR018361 for ; Thu, 20 Jan 2011 02:43:53 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AoMBALYhN03RVdg2kGdsb2JhbACZR4p6CBUBAQEBCQkMBxEEIKNOjBKEb4hbAQEDBYVLBIRthjGEEIU4 X-IronPort-AV: E=Sophos;i="4.60,347,1291590000"; d="scan'208";a="85585852" Received: from mail-qw0-f54.google.com ([209.85.216.54]) by mail4-smtp-sop.national.inria.fr with ESMTP/TLS/RC4-MD5; 20 Jan 2011 02:43:48 +0100 Received: by qwj9 with SMTP id 9so48687qwj.27 for ; Wed, 19 Jan 2011 17:43:47 -0800 (PST) DKIM-Signature: v=1; a=rsa-sha256; c=relaxed/relaxed; d=gmail.com; s=gamma; h=domainkey-signature:sender:subject:mime-version:content-type:from :in-reply-to:date:cc:content-transfer-encoding:message-id:references :to:x-mailer; bh=9119vKEEOS0Zo82a4wsexo1IY9MEQh9hKsGUxTaDSQM=; b=ouIl0xNxMqBBm8JuZo44IQDd3BEjMO2BffzL2R7H6oSyTFcYLizOxtd8G91MjVfgCT ZPCWF+4UcJqYSYtcGAUmB7lZsVBG8B/B76jYFnaAp/43yxBL45m4iMzMaHvlYCmCzmnd /V9dAlMtU0hYxNlbyCrzcE4cQ2h7oHmWkbwlo= DomainKey-Signature: a=rsa-sha1; c=nofws; d=gmail.com; s=gamma; h=sender:subject:mime-version:content-type:from:in-reply-to:date:cc :content-transfer-encoding:message-id:references:to:x-mailer; b=nsQtHcKz56qEPZ4cPv1YMkrEudzBKKs5DCynxQ/X4WH07CqT9fUgA5Hmli0iG+W+Wr QBJ/pB3LLXo3tSpXdZeApjQ4f9kydirPg8cVmUsKGcEXk3RrZZh53hlaN57A/dqbbhrG 9eMJOLm2Ss3G8q2Pzt1K1F0r9Lmq8JWFtJcG4= Received: by 10.229.220.81 with SMTP id hx17mr1218148qcb.116.1295487826523; Wed, 19 Jan 2011 17:43:46 -0800 (PST) Received: from tet.garrigue.jp (58x158x128x157.ap58.ftth.ucom.ne.jp [58.158.128.157]) by mx.google.com with ESMTPS id l12sm5242013qcu.7.2011.01.19.17.43.43 (version=TLSv1/SSLv3 cipher=RC4-MD5); Wed, 19 Jan 2011 17:43:44 -0800 (PST) Sender: Jacques Garrigue Mime-Version: 1.0 (Apple Message framework v1082) Content-Type: text/plain; charset=us-ascii From: Jacques Garrigue In-Reply-To: <20110119123335.GL323@melkinpaasi.cs.helsinki.fi> Date: Thu, 20 Jan 2011 10:43:41 +0900 Cc: caml-list@inria.fr Message-Id: References: <20110119123335.GL323@melkinpaasi.cs.helsinki.fi> To: Lauri Alanko X-Mailer: Apple Mail (2.1082) Content-Transfer-Encoding: 8bit X-MIME-Autoconverted: from quoted-printable to 8bit by walapai.inria.fr id p0K1hrvR018361 Subject: Re: [Caml-list] Limitations of first-class modules On 2011/01/19, at 21:33, Lauri Alanko wrote: > When first-class modules were announced for OCaml 3.12, I cheered them > as a sorely needed extension, and I have now begun to make heavy use > of them. I certainly prefer them over objects, even if I do find the > syntax of first-class modules a bit awkward. I would much prefer to > see a completely unified object-module system a la Scala, but I guess > such drastic changes are beyond the scope of OCaml's development > nowadays. > > Anyway, I'm now beginning to stumble into the limitations of the > extension, and I'm a bit curious about their rationale. > > In a type (module S), S must be a path to a named module type, and if > A and B are two different paths, (module A) and (module B) are > distinct even if A and B are transparent definitions for exactly the > same module types. This nominalism is quite surprising since one is > used to transparent definitions being just shorthands for signatures > that are compared structurally. In particular, this means that it is > no longer harmless to include a signature definition to compose a > convenience module from several submodules: > > module A = struct > module type S = sig end > type t = (module S) > module M : S = struct end > let v = (module M : S) > end > > module B = struct > include A > end > > # module X : A.S = B.M;; > module X : A.S > > # let x : A.t = B.v;; > Error: This expression has type (module B.S) > but an expression was expected of type A.t = (module A.S) I think there are two reasons for this limitation: * avoiding having to run a full module type comparison during unification (potentially costly) * in case the first-class module has type variables in its parameters, the original algorithm for module type comparison cannot be applied directly I'm not sure the first reason matters that much. The second one is more problematic, but clearly does not apply to your case. So it should at least be possible to check module type equality structurally for parameter-less first-class module types. Note that if you use the trunk version (3.13), you need less annotations, so you could write: let x : A.t = (module (val B.v)) A bit verbose, but no extra type annotations. > Also, the limitations of package type constraints were also somewhat > surprising. The main goal of package type constraints is to allow connecting types in the signature with type variables in the context. Since type variables cannot have higher-order kinds in ocaml, allowing to specify parameterized types in with constraints would not make sense from that point of view. It may still be useful, but there may be difficulties in connection with the new implicit pack/unpack mecanism. Jacques Garrigue