A confusing module question

A confusing module question

[Yaron Minsky]

[-- Attachment #1: Type: text/plain, Size: 1045 bytes --]

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:

module type S = sig type t end

module M :
sig
  type exposed_t = { foo : int }
  include S with type t = exposed_t
end =
struct
  type t = { foo : int }
  type exposed_t = t
end

module N :
sig
  type exposed_t = { foo : int }
  include S with type t = exposed_t
end =
struct
  type exposed_t = { foo : int }
  type t = exposed_t
end

The error is as follows:

File "foo.ml", line 8, characters 0-56:
Signature mismatch:
Modules do not match:
  sig type t = { foo : int; } type exposed_t = t end
is not included in
  sig type exposed_t = { foo : int; } type t = exposed_t end
Type declarations do not match:
  type exposed_t = t
is not included in
  type exposed_t = { foo : int; }

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?

y

[-- Attachment #2: Type: text/html, Size: 4236 bytes --]

Re: [Caml-list] A confusing module question

[Jeremy Yallop]

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

Re: A confusing module question

[Zheng Li]

"Yaron Minsky" <yminsky@gmail.com> writes:
> 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?

OCaml distinguish "type representation" from "type equation", you may
want to check the "module type" section of the manual for the
definitions.

Now consider the example:

module type S = sig
   type exposed_t = {foo : int}
   type t = exposed_t
end

We shouldn't expect type exposed_t and type t to be semantically
equivelent, as

module type S = sig
   type exposed_t = {foo : int}
   type t = {foo : int} (* both syntactically and semantically invalid *)
end

Notice the problem here: the constructors ("foo" here) of type
representations are _nominally_ and _exclusive_ bound, which leads to
the fact that any type equivelences can only be defined through type
equations. Though we can define as many type equivelences (anywhere) as
we want, you won't be able to define a single identical type
represetation. In other words, type representation is _principle_ and
type equation isn't. So we shouldn't expect them to be _exchangable_
just because of type arithmetic.

Back to the example, module type S requires a type representation
exposed_t and it's type equivelence t. If given

module M:S = struct
  type t = {foo : int}
  type exposed_t = t
end

The compiler will fail to find exposed_t has any kind of "representation"
and t is not a type equivelence of anyone. You can re-export exposed_t's
representation as 

module M:S = struct
  type t = {foo: int}
  type exposed_t = t = {foo: int}
end

HTH.

-- 
Zheng Li
http://www.pps.jussieu.fr/~li

Re: [Caml-list] A confusing module question

[Keiko Nakata]

From: "Yaron Minsky" <yminsky@gmail.com>

> 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:
> 
> module type S = sig type t end
> 
> module M :
> sig
>   type exposed_t = { foo : int }
>   include S with type t = exposed_t
> end =
> struct
>   type t = { foo : int }
>   type exposed_t = t
> end
> 
> module N :
> sig
>   type exposed_t = { foo : int }
>   include S with type t = exposed_t
> end =
> struct
>   type exposed_t = { foo : int }
>   type t = exposed_t
> end

I agree with you. 
I understand why N fails according to the language specification,
but I still do not understand why it should fail, or what is useful 
about this behavior when programming with.

Best,
Keiko