Calculating with Signatures
Jürgen Pfitzenmaier
26. Juli 2004
1 Introduction
This document describes an extension to the OCaml language.
The idea for this extension comes from Norman Ramsey[Ram01].
He saw the need for additional constructs in the OCaml signature language
and gave examples for their usage. He didn't give an implementation but
showed in [Ram01] and [Ram03] how to program
without these extensions but with additional effort.
I found the suggestions useful and wrote my own implementation.
Its syntax differs slightly from that in [Ram01] to make
it easier to use. Experience with an earlier implementation showed that
``lazy module types'' are necessary as a further extension.
2 Constraints for Functors
We can add constraints to the argument or the result of a functor after
forming the functor. This does not effect the original functor but only
a copy of it.
module type A = sig type a end
module type B = sig type b end
module type F = functor(A1 : A) > B
module type F1 = F with arg type a = int
module type F2 = F with res type b = char;;
OCaml treats the last two declarations as
module type F1 = functor (A1 : sig type a = int end) > sig type b end
module type F2 = functor (A1 : sig type a end) > sig type b = char end
arg and res are not keywords but they are the only identifiers
allowed between the keywords with and type. Therefor
arg and res can be used in other places as normal identifiers.
3 Union of Signatures
We can add two disjoint signatures:
module type A = sig type a end
module type B = sig type b end
module type U = A sig union B;;
OCaml treats the last declaration as
module type U = sig type a type b end
In the next example the signatures are not disjoint. The types
A.t and C.t
have equal names but they are not connected by a constraint.
module type A = sig type t and a end
module type B = sig type t and b end
module type U = A sig union B;; (* error *)
This is a potential error and the compiler gives a warning message:
Warning: the two types t are literally equal but not connected by a constraint
We must add a constraint saying that the two types are to be
considered equal:
module type A = sig type t and a end
module type B = sig type t and b end
module type U = (X : A) sig union (B with type t = X.t);;
OCaml treats the last declaration as:
module type U = sig type t and a and b end
4 Lazy functor arguments
We can see the need for lazy functor arguments in the next example (from the patched lua interpreter;
see below under more examples).
We want to express a dependency between two arguments of the same functor while these arguments themselves are functors.
To do this we need access to the argument or result module type of a functor. This is given by using
functor arg(F) or functor res(F) inside a constraint like in line 12:
1 module type Core = sig
2 type state
3 end
4 module type BARECODE =
5 functor (C : Core) > sig
6 val init : C.state > unit
7 end
8
9 module W = struct
10 module F =
11 functor (C1 : BARECODE) >
12 functor (C2 : BARECODE with arg type state = functor arg(C1).state) >
13 struct
14 end;;
15 end;;
Up to here everything seems fine but we can not define a module by applying the
functor W.F while imposing constraints on its functor arguments
(mind the use of double parentheses in this example):
16 module CC = functor (C : Core) > struct let init _ = () end;;
17 module Fimpl = W.F ( (C1 : BARECODE with arg type state = int) )
18 ( (C2 : BARECODE with arg type state = int) );;
The compiler complains about nonmatching type declarations:
Signature mismatch:
Modules do not match:
functor (C : sig type state = int end) >
sig val init : C.state > unit end
is not included in
BARECODE
Type declarations do not match:
type state
is not included in
type state = int
The reason for this error is the contravariance of the functor argument:
The C1 in line 17 should be a supertype of the C1 in line 11.
The solution is to add a constraint for the first functor argument
to make the C1 in line 11 less general.
But this constraint must respect the constraint on C2 in line 12.
This can only be expressed by a circular dependency between C1 and C2
and marking the name of the second functor argument as lazy:
module W = struct
module F =
functor (C1 : BARECODE) with lazy (C2) (arg type state = functor arg(C2).state) >
functor (C2 : BARECODE with arg type state = functor arg(C1).state) >
struct
end;;
end;;
module CC = functor (C : Core) > struct let init x = () end;;
module Fimpl = W.F ( (CC : BARECODE with arg type state = int) )
( (CC : BARECODE with arg type state = int) );;
A functor with a lazy module name must be fully applied.
module Fpart = W.F ( (CC : BARECODE with arg type state = int) );;
This partial application raises an error message:
This functor application depends on the following unresolved lazy names:
[C2]
This limitation will be lifted in the next version.
5 Renaming
We can also rename an item in a signature.
Take the following module type:
module type A = sig
type t
val f : unit > int
module type B = sig
type x
end
end;;
Rename a type in a module type:
module type A2 = sig rename (A; type t = tnew);;
to get:
module type A2 =
sig type tnew val f : unit > int module type B = sig type x end end
Rename a type deep inside:
module type A3 = sig rename (A; type B.x = u);;
to get:
module type A3 =
sig type t val f : unit > int module type B = sig type u end end
We can rename not only types but also values:
module type A4 = sig rename (A; val f = fnew);;
to get:
module type A4 =
sig type t val fnew : unit > int module type B = sig type x end end
We can rename several items at once:
module type A5 = sig rename (A; type t = tnew; val f = fnew);;
to get:
module type A5 =
sig type tnew val fnew : unit > int module type B = sig type x end end
The requests for renaming are separated
by semicolons. The requests are ordered from left to right with leftmost
renaming taking place first. As long as the requests do not overlap, the
order in which they appear is not important.
6 Installation and Usage
Get the patches as a gzipped difffile from here.
Unpack the diff with
gzip d sigpatch.diff.gz
Go to a directory where a fresh OCaml 3.08.0 distribution lives
and apply the patch
cd ocaml3.08.0
patch p1 < sigpatch.diff
Run configure as usual but use a different directory for installation.
This way you avoid overwriting your existing OCaml binaries.
./configure prefix yournewdirectory
Promote the patch to get the dependencies right:
make promotepatch
Then compile and install the patched OCaml as usual:
make world
make install
ocaml, ocamlc and ocamldep all use 2 flags to enable the new extensions:
usefunctors
enables only the `functor with arg type' extension.
usesigcalc
enables the `sig union', `with lazy' and renaming extensions.
You must use both flags to enable all of the extensions.
7 More Examples
The first real application for these extensions is the the luainterpreter from
the download area of www.cminusminus.org. My
patch for this interpreter implements most of the changes
Ramsey [Ram01] wanted to see.
The patch is not kept up to date on a daily basis. You have to use the
version of the luainterpreter with roughly the same date stamp as the patch.
Slightly newer versions of the lua interpreter should be ok as it is
only slowly evolving. The patch for for luaml20040721.tar.gz is here.
Unpack the source of the lua interpreter:
tar xzf luaml20040721.tar.gz
and apply the patch in the newly created directory luaml:
cd luaml
zcat luap20040721.diff.gz  patch p1
then build the lua interpreter as usual:
make f Makefile.alone depend
make f Makefile.alone all
8 Outlook
Some features will be implemented in the near future:

deleting of signature items
 allow lazy module names in partial functor application
9 Bugs and Limitations
The implementation is still in an experimental state and contains bugs
and/or undocumented behaviour. Among them are the following:

the code is a prototype. it needs cleaning/rewriting
 the lookup of names may be inconsistent
 needs better documentation
 needs better error messages
 some failures during renaming are not reported
 while renaming a type not every use of the type is changed
10 Contact
Send comments to pfitzen@pfitzenmaier.de
Please mention the version of the patch (as given by: ocamlc v) when reporting bugs
and send a small example that produces the offending behaviour.
References
 [Ram01]

Norman Ramsey.
Toward a Calculus of Signatures.
from http://www.eecs.harvard.edu/
~
nr/, October 2001.
 [Ram03]

Norman Ramsey.
ML Module Mania: A TypeSafe, Separately Compiled, Extensible
Interpreter.
from http://www.eecs.harvard.edu/
~
nr/pubs/, October 2003.
This document was translated from L^{A}T_{E}X by
H^{E}V^{E}A.