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 non-matching 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 diff-file 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 ocaml-3.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 promote-patch

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:


      -use-functors

enables only the `functor with arg type' extension.


      -use-sigcalc

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 lua-interpreter 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 lua-interpreter 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 lua-ml-20040721.tar.gz is here.
Unpack the source of the lua interpreter:


      tar xzf lua-ml-20040721.tar.gz

and apply the patch in the newly created directory lua-ml:


      cd lua-ml
      zcat  luap-20040721.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 Type-Safe, Separately Compiled, Extensible Interpreter. from http://www.eecs.harvard.edu/~nr/pubs/, October 2003.

This document was translated from L^AT_EX by H^EV^EA.