Q: Module system and separate compilation

Q: Module system and separate compilation

[Jocelyn Serot]

Hello,

I recently switched from Caml light to CSL and have been impressed
both by the resulting speedup of my programs and the usefulness of the 
module system. Thanks to X. Leroy and all the co-designers for making 
such a tool available !..

I have a question regarding relationships between the module system and
separate file compilation. I will try to explain my pb with a (small ;-))
but hopefully significant example:

Let say i have a module defining a kind of "addition" on a (abstract)
type t. Its signature might be:

	module type Foo = sig
		type t
		val one : t
		val add : t -> t -> t
	end

I want a module that defines a (restricted) notion of multiplication
on this type t. It signature might be:
 
	module type Bar = sig
		type t
		val one : t
		val double : t -> t
	end

My goal is to use any module M that matches the signature Foo to build
an implementation for Bar. This seems a good application for functors:

	module MakeBar(M: Foo) =
		(struct
		type t = M.t
		let one = M.one
		let double x = M.add x x
	end : Bar)

Now, suppose i have an implementation for Foo. For example:

	module Foo = struct
		type t = int
		let one = 1
		let add x y = x + y
	end

All i have to do build a Bar implemtation is to apply functor:

	module Bar = MakeBar(Foo)

	open Bar
	let two = double one

If the previous (indented) phrases are written in the same file (eg: foobar.ml)
and compiled as a whole, the command
	cslc -i foobar.ml
produces the following output:

>module type Foo = sig type t val one : t val add : t -> t -> t end
>module type Bar = sig type t val one : t val double : t -> t end
>module MakeBar : functor(M : Foo) -> Bar
>module Foo : sig type t = int val one : int val add : int -> int -> int end
>module Bar : sig type t = MakeBar(Foo).t val one : t val double : t -> t end
>val two : Bar.t

That's fine (though i dont really understand why the type <t> in the last line
is <MakeBar(Foo).t> and not simply <Bar.t>..)

Now, the pb is that in general both Foo and Bar signatures (as well as 
MakeBar functor definition) may be large and i want to put them in
separate files, that is:

	(* file "foo.mli": *)
		
	type t
	val one : t
	val add : t -> t -> t

	(* file "foo.ml": *)

	type t = int
	let one = 1
	let add x y = x + y

	(* file "bar.mli": *)

	type t
	val one : t
	val double : t -> t

all these files compiles (cslc xxx.ml[i]) and produce corresponding .cmi and
.cmo files.

Now, i suppose i have to put MakeBar def in the "bar.ml" file:

	module MakeBar(M: Foo) = (struct
		type t = M.t
		let one = M.one
		let double x = M.add x x
	end : Bar)

but this doesnt compile: CSL complains that
	"File "bar.ml", line 1, characters 18-21: Unbound module type Foo"
In the CSL HTML manual (node4.html), it is said, however that
	"When the compiler encounters a reference to a free module identifier Mod,
	 it looks in the search path for a file mod.cmi (note lowercasing of first
	 letter) and loads the compiled interface contained in that file."
In this case, the file "foo.cmi" exists !...
The same complain occurs with the Bar module type. Again the file bar.cmi
exists.

Ok, lets duplicate these sigs in the file bar.ml:

	(* file "bar.ml": *)

	module type Foo = sig type t val one : t val add : t -> t -> t end
	module type Bar = sig type t val one : t val double : t -> t end

	module MakeBar(M: Foo) = (struct
		type t = M.t
		let one = M.one
		let double x = M.add x x
	end : Bar)

But CSL now complains that:

"The implementation bar.ml does not match the interface bar.cmi:
The field `double' is required but not provided
The field `one' is required but not provided
The field `t' is required but not provided"

The only solution i found is then to rewrite to write bar.mli as:

	(* file bar.mli *)
	
	module type Bar = sig
		type t
		val one : t
		val double : t -> t
	end

But this seems contradictory with the fact that, as stated in node2.12 of
CSL html manual

"A compilation unit behaves roughly as the module definition
	module unit-name : sig unit-interface end = struct unit-implementation end"

Am i missing sth important, or even misusing the module system ?..
In particular, the need for textual duplication of the Foo and Bar signatures
(which have written and compiled in separate files) in the file defining
the functor seems a bit annoying..

Sorry for being so long, and thanks in advance for your help

J. Serot
--
E-mail: Jocelyn.Serot@lasmea.univ-bpclermont.fr .............................
S-mail: LASMEA - URA 1793 CNRS, Universite Blaise Pascal, 63177 Aubiere cedex
Tel: (33) 73.40.73.30 - Fax: (33) 73.40.72.62 ...............................
.... http://wwwlasmea.univ-bpclermont.fr/Personnel/Jocelyn.Serot/Welcome.html

Re: Q: Module system and separate compilation

[Wolfgang Lux]

> [Definition of module signature omitted]
> 
> My goal is to use any module M that matches the signature Foo to build
> an implementation for Bar. This seems a good application for functors:
> 
> 	module MakeBar(M: Foo) =
> 		(struct
> 		type t = M.t
> 		let one = M.one
> 		let double x = M.add x x
> 	end : Bar)
> 
> Now, suppose i have an implementation for Foo. For example:
> 
> [Definition of Foo omitted]
> 
> All i have to do build a Bar implemtation is to apply functor:
> 
> 	module Bar = MakeBar(Foo)
> 
> 	open Bar
> 	let two = double one
> 
> If the previous (indented) phrases are written in the same file (eg: foobar.ml)
> and compiled as a whole, the command
> 	cslc -i foobar.ml
> produces the following output:
> 
> >module type Foo = sig type t val one : t val add : t -> t -> t end
> >module type Bar = sig type t val one : t val double : t -> t end
> >module MakeBar : functor(M : Foo) -> Bar
> >module Foo : sig type t = int val one : int val add : int -> int -> int end
> >module Bar : sig type t = MakeBar(Foo).t val one : t val double : t -> t end
> >val two : Bar.t
> 
> That's fine (though i dont really understand why the type <t> in the last line
> is <MakeBar(Foo).t> and not simply <Bar.t>..)

This is because MakeBar(Foo).t provides more information about the
type t than simply Bar.t. If it simply were Bar.t, two following two
functor applications would yield incompatible types:

    Bar = MakeBar(Foo).t
    Bar' = MakeBar(Foo).t

i.e, the types Bar.t and Bar'.t would be incompatible. But the type
MakeBar(Foo).t gives you enough information to see that the type
result from the same functor application and CSL will regard them as
compatible types. If you are interested in details, I would recommend
reading X.Leroy papers "Manifest types, modules, and separate
compilation" and "Applicative Functors and Higher Order Modules",
which describe the ideas behind CSL's modules (but in the context of
SML structures). They are available as:

    http://pauillac.inria.fr/~xleroy/publi/manifest-types-popl.dvi.gz
    http://pauillac.inria.fr/~xleroy/publi/applicative-functors.dvi.gz

> 
> Now, the pb is that in general both Foo and Bar signatures (as well as 
> MakeBar functor definition) may be large and i want to put them in
> separate files, that is:
> 
> [Obvious contents omitted :-)]
> 
> all these files compiles (cslc xxx.ml[i]) and produce corresponding .cmi and
> .cmo files.
> 
> Now, i suppose i have to put MakeBar def in the "bar.ml" file:
> 
> 	module MakeBar(M: Foo) = (struct
> 		type t = M.t
> 		let one = M.one
> 		let double x = M.add x x
> 	end : Bar)
> 
> [ Remaining redefinition deleted]
> 

What are defining here is not the module MakeBar, but a module

    Bar.MakeBar

i.e. a nested module!

> "A compilation unit behaves roughly as the module definition
> 	module unit-name : sig unit-interface end = struct unit-implementation end"
> 
> Am i missing sth important, or even misusing the module system ?..

So what you are actually going to write into bar.ml is the following:

    type t = Foo.t
    let one = Foo.one
    let double x = M.add x x

This will yield a structure that matches the signature defined in
"bar.mli". 

Now you say: "I have defined a functor and you give me a structure".
But wait the functor is still there; but it is now hidden in the
filesystem.

If you read on in the section about compilation units, it says that
the module expression will be evaluated in an initial environment
where all the interfaces available in the search path are defined. You
could read this as well as follows: The implementation file is the
body of a functor, whose parameters are all the modules available in
the search path, i.e. given the interfaces Bar, Foobar, etc. are in
the search path, the compilation unit Foo is interpreted as:

    module Foo(Bar : Bar)(Foobar : Foobar)... :
      sig <contents of foo.mli> end =
      struct <contents of foo.ml> end

Seen that way functor application will take place when the program is
linked together from the separatly compiled modules.


Regards
Wolfgang

----
Wolfgang Lux
WZH Heidelberg, IBM Germany             Internet: lux@heidelbg.ibm.com
+49-6221-59-4546                        VNET:     LUX at HEIDELBG
+49-6221-59-3500 (fax)	                EARN:     LUX at DHDIBMIP

Re: Module system and separate compilation

[Christian Boos]

[-- Warning: decoded text below may be mangled, UTF-8 assumed --]
[-- Attachment #1: Type: text/plain, Size: 3162 bytes --]



[French translation below]

	Hello, 

Here's some comments about your questions :

Jocelyn Serot writes:
 > 
 > (...)
 > 	(* file "bar.ml": *)
 > 
 > 	module type Foo = sig type t val one : t val add : t -> t -> t end
 > 	module type Bar = sig type t val one : t val double : t -> t end
 > 
 > 	module MakeBar(M: Foo) = (struct
 > 		type t = M.t
 > 		let one = M.one
 > 		let double x = M.add x x
 > 	end : Bar)
 > 
 > (...)
 >
 > 	(* file bar.mli *)
 > 	
 > 	module type Bar = sig
 > 		type t
 > 		val one : t
 > 		val double : t -> t
 > 	end

[1] This is the right way. To do the best, you should add :

	'module type Foo = sig ... end '
and	'module MakeBar (M : Foo) : Bar'

in the file "bar.mli".


 > 
 > But this seems contradictory with the fact that, as stated in node2.12 of
 > CSL html manual
 > 
 > "A compilation unit behaves roughly as the module definition
 > 	module unit-name : sig unit-interface end = struct unit-implementation end"
 > 

[2] There's no contradiction. In  the file "foo.mli",  a module Foo is
implicitly declared. This module has type 'sig type t val one ... end'
which is a   sort of "anonymous"  module  type.  In  no way  have  you
declared a module type named Foo, as expected in the "bar.ml" file.


 > Am i missing sth important, or even misusing the module system ?..
 > In particular, the need for textual duplication of the Foo and Bar signatures
 > (which have written and compiled in separate files) in the file defining
 > the functor seems a bit annoying..

[3] I agree with   you that this  duplication  is annoying.  It's only
justification is that a 'module type XXX = sig ... end' statement in a
.mli is a  module type declaration, and that  the same  statement in a
.ml is a  module type definition.  This  allows one to define abstract
module types, for example.  I suggest that the compiler be modified to
automatically  generate module  type  definition   from  module   type
declaration when this declaration is not an abstract one.
  This would eliminate the need for duplication in most cases.


-- Christian Boos.

------------------------------------------------------------------

Bonjour,

Je peux faire quelques commentaires sur vos questions.

[1] C'est effectivement comme cela qu'il faut faire.  Pour bien faire,
il faudrait  encore rajouter la déclaration du  type de module 'module
type Foo = sig ... end '  et celle foncteur  'MakeBar' dans le fichier
bar.mli:

	module MakeBar (M : Foo) : Bar


[2] Non, je ne vois pas la contradiction : le fichier "foo.mli" declare
un module  Foo,  qui se  trouve   avoir un type  (sig  type  t val one
... end), ce type n'étant pas nommé (il n'y a  pas création de 'module
type Foo = sig ... end').


[3] Oui,  alors  là d'accord. Le  fait de  devoir recopier les 'module
type' dans les implémentations est pénible et source d'erreur. Cela se
justifie parceque dans le .mli il s'agit de déclaration et dans le .ml
d'une définition. Cette séparation  permet par exemple de déclarer des
types de modules abstraits  ('module type Foo'). Mais  la plus part du
temps, il serait plus pratique de générer la définition à partir de la
déclaration du .mli.