Message-Id: <9603201349.AA31008@idse.heidelbg.ibm.com>
To: Jocelyn Serot <Jocelyn.Serot@lasmea.univ-bpclermont.fr>
Subject: Re: Q: Module system and separate compilation
In-Reply-To: (Your message of Tue, 19 Mar 96 10:29:48 T.)
<199603190931.KAA11239@nez-perce.inria.fr>
Date: Wed, 20 Mar 96 14:49:45 +0100
From: Wolfgang Lux <lux@heidelbg.ibm.com>
> [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