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 mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by yquem.inria.fr (Postfix) with ESMTP id 564C8BC57 for ; Thu, 22 Jul 2010 09:07:29 +0200 (CEST) X-IronPort-AV: E=Sophos;i="4.55,242,1278280800"; d="vcf'?scan'208";a="64251391" Received: from vpn-rocq-152.inria.fr (HELO [127.0.0.1]) ([128.93.42.152]) by mail1-relais-roc.national.inria.fr with ESMTP/TLS/DHE-RSA-CAMELLIA256-SHA; 22 Jul 2010 09:07:28 +0200 Message-ID: <4C47EE3C.2010908@inria.fr> Date: Thu, 22 Jul 2010 09:07:40 +0200 From: Dumitru Potop-Butucaru User-Agent: Mozilla/5.0 (Windows; U; Windows NT 6.1; en-US; rv:1.9.1.10) Gecko/20100512 Thunderbird/3.0.5 MIME-Version: 1.0 To: caml-list@inria.fr Subject: Re: [Caml-list] Bug in the module system of version 3.12.0+beta1 References: <4C46F866.9050900@inria.fr> <4C473F45.6020307@inria.fr> <20100722.151839.48519361.garrigue@math.nagoya-u.ac.jp> <4C47E768.4080507@inria.fr> <9454F06C-C286-4A1F-8A9F-CA3B27F8E3BB@gmail.com> In-Reply-To: <9454F06C-C286-4A1F-8A9F-CA3B27F8E3BB@gmail.com> Content-Type: multipart/mixed; boundary="------------010902010606080700030106" X-Spam: no; 0.00; bug:01 syntax:01 overloading:01 haskell:01 haskell:01 functors:01 ocaml:01 syntax:01 functor:01 sig:01 val:01 functor:01 sig:01 coq:01 overloading:01 X-Attachments: cset="utf-8" name="dumitru_potop_butucaru.vcf" name="dumitru_potop_butucaru.vcf" This is a multi-part message in MIME format. --------------010902010606080700030106 Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit Ok, I got it. Thank you all for the help, Jacky On 22/07/2010 08:47, Jacques Garrigue wrote: > No, I'm saying that this kind of syntax overloading occurs in Haskell. > However, since Haskell has no functors, you cannot do that either. > > Again, what you ask for is possible in ocaml, and in a particularly clean > way in 3.12. Namely, Jeremy Yallop's second example does exactly what you want. > The only difference is the syntax: you write "ABC with module M := IntList" > rather than "ABC(IntList)". Different concepts get different syntax. > > Jacques > > On 2010/07/22, at 15:38, Dumitru Potop-Butucaru wrote: > > >> So, what you say is that this way of manipulating >> module types can be done in Haskell? >> >> Yours, >> Jacky >> >> >> On 22/07/2010 08:18, Jacques Garrigue wrote: >> >>> 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 >>> >>> >>> >>> >> >> > > > --------------010902010606080700030106 Content-Type: text/x-vcard; charset=utf-8; name="dumitru_potop_butucaru.vcf" Content-Transfer-Encoding: 7bit Content-Disposition: attachment; filename="dumitru_potop_butucaru.vcf" begin:vcard fn:Dumitru Potop-Butucaru n:Potop-Butucaru;Dumitru org:INRIA Rocquencourt;Project AOSTE adr:;;Domaine de Voluceau, BP 105;Le Chesnay;;F-78153;France email;internet:dumitru.potop_butucaru@inria.fr tel;work:+33-139.63.55.80 tel;fax:+33-139.63.51.93 x-mozilla-html:FALSE url:http://www.DumitruPotop.net version:2.1 end:vcard --------------010902010606080700030106--