From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: Delivered-To: caml-list@yquem.inria.fr Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by yquem.inria.fr (Postfix) with ESMTP id A1FE4BCAB for ; Thu, 12 May 2005 16:24:54 +0200 (CEST) Received: from pauillac.inria.fr (pauillac.inria.fr [128.93.11.35]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j4CEOsSr027316 for ; Thu, 12 May 2005 16:24:54 +0200 Received: from concorde.inria.fr (concorde.inria.fr [192.93.2.39]) by pauillac.inria.fr (8.7.6/8.7.3) with ESMTP id QAA06928 for ; Thu, 12 May 2005 16:24:53 +0200 (MET DST) Received: from triton.rz.uni-saarland.de (triton.rz.uni-saarland.de [134.96.7.25]) by concorde.inria.fr (8.13.0/8.13.0) with ESMTP id j4CEOr8X027313 for ; Thu, 12 May 2005 16:24:53 +0200 Received: from uni-sb.de (uni-sb.de [134.96.7.230]) by triton.rz.uni-saarland.de (8.12.10/8.12.10) with ESMTP id j4CEOqQw2663633 for ; Thu, 12 May 2005 16:24:52 +0200 (CEST) Received: from cs.uni-sb.de (cs.uni-sb.de [134.96.252.31]) by uni-sb.de (8.13.4/2005033000) with ESMTP id j4CEOpUB020763 for ; Thu, 12 May 2005 16:24:51 +0200 (CEST) Received: from mail.cs.uni-sb.de (mail.cs.uni-sb.de [134.96.254.200]) by cs.uni-sb.de (8.13.4/2005033000) with ESMTP id j4CEOo0M018610 for ; Thu, 12 May 2005 16:24:50 +0200 (CEST) Received: from ps.uni-sb.de (grizzly.ps.uni-sb.de [134.96.186.68]) by mail.cs.uni-sb.de (8.13.4/2005033000) with ESMTP id j4CEOnm3008185 for ; Thu, 12 May 2005 16:24:49 +0200 (CEST) X-Authentication-Warning: mail.cs.uni-sb.de: Host grizzly.ps.uni-sb.de [134.96.186.68] claimed to be ps.uni-sb.de Received: from ps.uni-sb.de (groove.ps.uni-sb.de [134.96.186.172]) by ps.uni-sb.de (8.12.10/8.12.10) with ESMTP id j4CEOmqL003568; Thu, 12 May 2005 16:24:48 +0200 Message-ID: <42836730.9050603@ps.uni-sb.de> Date: Thu, 12 May 2005 16:24:48 +0200 From: Andreas Rossberg User-Agent: Mozilla/5.0 (X11; U; Linux i686; en-US; rv:1.4.1) Gecko/20031114 X-Accept-Language: en-us, en MIME-Version: 1.0 To: ocaml Subject: Re: [Caml-list] Renaming structures during inclusions? References: <20050511.183319.06547596.debian00@tiscali.be> <42823CDF.3060109@ps.uni-sb.de> In-Reply-To: Content-Type: text/plain; charset=us-ascii; format=flowed Content-Transfer-Encoding: 7bit X-Greylist: Sender IP whitelisted, not delayed by milter-greylist-1.5.1 (triton.rz.uni-saarland.de [134.96.7.25]); Thu, 12 May 2005 16:24:52 +0200 (CEST) X-AntiVirus: checked by AntiVir Milter 1.0.6; AVE 6.30.0.12; VDF 6.30.0.174 X-Miltered: at concorde with ID 42836736.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Miltered: at concorde with ID 42836735.000 by Joe's j-chkmail (http://j-chkmail.ensmp.fr)! X-Spam: no; 0.00; rossberg:01 rossberg:01 caml-list:01 markus:01 mottl:01 ocaml's:01 compiler:01 internals:01 inference:01 struct:01 sml:01 ocaml:01 compiler:01 christophe:01 troestler:01 X-Spam-Checker-Version: SpamAssassin 3.0.2 (2004-11-16) on yquem.inria.fr X-Spam-Status: No, score=0.0 required=5.0 tests=none autolearn=disabled version=3.0.2 X-Spam-Level: Markus Mottl wrote: > >> Note that OCaml's type system fundamentally relies on the fact that >> type names cannot be shadowed in structures. > > Hm, I don't see why this should be so, can you elaborate? I don't know > the compiler internals about type inference, this seems like a > question of how types are identified internally. I make the reasonable > guess that it is not by names (strings) but some kind of integer id or > similar. It's by paths like A.B.C, in which only A is an alpha-convertible identifier, the rest are labels. Now consider: module X = struct type t = C let x = C type t = int end How would you express the type of X.x? There is no label that allows projecting the shadowed t. Sure there are ways to solve this (SML allows the above, for example), but most likely they require deviating from, or at least extending the theory underlying OCaml modules at the moment (and are likely to be not as nice). > Maybe I don't see the problem, but since I feel confident that I can > always solve this problem manually in a fairly mechanized and > straightforward way, I'd be surprised if this couldn't be done by the > compiler. Isn't it just a normal alpha conversion problem? Christophe TROESTLER wrote: > > The substitution in itself is nothing difficult, isn't it. Or is it > because you need to "backtrack" to change the inferred sigs? Is the > problem when to do it? Do you have examples? I do not immediately > see why a rule like "duplicate types/modules are forbidden in a sig > unless one of them is explicitely renamed" would be difficult to check[1]. The first problem is that this construction is a special case - you write a signature and it contains occurrences of shadowing. In general shadowed items cannot just be forgotten (see the example above), so how do you characterise this special case? How can the type checker recognise it? It would probably be pretty ad-hoc. The obstacles are the dependencies within a signature, which prohibit arbitrary reordering, and the inability to alpha-rename labels. An algorithm that covers all possible cases where a type or module name can be forgotten is non-obvious (probably as difficult as identifying these cases in the first place). I don't think it's easily doable within the current theoretical framework. Jacques pointed to a paper that seems to be solving this problem, but it is using an entirely different framework (and quite a baroque one, I have to add). Not all signatures in this framework are translatable back to OCaml's, e.g. they can contain mutually dependent substructures. However, if we just want renaming, and it is explicit, then everything should be pretty straightforward. > Yes, you are correct -- I was thinking of checking the sig against a > given one, not to generate it. But as is, this isn't a valid sig, so you cannot match it against another one. Cheers, - Andreas -- Andreas Rossberg, rossberg@ps.uni-sb.de Let's get rid of those possible thingies! -- TB