From mboxrd@z Thu Jan 1 00:00:00 1970 Return-Path: X-Spam-Checker-Version: SpamAssassin 3.1.3 (2006-06-01) on yquem.inria.fr X-Spam-Level: X-Spam-Status: No, score=0.0 required=5.0 tests=AWL autolearn=disabled version=3.1.3 Received: from mail3-relais-sop.national.inria.fr (mail3-relais-sop.national.inria.fr [192.134.164.104]) by yquem.inria.fr (Postfix) with ESMTP id 3A9BBBC6B for ; Fri, 11 Jan 2008 22:04:12 +0100 (CET) X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: Ao8CABZoh0fAXQInh2dsb2JhbACBVo5EAQEBCAopmV4 X-IronPort-AV: E=Sophos;i="4.24,273,1196636400"; d="scan'208";a="7717930" Received: from concorde.inria.fr ([192.93.2.39]) by mail3-smtp-sop.national.inria.fr with ESMTP; 11 Jan 2008 22:04:11 +0100 Received: from mail1-relais-roc.national.inria.fr (mail1-relais-roc.national.inria.fr [192.134.164.82]) by concorde.inria.fr (8.13.6/8.13.6) with ESMTP id m0BL4Bd8026430 (version=TLSv1/SSLv3 cipher=RC4-SHA bits=128 verify=OK) for ; Fri, 11 Jan 2008 22:04:11 +0100 X-IronPort-Anti-Spam-Filtered: true X-IronPort-Anti-Spam-Result: AgAAABZoh0dT9QHmi2dsb2JhbACBVo5EAQEBCAQGDxqZXg X-IronPort-AV: E=Sophos;i="4.24,273,1196636400"; d="scan'208";a="6553649" Received: from pop.bulldoghome.com (HELO bdmail1.accesst.com) ([83.245.1.230]) by mail1-smtp-roc.national.inria.fr with ESMTP; 11 Jan 2008 22:04:11 +0100 Received: from host-84-9-232-121.bulldogdsl.com ([84.9.232.121] helo=[192.168.123.191]) by bdmail1.accesst.com with esmtpa (Exim 4.50) id 1JDR0r-0004oj-NS; Fri, 11 Jan 2008 21:02:01 +0000 Message-ID: <4787D89D.8040302@ed.ac.uk> Date: Fri, 11 Jan 2008 20:59:09 +0000 From: Jeremy Yallop User-Agent: Mozilla-Thunderbird 2.0.0.9 (X11/20080110) MIME-Version: 1.0 To: yminsky@gmail.com Cc: Caml Mailing List Subject: Re: [Caml-list] A confusing module question References: <891bd3390801111105xb75df53id4358939e8b2b05c@mail.gmail.com> In-Reply-To: <891bd3390801111105xb75df53id4358939e8b2b05c@mail.gmail.com> Content-Type: text/plain; charset=ISO-8859-1; format=flowed Content-Transfer-Encoding: 7bit X-Miltered: at concorde with ID 4787D9CB.000 by Joe's j-chkmail (http://j-chkmail . ensmp . fr)! X-Spam: no; 0.00; impatient:01 yaron:01 minsky:01 sig:01 foo:01 struct:01 foo:01 struct:01 ocaml:01 model:01 syntax:01 ocaml:01 datatype:01 haskell:01 specifies:01 [Warning: rather long. There's a summary at the end for the impatient.] Yaron Minsky wrote: > Here's some fairly simple module code that fails unexpectedly. N > compiles cleanly, but M has an error, even though they seem like > they should both work: Here's a slightly simplified version which retains the essence of the problem (the "include" and "with"-constraint are not essential in this case): module type S = sig type exposed_t = { foo : int } type t = exposed_t end module M : S = struct type t = { foo : int } type exposed_t = t end module N : S = struct type exposed_t = { foo : int } type t = exposed_t end > I've been programming in OCaml for along time, and I still don't > have a really good mental model to understand when some module trick > I try is going to work. How do people think about things like this? I think of the two type declarations in each module as being quite different, despite the similar syntax. Type declarations in OCaml fall into two categories. A declaration for a record or variant type type t1 = { foo : int } type t2 = Foo of int declares a fresh type, incompatible with all other types. Other declarations type t3 = [`Foo of int] type t4 = int * string type t5 = t2 type t6 = t1 list (* etc. *) don't create new types: they just introduce aliases for types which already exist. (Other functional languages use different keywords to capture this distinction. Standard ML uses "datatype" for fresh types and "type" for aliases in Standard ML; Haskell uses "data" and "type" respectively.) The key to understanding this example is the requirement that the implementation of a signature be, for each type component, at least as fresh as the signature. That is, if a type in the signature is declared fresh then the corresponding declaration in the implementation must also declare a fresh type. In the modified example above the declaration for "exposed_t" in the signature "S" specifies a fresh type: the corresponding declaration in any module matching the signature must therefore also specify a fresh type. In contrast, the declaration for "t" in "S" simply gives an equation: the type "t" in any matching module must be equivalent to the type "exposed_t". Now it should be clear why "N" matches "S", but "M" does not. In "N" the right-hand side for the declaration of "exposed_t" is a fresh type (since it's a record definition), so it's possible for it to match the corresponding declaration in "S". In the module "M" the right-hand side for the declaration of "exposed_t" isn't a fresh type at all, so it cannot match the "exposed_t" in the signature. I've simplified slightly in the notes above: the precise rules (which include cases for abstract types and datatype replication) are given in 6.10.2 of the manual under the heading "Type specification" (http://caml.inria.fr/pub/docs/manual-ocaml/manual018.html). Finally, the promised summary: type declarations declare either fresh types or aliases; fresh type declarations in signatures are matched only by fresh type declarations in structures. Jeremy.