Recursive Module Playground

Question: does the elaboration of module expressions always produce a term with type of kind $\star$ ? Question: can we use Derek’s double vision solution A Type System for Recursive Modules (two pass checking + internal/external view tagging)

A minimal example of double vision problem

module rec X : sig 
  module A : sig type t end 
  module B : sig 
	val g : X.A.t -> X.A.t 
  end 
end = struct 
  module A = struct 
    type t = int 
    let f (x : t) = X.B.g (x + 1) (* Error 1 *) 
    let z = let y = X.B.g 42 in y + 5 (* Error 2 *) 
  end 
  module B = struct 
    let g (x : X.A.t) = x 
  end
end

The module typing (without identity tagging):

This is modified form of Derek’s method, as we try to avoid using the forward declaration signature

---

First pass, compute the recursive signature by static parts of the module expression

module rec X : sig 
  module A : sig type t end 
  module B : sig 
	val g : X.A.t -> X.A.t 
  end 
end

[First pass] we get Approx is
\alpha. sig
  module A : sig type t = alpha end
  module B : sig end
end

[Second pass] we are checking in the context of:
alpha, X : sig
  module A : sig type t = alpha end
  module B : sig end
end |- ... :
\beta. sig
	sig type t = beta end
	sig val g: X.A.t -> X.A.t end 
	<--- problem: at this point X.A.t cannot be retrieved from C
	<--- we don't have the M-type-typedef-path rule?
end

Assuming a typing path rule, we get:
alpha, X : ... |- ... :
\beta. sig
	sig type t = beta end
	sig val g: alpha -> alpha end 
end

so the overall rec signature is:

  exists (beta : * -> *).
     forall (alpha : *). sig
        sig type t = beta(alpha) end
        sig val  g = alpha -> alpha end
     end
        
       


module rec X : sig 
    type u = X.t
    type t = X.u
end


[First pass] we get Approx is
\alpha1 alpha2. sig type t = alpha1, u = alpha2 end

[Second pass] we are checking in the context of:
alpha1, alpha2, 
X : sig type t = alpha1, u = alpha2 end 
|- ... :
sig
	sig type t = alpha2 end
	sig type u = alpha1 end 
end

?

mu (X : *). sig 
  type t = X.u
  type u = X.t
end

and the second pass will be a similar formalization like applicative functors (but actually no, since we still need path information), by assuming the (approximated) recursive signature is known

$$\frac{\begin{array}{c}\Gamma {⊢}_X\text{Approx}(\overline{S}):\lambda \overline{\alpha }.{\mathcal{C}}_{\text{approx}}\\ \Gamma ,\overline{\alpha },(X:{\mathcal{C}}_{\text{approx}})){⊢}_X\overline{S}:\lambda \overline{\beta }.\mathcal{C}\end{array}}{\Gamma ⊢\text{rec }X.\overline{S}:\mu (X:\star ).{\exists }^{▽}\overline{(\beta :\star \to \star )}.\forall \overline{(\alpha :\star )}.\mathcal{C}[\overline{\beta }\mapsto \overline{{\beta }^{\prime }(\overline{\alpha })}]}\text{M-Typ-Sig-Rec}$$

• for the second premise we are not intending to use the path $X$, should be refined?

To see: later when checking module expressions, how the skolemization will be treated, we need to finetune the rules here so that the modules and signature elaborations can coincide

---

What we do for elaborating rec module expressions?

$$\frac{\begin{array}{c}\Gamma {⊢}_X\text{Approx}(\overline{S}):\lambda \overline{\alpha }.{\mathcal{C}}_{\text{approx}}\\ \Gamma ,\overline{\alpha },(X:{\mathcal{C}}_{\text{approx}})){⊢}_X\overline{S}:\lambda \overline{\beta }.\mathcal{C}\end{array}}{\Gamma ⊢\text{rec }(X:\overline{S}).\text{struct }\overline{\mathcal{D}}\text{ end}:\mu (X:\star ).{\exists }^{▽}\overline{(\beta :\star \to \star )}.\forall \overline{(\alpha :\star )}.\mathcal{C}[\overline{\beta }\mapsto \overline{{\beta }^{\prime }(\overline{\alpha })}]}\text{M-Typ-Sig-Rec}$$

A concern to soundness is: whether this strengthening? weakening? that: $\Gamma ,\overline{\alpha },(X:{\mathcal{C}}_{\text{approx}})⊢\overline{S}:\lambda \overline{\beta }.\mathcal{C}$ vs. (the actual, coinductive?) $\Gamma ,\overline{\alpha },(X:\mathcal{C})⊢\overline{S}:\lambda \overline{\beta }.\mathcal{C}$

• which requires $\mathcal{C}<:{\mathcal{C}}_{\text{approx}}$, however, ${\mathcal{C}}_{\text{approx}}$ is more abstract than $\mathcal{C}$, so we should not drop type definitions as Leroy did? is sound and to what extent incomplete

---

So far, we haven’t solved the double vision problem, but we can follow the elaboration in A Type System for Recursive Modules to expose external and internal views?

---

mu (X : *) . {
  A = {
	t_t = ⟨⟨ Int ⟩⟩
	v_f = \(x : ⟨⟨ Int ⟩⟩). X.B.g (x + 1)
  }
  B = sig val g : X.A.t -> ?
}


where ⟨⟨ Int ⟩⟩ : ⋆ = ∀(φ : ⋆ → ⋆). φ Int → φ Int




{ l_t = ⟨⟨ Int ⟩⟩
  l_f = \(x : ⟨⟨ Int ⟩⟩). 


}


where ⟨⟨ Int ⟩⟩ : ⋆ = ∀(φ : ⋆ → ⋆). φ Int → φ Int

Question: are existentials required to lift out of mu binders? (maybe due to the need of functor application?) (or, with equi-recursive types, they are just equal to existentials (in unfolded form))

References:

(from Retrofitting and strengthening the ML module system)

first class modules have to be generative functors?

avoidance can account for many mechanisms (e.g. shadowing)

zipML

• core idea: if a field is avoided, you must find an alias … s.t.

• no complex stuff

• potential for scale? (with applicative functor)

• best effort type checking: module rec should subsume module

  • whether Approx(type t = Int) = (type t), depends on “best effort”
  • constraint resolution