How does infinite-looping the OCaml type checker using modules work?

user_2482570 0
Viewed 147

The OCaml type-checker infinite-loops on this example:

     module type I =
     sig
       module type A
       module F :
         functor(X :
         sig
           module type A = A
           module F : functor(X : A) -> sig end
         end) -> sig end
     end

     module type J =
     sig
       module type A = I
       module F : functor(X : I) -> sig end
     end

     (* Try to check J <= I *)

     module Loop(X : J) = (X : I)

source: Andreas Rossberg adapting Mark Lillibridge's example

I don't have a good handle of how/why this works. In particular:

  • Is the example minimal?
  • What work are all the sharing constraints A = I, A = A, etc. doing? Are sharing constraints necessary in order to cause this infinite loop?
  • What work is the inline signature in the first functor doing? That seems to be essential to the example.
  • Is this trick useful only for infinite-looping, or can arbitrary computation happen in the module system?
  • Can examples like this be translated to other languages? Traits and classes with type members and parameterized type aliases look a lot like the code above.
ocaml
1 Answers
  • The example is pretty minimal, it relies on two essential ingredients:
    • an abstract module type
    • a functor to make the abstract module type appear in both covariant and contravariant position.

Answering your high-level questions before going back to the example:

  • With this trick only the subtyping checker for the module type system is doing an unbounded amount of work. You cannot observe the result of this computation. However, using abstract module type is the key to trick the module type system into doing expansive computation (a module with a chain of 4↑↑4 submodule for instance)

  • Reproducing this exact problem probably requires both subtyping and impredicativity, I am not sure how often this combination appears outside of module systems.

Going back to the example at hand, I propose to leap a bit into the future with OCaml 4.13 and its with module type constraint. I hope that this makes the ingredients behind this trick a little bit more visible:

module type e = sig end

module type Ieq = sig
  module type X
  module type A = X
  module F : X -> e
end

module type I = sig
  module type A
  module F : Ieq with module type X = A -> e
end

module type J = Ieq with module type X = I

Opinions may vary, but I find that this form makes it more obvious that in the I case, we have more equations on the functor F component, whereas in the Ieq with module type X = ... case, we have one more equation on the module type A component.

While trying to prove that J<I, we end up moving around those equations without achieving any progress. Let's try to see how that happens step by step. First, we look at the module type A:

J I
J.A = module type A = I I.A = module type A (abstract)

Since I.A is abstract, this is true. Then, we need to compare J.F and I.F, but only after adding the equation A=I from J.

J I with module type A = I
J.F = I -> e I.F = (Ieq with module type X = (*A =*) I) -> e

Now, we have a functor. Functors are contravariant in their argument. In other words, to prove that X -> e < Y -> e, we need to prove that Y < X.

Thus, we need to prove that Ieq with module type X = I < I... but this inequation looks a bit familiar. And indeed, we had defined:

module type J = Ieq with module type X = I

Reusing this definitions, this means that we are back to trying to prove J<I, without making any progress.

If we look at our previous steps, the problem started when we extended I with another copy of itself I with module type A = I. Then contravariance allowed us to spread this increase of size to both side of the comparison. Therefore, our inclusion check is always producing more work for its future self and this specific inclusion check never ends.

user_73693660
Related