From frisch@clipper.ens.fr Sun Jan 21 18:39:19 2001
Date: Sun, 7 Jan 2001 01:20:42 +0100 (MET)
From: Alain Frisch
To: Caml list
Subject: first class modules (was: alternative module systems)
Hello,
a few month ago, Markus Mottl pointed to this mailing list the work by
Claudio Russo on first class modules. There were no answer about plans to
implement such a system for OCaml.
I also have the feeling that there should be no problem to implement first
class "packaged" modules à la Russo for OCaml. The idea is to keep the
core and module langages distinct but provide bridges between them.
The type algebra is enriched with the syntax < S > where S is a module
type.
(pack (m:S)) is a core expression of core type < S > when m is a module
of module type S.
(open a1 as X : S in a2) has the natural meaning; a1 must have type
< S >, X is bound in a2 to the module packaged by a1.
As I see it, the main issue is the unification problem < S > = < T >. I
implemented as a quick and dirty hack such a system, where < S > and < T
> unify if and only if S and T represent syntactically the same path. It
is the simpliest solution, but it is general enough (by defining named
module types and putting some explicit coercions). It should be possible
to check that S and T are structurally compatible.
Here is the classical example of arrays of size 2^n:
========================================================================
module type ARRAY = sig
type 'a array
val init: 'a -> 'a array
val sub: 'a array -> int -> 'a
val update : 'a array -> int -> 'a -> 'a array
end
module ArrayZero = struct
type 'a array = 'a
let init x = x
let sub a i = a
let update a i x = x
end
module ArraySucc (A:ARRAY) = struct
type 'a array = 'a A.array * 'a A.array
let init x =
(A.init x, A.init x)
let sub (l,r) i =
if i mod 2 = 0 then A.sub l (i/2) else A.sub r (i/2)
let update (l,r) i x =
if i mod 2 = 0 then (A.update l (i/2) x, r) else (l, A.update r (i/2)
x)
end
let rec array = function
| 0 -> pack (ArrayZero:ARRAY)
| n -> open array (n-1) as A : ARRAY in pack (ArraySucc(A):ARRAY)
========================================================================
The last definition yields as expected:
val array : int -> < ARRAY >
It couldn't be expressed without the extension.
Now:
======
let _ =
open (array 2) as A:ARRAY in
let a = A.init "hello" in
let a = A.update a 1 " " in
let a = A.update a 2 "world" in
let a = A.update a 3 " !\n" in
for i = 0 to 3 do print_string (A.sub a i) done
======
builds a module of "array of size 4=2^2" and use it.
Naturally, a type that makes reference to a module value can't escape
the scope where this module is visible:
======
# open (array 3) as A:ARRAY in A.init 5;;
This `let module' expression has type int A.array
In this type, the locally bound module name A escapes its scope
======
(in the first line of the error message, `let module' should read `open...')
Everything seems to work as expected for higher order modules:
=====================================
module type S = sig type t val x:t val y:t val print:t->unit end
module type T = sig type u val a:u end
module type F = functor (X:S) -> T with type u = X.t
module TAKE_x(X:S): T with type u = X.t = struct type u = X.t let a = X.x end
module TAKE_y(X:S): T with type u = X.t = struct type u = X.t let a = X.y end
module A = struct type t = int let x = 1 and y = 2 and print = print_int end
module B = struct type t = string let x= "A" and y = "B" and print = print_string end
let take_x = pack (TAKE_x : F)
let take_y = pack (TAKE_y : F)
let apply f m =
open f as TAKE : F in
open m as X : S in
let module Y = TAKE(X) in
X.print Y.a
let _ =
apply take_x (pack (A:S));
apply take_y (pack (A:S)); print_newline ();
apply take_x (pack (B:S));
apply take_y (pack (B:S)); print_newline ();
=====================================
Interesting types are:
val take_x : < F >
val take_y : < F >
val apply : < F > -> < S > -> unit
and the execution gives of course:
12
AB
(as a side effect, we get the local "open ... in ...")
Almost everything is already there in OCaml to implement easily this
system. Basically, with trivial extensions of ast, typed ast and type
expressions, for the typing, this gives something like:
(typing/typecore.ml, function type_exp):
....
| Pexp_pack m ->
let modl = !type_module env m in
let ty = newty (Tpackage modl.mod_type) in
{ exp_desc = Texp_pack(modl);
exp_loc = sexp.pexp_loc;
exp_type = ty;
exp_env = env }
| Pexp_unpack (e1, name, mty, sbody) ->
let ty = newvar() in
Ident.set_current_time ty.level;
let mty = !transl_modtype env mty in
let arg = type_expect env e1 (newty (Tpackage mty)) in
let (id, new_env) = Env.enter_module name mty env in
Ctype.init_def(Ident.current_time());
let body = type_exp new_env sbody in
begin try
Ctype.unify new_env body.exp_type ty
with Unify _ ->
raise(Error(sexp.pexp_loc, Scoping_let_module(name, body.exp_type)))
end;
{ exp_desc = Texp_unpack(arg, id, mty, body);
exp_loc = sexp.pexp_loc;
exp_type = ty;
exp_env = env }
for the conversion to lambda-code:
(bytecomp/translcore.ml, function transl_exp)
...
| Texp_pack modl ->
!transl_module Tcoerce_none None modl
| Texp_unpack (arg,id,mty,body) ->
Llet(Strict, id, transl_exp arg, transl_exp body)
and something very stupid in typing/ctype.ml for the unification:
| (Tpackage (Tmty_ident p1), Tpackage (Tmty_ident p2)) when Path.same
p1 p2 ->
update_level env t1.level t2;
t1.desc <- Tlink t2
I may have overlooked some important consequences on the type safety
properties.
Is there any theoretical work about the integration of such a system to
the OCaml module system ? Any plan to include it in a future release ?
--
Alain Frisch