Re: [Caml-list] A confusing module question

[Jeremy Yallop <jeremy.yallop@ed.ac.uk>]

[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.