contractiveness-im-example-momega-note

Im et al. non-contractive-signature example in Mω / Fωμ

This note addresses the OCaml -rectypes example from Im, Nakata, and Park 2013, and how it should be discussed in the WIP Mω paper. I did not modify the TeX source.

1. The important correction

The safest conclusion is slightly more nuanced than “Mω rejects the signature immediately.”

In the current draft, Mω relies on Fωμ as the target calculus. Fωμ permits non-contractive recursive types syntactically, but root-active types are mapped to ⊥ by the target equivalence semantics. Therefore, if the Im et al. example is elaborated all the way to the target, the bad instantiation of the abstract type constructor is exposed and the sealing/subtyping check fails.

So:

• The whole program should be rejected by Mω.
• The reason is target-level: after substituting the implementation witness for the abstract type constructor, the exported cycles become root-active and collapse to ⊥, so the implementation no longer matches the claimed interface.
• The extra source/module-level contractiveness check on exported signatures is a design choice for rejecting such interfaces early and for keeping public interfaces productive; it is not the same foundational necessity as in λ^rec_abs, whose soundness proof assumes ordinary ML sealing erasure and therefore must reject non-contractive signatures in the source calculus.

In other words, the target system already gives us a safety net. The signature-level restriction is still a good design, but its role is “interface hygiene / early rejection / predictable API semantics,” not “otherwise the target calculus becomes unsound.”

2. The Im et al. example

The paper’s example is:

module M : T = struct                    module type T = sig
  type 'a t = 'a                           type 'a t
  type s = int and u = bool                type s = s t and u = u t
  let f x = x                              val f : int -> s
  let g x = x                              val g : u -> bool
end                                      end
let h x = M.g (M.f x)
let y = h 3                              (* run-time error in old OCaml -rectypes *)

Im et al. explain the issue as follows:

• In the signature T, the cycles s = s t and u = u t appear guarded by the abstract type constructor t.
• OCaml treated them as contractive because the recursive occurrences are under t.
• But the implementation instantiates t with the identity constructor λa.a.
• Then the equations become s = s and u = u, i.e. non-contractive/root-active.
• Since s and u become structurally equivalent under the signature, M.g (M.f 3) typechecks as bool even though it applies the identity g to the integer 3 at runtime.

Their key meta-point is the sentence you noticed: non-contractive types in signatures lead to unsoundness, but non-contractive types may be allowed in modules. This is because signatures are abstractions that may later be implemented by a bad witness, whereas module bodies are concrete: once the representation is known, the type equalities can be checked against the actual definitions.

3. Step-by-step Mω view

I will write this in an intentionally paper-like style.

3.1 Elaborating the signature shape

Let the abstract type constructor in T be represented by a target variable:

α : ★ → ★        -- the abstract constructor for type 'a t

The declarations

type s = s t
type u = u t

induce recursive equations:

βs = α βs
βu = α βu

Solving them by target μ gives:

βs ↦ μβ. α β
βu ↦ μβ. α β

So the internal signature looks morally like:

∃ α : ★→★. sig
  type t = α
  type s = μβ. α β
  type u = μβ. α β
  val f : int -> μβ. α β
  val g : μβ. α β -> bool
end

This explains why s and u are equal at the abstract interface: they are both represented by the same target type expression μβ. α β.

3.2 Is μβ. α β already root-active?

This is the subtle point.

With α abstract, μβ. α β is not syntactically the obvious bad type μβ. β. Its unfolding reaches a stable head α, so if α is treated as an opaque constructor, the type looks productive.

But it is not stable under substitution: instantiating

α ↦ λα. α

turns it into

μβ. (λα. α) β  →β  μβ. β

which is root-active and therefore collapses to ⊥ in the Fωμ equivalence semantics.

This is exactly the phenomenon described in the WIP draft around the Fωμ/root-active discussion: abstract types make purely syntactic contractiveness checks fail to respect substitution.

3.3 Sealing the implementation against the signature

The implementation defines:

type 'a t = 'a
type s = int
type u = bool
let f x = x
let g x = x

So the witness for the abstract constructor is:

α = λα. α

Substituting this witness into the interface equations gives:

s_T = μβ. (λα. α) β  ≡ μβ. β ≡ ⊥
u_T = μβ. (λα. α) β  ≡ μβ. β ≡ ⊥

But the implementation provides:

s_M = int
u_M = bool
f_M : int -> int
g_M : bool -> bool

To seal M : T, the elaboration/subtyping step must show that the implementation’s concrete type components and value components match the instantiated interface. In target terms this requires at least the following equalities/typing obligations:

int  ≡ ⊥       -- for type s
bool ≡ ⊥       -- for type u
int -> int  ≤/≡  int -> ⊥
bool -> bool ≤/≡ ⊥ -> bool

These obligations fail in Fωμ. Therefore the module sealing is rejected.

This is the key difference from the source-level unsoundness in old OCaml: the Mω elaboration does not erase sealing as a mere source-level abstraction; it elaborates sealing into an explicit target package/coercion whose witness types must satisfy the target type equalities.

3.4 What if we accepted the signature alone?

If a bare signature T is accepted with abstract α, then inside that signature s and u are equal because both elaborate to μβ. α β. That is not by itself unsound. It says: any valid implementation of T must supply an α such that the required value typings are coherent.

The bad implementation with α = id is not valid, because after witness substitution the interface cycles collapse to ⊥ and no longer match int/bool.

This suggests an important distinction:

• Rejecting the signature T itself is an interface-design restriction.
• Rejecting the program module M : T = ... follows from target-level sealing/subtyping.

If the paper says “we reject the signature at elaboration time,” then it should make explicit that this is an extra well-formedness policy for exported signatures, not a consequence forced solely by Fωμ typing.

4. Signature vs module body in Mω

Your question was whether in Mω this becomes “foundationally unrelated,” so that both signatures and module bodies can have non-contracted types.

My answer:

Yes, at the target-calculus foundation level, non-contractive μ-types are not inherently unsound. Fωμ gives them a meaning by collapsing root-active types to ⊥. Therefore the target can tolerate non-contractive cycles in both module bodies and signatures, as long as all target terms are typechecked after the relevant witnesses are substituted.

But no, they are not entirely irrelevant at the module-design level:

• In module bodies, non-contractive definitions are concrete. They either collapse to ⊥ harmlessly, or fail when used in a context requiring a non-⊥ type. There is no abstract witness that can later invalidate a public promise.
• In signatures, non-contractive definitions become part of the public contract. If a signature exports a type that may collapse to ⊥ under some implementation witness, clients may see degenerate type equalities such as s ≡ u. Fωμ can keep this sound, but the interface is not a well-behaved ML signature.

Therefore the paper’s current design — reject non-contractive exported cycles — is still defensible. But the justification should be phrased differently from Im et al. 2013:

• Im et al.: must reject such signatures for source-level type soundness, because sealing is erased by the operational semantics and their calculus would otherwise typecheck M.g (M.f 3).
• Mω: target-level elaboration already rejects the bad implementation or collapses the bad cycles to ⊥; the source-level check is an early, modular discipline that prevents exported interfaces from relying on degenerate target equalities.

5. Is it “for free” from the target system?

Mostly yes, but with one caveat.

The safety of the concrete program is for free if elaboration is faithful and all witness substitutions/subtyping obligations are checked in Fωμ. The target catches the problem when α = id is substituted.

However, a separate source-level contractiveness check may still be needed for algorithmic/modularity reasons:

1. To avoid publishing interfaces whose type equalities depend on later collapsing to ⊥.
2. To ensure that interface equality remains predictable to programmers.
3. To keep separate compilation/module signatures from accepting a contract that no sensible implementation can satisfy, or that only degenerate implementations can satisfy.
4. To avoid having the source language expose ⊥-induced equalities as if they were ordinary ML type equalities.

So I would not claim “contractiveness is foundationally unnecessary” without qualification. I would say:

Contractiveness is not needed as an additional soundness theorem for the elaborated target calculus; Fωμ already accounts for root-active types. Mω imposes contractiveness on exported signatures as a source-language interface discipline, while allowing non-contractive cycles in module bodies whenever their target meaning remains hidden or is checked against the exported interface.

6. Suggested paper insertion

Here is a possible paragraph/example to insert near the related-work discussion of Im et al. 2013 or near the Fωμ/root-active section.

\paragraph{Non-contractive signatures versus bodies.}
Im et al.~\citep{im2013contractive} observe that non-contractive types in
signatures are more dangerous than non-contractive types in modules.  Their
motivating OCaml example declares an abstract constructor \ocaml{'a t} in a
signature together with \ocaml{type s = s t} and \ocaml{type u = u t}, while
the implementation chooses \ocaml{'a t = 'a}, \ocaml{s = int}, and
\ocaml{u = bool}.  Under a source-level treatment of sealing, the signature
appears to equate \ocaml{s} and \ocaml{u}, so \ocaml{M.g (M.f 3)} is accepted
although it applies an integer at type \ocaml{bool}.
 
In our elaboration the same equations first produce the target types
$\mu\beta.\alpha\,\beta$ for both \ocaml{s} and \ocaml{u}, where
$\alpha$ is the witness for the abstract constructor \ocaml{'a t}.  When the
implementation witness $\alpha = \lambda\gamma.\gamma$ is substituted during
sealing, both types reduce to $\mu\beta.\beta$, hence are root-active and
collapse to $\bot$ in \Fomegarec.  The implementation would then have to show
$\texttt{int} \equiv \bot$ and $\texttt{bool} \equiv \bot$, so sealing fails in
the target.  Thus the bad program is rejected by target typing rather than by a
bespoke source-level contractiveness theorem.
 
We nevertheless reject non-contractive cycles in exported signatures.  This is
not needed to repair the target calculus, which already assigns root-active
cycles the degenerate meaning $\bot$; rather, it is an interface discipline that
prevents public module types from exposing degenerate equalities.  Inside module
bodies, non-contractive cycles may be tolerated because their concrete witnesses
are checked before they can be exported.

If you want a more compact related-work version:

Im et al.~\citep{im2013contractive} separate non-contractive signatures from
non-contractive module bodies: the former break source-level sealing, while the
latter may be harmless.  In \Momega this distinction is inherited from the target
rather than reproved for the source.  A signature equation such as
\ocaml{type s = s t} elaborates to $\mu\beta.\alpha\,\beta$; if an
implementation later instantiates $\alpha$ with the identity constructor, the
cycle becomes root-active and collapses to $\bot$ in \Fomegarec, causing the
sealing check to fail.  We therefore impose contractiveness on exported
signatures as an interface discipline, not because target soundness would fail
without it.

7. Recommended changes to current wording

The current related-work draft has a line like:

Contractiveness is largely orthogonal: Fωμ already treats non-contractive recursive types as ill-formed, and elaboration does not re-implement that check.

I would change this. Fωμ does not simply treat them as ill-formed; according to the current draft’s Section 2.5, it allows them syntactically and maps root-active types to ⊥ in equivalence. A safer version is:

Contractiveness is largely delegated to the target: Fωμ permits recursive types syntactically but maps root-active cycles to ⊥ in its equivalence semantics. We add a source-level check only for exported signatures, so public interfaces do not rely on degenerate target equalities.

Also avoid saying:

Mω rejects T because μβ. α β is non-contractive.

That is ambiguous/wrong unless you define contractiveness universally over all substitutions for α. More precise:

The bare equation μβ. α β is productive while α remains opaque, but it is not stable under the implementation witness α = λγ.γ. During sealing, the witness substitution exposes the root-active cycle μβ.β, and the target check fails.

8. Relation to the “static/dynamic” intuition

This example also clarifies the connection you wanted to highlight.

• RTG/RMC-style backpatching handles forward-declared abstract type names. That is analogous to the Mω opaque/single-vision path: keep a secret representation behind an abstract type, then check the witness when the recursive knot is tied.
• Transparent recursive signature equations are a different phenomenon: they are genuine static equations. In Mω, these equations are represented as explicit target μ-types.
• The Im et al. example straddles the two: the public static equations s = s t and u = u t look guarded only because t is abstract; once the dynamic implementation witness for t is supplied, the static equation becomes root-active.

This is a nice explanation of why the target-calculus story is cleaner: it forces the witness substitution and the recursive-type equivalence to meet at the sealing boundary.

9. Final recommendation

Add the example, but use it to make this conceptual distinction:

1. λ^rec_abs rejects the signature as a source-level soundness condition.
2. Mω rejects the full implementation because target sealing exposes the bad witness and Fωμ collapses the resulting cycle to ⊥.
3. Mω still chooses to reject non-contractive exported signatures, but this is a conservative interface discipline rather than the foundational source of soundness.

This will make the comparison with Im et al. sharper and avoid overclaiming that Mω has simply imported their semantic contractiveness check wholesale.