Tony's Wiki

What is a recursive module?

4 min read

Section 2 - Type-theoretic Framework

  • Singleton kinds
    • note that the syntax constructor (applied to monotypes) is generalized to a certain class of well-formed kinds (with proper restriction on positivity and dependent sum kinds)
  • value restriction via valuable for recursive functions
  • contraction condition for equi-recursive type constuctors

2.2 The Structure Calculus

  • module (or structures s) M = [c, e] for constructors and expressions
  • signatures S = [alpha:k, sigma] for kinds and types (e has type sigma[alpha/k])

Related work: higher order modules can be reduced to flattened structure calculus

Section 3 - Opaque Recursive Modules

  • We get an opaque encoding for free in the core language
  • It is not enough for the purpose of programming mutually recursive modules
    • The decl expr mutually recursive examples

Section 4 - Transparent Recursive Modules

What we need is a means of propagating the type equations, such that exp is known to be Decl.exp

Solution: Recursive Dependent Signature - making what is necessary transparent e.g. make t = ... | List.t part of the contract

Section 4.1 Functors and Separate Compilation

  • in order to achieve separate compilation, we can write functors and then gluing the functors by instantiating them in a recursive structure binding
  • However, by checking closely, for sake of in-opacity, we are forced to provide recursively dependent signature for Expr and Decl, specifying the other module
    • Code may be separate, type may not
  • See Section 5.1 for relaxation

Section 4.2 Formalization

It can be shown, for recursive dependent signature rho s. S

  • we have
    • intro/elim rules for M : rho s. S auto unfold/folding
    • well-formed rules enforcing static components in S to be fully transparent
  • we show
    • rho s. S can be encoded by a recursive type constructor
    • the rules above follow from the definition, need not be primitive

Section 4.3 Opacity revisited

From the rules, we can see that the only part that is recursive is

  • static-on-static (types on types)
  • dynamic-on-dynamic (terms on types) (by redirecting to Fst s)

I guess the authors’s point here is that, though it is possible to avoid static-on-static with other means, this will be beyond the paper’s concern (on ML modules, statically typed programming …)

Not quite true, see Opacity Revisited in Recursive Modules

Corrected view:

  • see the two examples, where in the opaque version we use Decl.make_val but with transparent signature we can directly use Decl.VAL constructor

There goes: One can always program opaquely (i.e., without any type sharing information) if one is willing to incur mediating function calls between types that are actually equal. Tools for supplying type equality information, such as sharing [15], translucent sums [9,13], and recursively dependent signatures, serve only to improve performance.

Section 5 - External Language

5.1 Elaboration

5.2 Type Checking

structure rec A : ASIG(A) =
  struct ... body ... end
  • Intended checking: body (actual implementation) has type rho s. ASIG(s) under assumption that A has type rho s. ASIG(s)
  • Appealing checking:
    1. rho s. ASIG(s) is well-formed
    2. the structure definition has type ASIG(A) under assumption that A has type ASIG(A) --- easier to check
  • Authors show: the two are equivalent

5.3 Iso- vs. Equi- constructors

Conjecture: equi are not essentially necessary

Extended Reading

Graph View

Backlinks