A Type System for Recursive Modules

A Type System for Recursive Modules Derek Dryer, ICFP’07

Previous work: RTG This work: RMC

RMC is elaborated in to RTG

“The proper handling of double vision seems to demand the use of a two-pass algorithm for typechecking certain kinds of modules the first (“static”) pass computes only the type components of the module, while the second pass typechecks the full module.” (Dreyer, p. 290)

Section 2 - The Double Vision Problem

• rec (X: sig) mod : the recursive module construct
  • where sig is the forward declaration signature
• rec (X) sig: the recursive dependent signature
  • signatures can refer recursively to the modules that inhabit them
    • not to the signature itself

2.1 Motivating Example

Figure 1 -

• fibration in ML programming S_A and S_B

2.2 Existing Approaches

• Section 4.3 Opacity revisited - trouble with opacity
  • Crary et. al: simply to restrict the forward declaration signature of a recursive module to be transparent.
  • i.e. definitions of A.t, B.u needs to be transparent issue of transparency in ZipML + Recursive modules
• Russo (2001) Moscow ML Recursive structures for Standard ML
  • Although Russo does not explicitly require forward declarations to be transparent, other restrictions of his system implicitly do.
  • It is worth noting that Russo makes an exception for types that are defined by an algebraic datatype definition.
• Leroy (2003) Manifest types, modules and separate compilation
  • no formal account
  • cannot deal with internally defined types by transparent bindings
• Nakata and Garrigue (2006)
  • different from other proposals: no requirement for forward declarations
• Derek’s thesis (2005)
  • TILT + extension: complex and ad hoc
  • motivation for this work

2.3 The RTG Type System

Source of double vision:

• requirement that one can only create a new abstract type name if one supplies a definition along with it
  • the joining of type creation + type definition → double vision problem
  • which is just trying to define an abstract type t in a scope where a name of that type already exists X.A.t
  • What’s the case in OCaml?
• Figure 2 is the encoding of Figure 1
  • Require what extension of syntax in Figure 1?
    • to really compare what is different

Section 3 Overview of RMC Typechecking

3.1 Typechecking Recursive and Sealed Modules

inspirations unlike transparent existentials in $M^{\omega }$, here the “transparent” type variables are used to enable giving definitions to pre-defined names

Exercise 1

(* Exercise #1: Figure 1 with module B not sealed *)
 
structure AB = rec (X : S) struct 
  structure A :> (SA where type u = X.B.u) = struct 
    type u = X.B.u 
    type t = int 
    fun f (x:t) : u * t = 
        let val (y,z) = X.B.g(x+3) (* Error 1 *) 
        in (y,z+5) end (* Error 2 *) 
    ... 
  end 
  
  structure B = struct 
    type t = X.A.t 
    type u = bool 
    fun g (x:t) : u * t = ... X.A.f(...) ... 
    ... 
  end
end

translates to RTG

new a ↑ T in
  let AB = rec (X : Σ) [
    A = def a := int in
          [ u = bool, t = int, f = ... ] : ΣA,
    B =   [ t = a, u = bool, g = ...  ]  : ΣB
  ] in ...
where

ΣA = [ u : bool, t : a, f : a -> bool * a ]
ΣB = [ t : a, u : bool, g : a -> bool * a ]
Σ = [ A : ΣA, B : ΣB ]

Exercise 2

Assume this is well typed:

rec (X : sig structure A : SOME_SIG end) struct
   structure A = SOME_MOD
end

• X , A not free in SOME_SIG
• We get conditions: SOME_MOD : SOME_SIG

(* Example 1 : OK *)
rec (X : sig structure A : SOME_SIG end) struct
   structure A :> SOME_SIG = SOME_MOD
end
 
(* Example 2 : OK *)
rec (X : sig structure A : SOME_SIG end) struct
	 structure B :> SOME_SIG = SOME_MOD; structure A = B
end
 
(* Example 3 : is not necessarily, (suggest should not) *)
rec (X : sig structure A : SOME_SIG end) struct
	 structure B = SOME_MOD;
	 (* Key difference: SOME_MOD is not under sealing any more
		  say, SOME_MOD contains a defintion `t = int`
		  B.t is transparently equal to `int`
      *)
	 structure A :> SOME_SIG = B
	 (* If SOME_SIG says that `type t` is abstract,
	    then the type system is supposed to hide the fact that `A.t = int`
	    
	    THE LEAK!!
	    Although `A` is sealed, the full transparent definition 
	    of the structure still exists in B
	    
	    will be detected as a path clash (abstrct vs. concrete)
	    and a source of unsoundness
	 *)
end

The existence of the unconstrained name B inside the recursive definition provides an alias that bypasses the sealing of A. If the recursive body later uses B, it can access the internal concrete representation of what should be an abstract type when viewed through A. This violates the integrity of the abstract type X.A.t, which is essential for type soundness in a recursive setting

A more detailed explanation: Double Vision Problem - Abstract Types vs. Unconstrained Aliases in Recursive Modules

3.2 Forward Declarations, Not Signature Ascriptions

• Crary et al.’s is the only proposal to treat recursive modules as fixed points explicitly.

• Others treat forward declaration as the principal exported signature of the recursive module itself

• Russo’s Moscow ML, treat it as only a forward declaration, not a sealing signature

  • can be recovered by rec (X:sig) (mod :> sig) to recover the sealed version

• RMC follows Russo’s approach

3.3 Computing the Type Components of a Module

• full equi-recursive type, allow transparent type cycles, not understood, requires equi-recursive type and higher kinds
• Cyclic type definitions in OCaml with opaque sealing
• This work: needs to go through at lease one component that is defined by a datatype declaration

This policy has the advantage that recursive modules do not introduce any new forms of (equi-)recursive type definitions that are not already expressible in the underlying core language of ML—they just provide the ability to decompose ML’s existing forms of recursive type definitions into modular components

• which creates some restrictions (TOCHECK)
• but still useful to encode practicals Okasaki’s bootstrapped heap example

3.5 Recursively Dependent Signatures

The basic goal is to check that the rds does not contain any cyclic transparent type specifications, whose presence would demand support for equirecursive types.

This is in stark contrast to Crary et al.’s original proposal for rds’s, which requires them to be fully transparent specifically so that they can be implemented internally using equi-recursive types. No subsequent proposal has followed their approach.

Section 4.

• Evidence translation is just the module typing judgement appended with $⇝M$, signature matching appended with $⇝F$ (the internal language functor F, coercing source signature to target signature)

TODO

• Check examples in Section 2 - The Double Vision Problem again
• Check related work in detail