Recursive modules for programming

Recently, much work has been devoted to investigating extensions with recursion of the ML module system. Two important issues involved are type checking and initialization. Crary, Harper and Puri [3], Russo [23], and Dreyer [5] have given type theoretic accounts for recursive modules. Boudol [1], Hirschowitz and Leroy [11], and Dreyer [4] have investigated type systems which guarantee well-formedness of recursive modules, ensuring that initialization of recursive modules will not attempt to access not-yetevaluated values.

todo The second half, regarding well-formedness and initialization has not been reviewed

Privacy & Intimacy - double vision?

Important feature: no requirement on annotations

They do support fine grained sealing within recursive sub modules

• todo Question: do the two examples they present can be encoded in ours?
  • i think so? module rec ... and ... vs module rec .. : struct M1 M2... end

Formalism

• Syntax: struct (Z) D1 . . . Dn end vs. our rec X: S = M, where M can be not just a structure

• To obtain a decidable type system, we impose a first-order structure restriction that requires functors 1) not to take functors as argument, 2) nor to access sub-modules of arguments.

• We need to check: Trivata is shallow checking lookup:

The look-up judgment does not hold for arbitrary module paths.

struct (Z) 
  module M1 = (functor(X : sig type t end3) →  struct 
    module M11 = struct end5 end4)2  
  module M2 = struct type t = int end6  
  module M3 = Z.M1(Z.M2)7  
end

Cyclic Definitions

Dreyer (Dreyer, 2005a) gave a theoretical account for type abstraction inside recursive modules. In particular, he investigated generative functors in the context of recursive modules, by proposing a “destination passing” interpretation of type generativity. There is a critical difference in design choices between us, with respects to type abstraction inside recursive modules. For instance, consider the two programs:

module M = (struct type t = N.t end : sig type t end) 
module N = (struct type t = M.t end : sig type t end)

and

module M = (struct type t = N.t end : sig type t = N.t end) 
module N = (struct type t = M.t end : sig type t = M.t end)  

Dreyer prohibits both programs, since, in both cases, underlying implementations of the types M.t and N.t make a cycle. We only prohibit the latter, since, according to the signatures, only the latter contains a cycle; in the former program, the types M.t and N.t are nothing more than abstract types. His choice may detect possible bugs in programs due to cyclic definitions, but results in restrictions on uses of structural types such as lists and tuples together with type abstraction5. The core language we want to support is that of Objective Caml, and we want to keep liberal uses of polymorphic variants (Garrigue, 1998) and objects, which are useful structural types supported in O’Caml.