From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Original-To: caml-list@sympa.inria.fr Delivered-To: caml-list@sympa.inria.fr Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by sympa.inria.fr (Postfix) with ESMTPS id E11C47ED27 for ; Fri, 1 Jun 2012 00:37:03 +0200 (CEST) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AnoBALTxx0+LEwExkWdsb2JhbABEgx2xAyIBAQEBCQsLBxQFIoIYAQEBBDgCBgEBNwEPCxguVxkbh3AEpTaELgEFjnIGixGCMII2YKdw X-IronPort-AV: E=Sophos;i="4.75,693,1330902000"; d="scan'208";a="160806251" Received: from hera.mpi-klsb.mpg.de ([139.19.1.49]) by mail1-smtp-roc.national.inria.fr with ESMTP/TLS/AES256-SHA; 01 Jun 2012 00:37:03 +0200 DKIM-Signature: v=1; a=rsa-sha256; q=dns/txt; c=relaxed/relaxed; d=mpi-sb.mpg.de; s=mail200803; h=Cc:Date:Mime-Version:Content-Transfer-Encoding:Content-Type:Message-Id:References:Subject:In-Reply-To:To:From; bh=qIYU2bOWmpVT/AMTNS5bTzUObH8L5DvMrMyHSRKaR8s=; b=trOep+VRiBkZGR8AYBJlzrnKw9nZeKLqZLoT9teOzEt2TBoHeN+EOWXy4O4HCtasruovE84BHuyNn4tef5vI1tRkjJJznHXdvIoSZ42ewxJrynTAsUNp6ewPpXtDbhnTXEEtV1Nauw5qnoVhBJAmFhqWgIuXX8oOGzDrWBnLAQY=; Received: from maniac.mpi-klsb.mpg.de ([139.19.1.28]:44548) by hera.mpi-klsb.mpg.de (envelope-from ) with esmtp (Exim 4.72) id 1SaDzI-00008c-AR; Fri, 01 Jun 2012 00:37:02 +0200 Received: from mnch-4d043327.pool.mediaways.net ([77.4.51.39]:55906 helo=[192.168.178.31]) by maniac.mpi-klsb.mpg.de (envelope-from ) with esmtpsa (TLS1.0:RSA_AES_128_CBC_SHA1:16) (Exim 4.72) id 1SaDzH-00036C-PR; Fri, 01 Jun 2012 00:36:59 +0200 From: Andreas Rossberg To: rixed@happyleptic.org In-Reply-To: <20120531212229.GB28948@yeeloong.happyleptic.org> References: <20120531200555.GA30956@securactive.lan> <20120531212229.GB28948@yeeloong.happyleptic.org> Message-Id: <3C31823E-C0B6-49B5-928D-BD6083559841@mpi-sws.org> Content-Type: text/plain; charset=US-ASCII; format=flowed; delsp=yes Content-Transfer-Encoding: 7bit Mime-Version: 1.0 (Apple Message framework v936) Date: Fri, 1 Jun 2012 00:36:59 +0200 Cc: caml-list@inria.fr X-Mailer: Apple Mail (2.936) Subject: Re: [Caml-list] Strange behavior from type inference after functor application On May 31, 2012, at 23.22 h, rixed@happyleptic.org wrote: > -[ Thu, May 31, 2012 at 10:23:13PM +0200, Gabriel Scherer ]---- >> The problem with >> module C = Combi (S) (TypeWithConf (struct let v = 1 end)) >> is that the resulting type has no "name": (struct let v = 1 end) can >> not be part of a type path. > > So in order for the compiler to infer a type the type must have a > 'name'? > That's funny because this 'name' is not used anywhere. Couldn't just > such anonymous modules be given random names so that everything > works as > long as these names are unused? I mean, in the given example no type > of > this Conf module was required to infer that C.t is a product type > (which > was everything needed since f was returning the first value). > > Or would it be just too obscure and not useful enough? The compiler has to give a module type to the module C, and the OCaml type system insists that any module type it computes is expressible by a syntactically valid signature. So it has to find one that avoids mentioning S2.t. The only way to do so in a syntactically valid manner is to make t abstract altogether in the resulting signature. This is known as the "avoidance problem" in literature on ML modules. The only solution to avoid the avoidance problem is to not insist on syntactic signatures during type checking, which is essentially what you suggest (although it's a bit more complicated in general). Other dialects of ML modules indeed work like that, but it would be quite a fundamental change to the way module type checking is done in OCaml. /Andreas