From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@yquem.inria.fr Delivered-To: caml-list@yquem.inria.fr Received: from mail4-relais-sop.national.inria.fr (mail4-relais-sop.national.inria.fr [192.134.164.105]) by yquem.inria.fr (Postfix) with ESMTP id EE9E8BC57 for ; Thu, 22 Jul 2010 08:18:50 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AtoEADp/R0yFBoIFgWdsb2JhbACTN4xTAQEWIiKxZI8SAQSFMoQChFs X-IronPort-AV: E=Sophos;i="4.55,241,1278280800"; d="scan'208";a="66791065" Received: from rabbit.math.nagoya-u.ac.jp (HELO mailhost.math.nagoya-u.ac.jp) ([133.6.130.5]) by mail4-smtp-sop.national.inria.fr with ESMTP; 22 Jul 2010 08:18:49 +0200 Received: from mailhost.math.nagoya-u.ac.jp (localhost [127.0.0.1]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 0BA95B679; Thu, 22 Jul 2010 15:18:45 +0900 (JST) Received: from mailhost.math.nagoya-u.ac.jp (camel-172 [172.16.254.4]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id BBFD588B7; Thu, 22 Jul 2010 15:18:44 +0900 (JST) DKIM-Signature: v=1; a=rsa-sha1; c=relaxed; d=math.nagoya-u.ac.jp; h= date:message-id:to:cc:subject:from:in-reply-to:references :mime-version:content-type:content-transfer-encoding; s=alpha; bh=w7fTyzBBOnxJETDa4k2ONTMjUM0=; b=fou+uAyZqpL4MNAGTDlu3B71c3Yx pBQfJzkb+5Qt+HAj/WWXJ3IMRPdjJqT2BNQEueJu0ynOB78Jae13QiH8zxxW7i45 a5Q7S+tB+UKx4wrLqpZW7E9OYmKMcbesaGvFj23QycJZPm0nC10pumG2b8Zg4Dqz Mhy59ac7oQIOzdM= DomainKey-Signature: a=rsa-sha1; h=Received:Date:Message-Id:To:Cc:Subject:From:In-Reply-To:References:X-Mailer:Mime-Version:Content-Type:Content-Transfer-Encoding; b=zV6FzltEMg01rxlEnjIjd7JmUxM3qQOLg9rVw2tS8taolHinvwMktvgQZ7+eLZhZD2+ssvSfhuME9RB7dvBmUBW8Bmbfi0QJMzuTQPOJf83iAkmulwLb2b0Cu8hAjJ8yzODuLncF+ObJGuq2czXvWCKP65qVWoNJ49TlQ1OucrA=; c=nofws; d=math.nagoya-u.ac.jp; q=dns; s=alpha Received: from localhost (bsdserver02 [172.16.249.2]) by mailhost.math.nagoya-u.ac.jp (Postfix) with ESMTP id 8F2B488B6; Thu, 22 Jul 2010 15:18:44 +0900 (JST) Date: Thu, 22 Jul 2010 15:18:39 +0900 (JST) Message-Id: <20100722.151839.48519361.garrigue@math.nagoya-u.ac.jp> To: dumitru.potop_butucaru@inria.fr Cc: caml-list@inria.fr Subject: Re: [Caml-list] Bug in the module system of version 3.12.0+beta1 From: Jacques Garrigue In-Reply-To: <4C473F45.6020307@inria.fr> References: <4C46F866.9050900@inria.fr> <4C473F45.6020307@inria.fr> X-Mailer: Mew version 6.3 on Emacs 22.3 / Mule 5.0 (SAKAKI) Mime-Version: 1.0 Content-Type: Text/Plain; charset=us-ascii Content-Transfer-Encoding: 7bit X-Spam: no; 0.00; bug:01 functor:01 sig:01 val:01 functor:01 sig:01 haskell:01 coq:01 overloading:01 doubly:01 functors:01 signatures:01 signatures:01 caml-list:01 pairs:01 From: Dumitru Potop-Butucaru > However, I still did not understand this statement of > Jeremy Yallop: >>> module type Abc = >>> functor (M:Simple) -> >>> sig >>> val x : M.t >>> end >>> >> You're trying to treat Abc as a functor from signatures to signatures >> (i.e. as a parameterised signature). In fact, it's something quite >> different: it's the *type* of a functor from structures to structures. >> > If I understand well, what I try to do is impossible for > some deep theoretical reason. Can someone explain this > to me, or point me to a relevant paper explaining it? I think this is not a question of impossibility, rather of misunderstanding of the relation between modules and signatures. A module type describes modules, it does not replace them. In particular, in another mail you asked for the construct: module type MyModuleType(Param:ParamType) = sig ... end But this just doesn't make sense. The type of a functor is not a functor between module types. Just like the type "t1 * t2" describes pairs of values of type t1 and t2, but it is not itself a pair of types, but rather a product. Note of course that one might want to play on the conceptual similarity to write the two in the same way. Haskell does that a lot, writing (t1,t2) for the product of the types t1 and t2. But if you look at languages like Coq, where types are also values, this kind of overloading seems dangerous. Another similar misunderstanding is when you write include Abc(module type of IntSet) This statement is doubly wrong: first you cannot apply a module type, but even if Abc were a functor, it could only be applied to a module, not a module type. Others have explained how you can do what you intended, in two different ways. The classical way is to use a real functor, returning a signature enclosed in a module, since there is no way to return a signature alone. There is nothing against applying functors inside signatures. The new solution in 3.12 is to use a variant of the "with" construct, which does exactly what you want, i.e. it turns a signature into a "function" returning a signature. Hope this helps, Jacques Garrigue