Why RMC can’t be defined coinductively
In Dreyer's "A Type System for Recursive Modules" (also known as the RMC paper), there is something very curious going on with the inference rules: in order to support recursive signatures and modules, RMC must do a pre-pass before doing the typechecking pass proper. This is actually quite common in recursive module systems (e.g., you see it again in MixML).
In RMC, there are three places where this occurs:
In a recursive signature rec (X) sig ... end, we first elaborate a "shallow" version of the signature, so that when we typecheck proper we can have X in the context with some type variables (which will be subsequently substituted once we are finished.)
In a recursive module rec (X : S) struct ... end, we must first compute the type components of all types in the module before we typecheck values. This solves a simplified double vision problem: where expressions in the recursive module should "see" that X.t and t are the same type.
When we opaquely seal a module M :> S, we must compute the type components of the inner module, so that we can update the context with the revealed types inside the module. This situation arises in combination with recursive modules.
While studying GHC's source code, I discovered an interesting way we implemented recursive modules using knot-tying. Essentially, GHC does not implement any pre-pass; instead, it lazily feeds in the result of typechecking into the typechecking process itself. As long as we don't try to look at the actual type while we are constructing them, everything will be in the right place.
This suggested two things to me:
Knot-tying should be a reasonable implementation mechanism for RMC, which would allow us to avoid having to implement typechecking twice.
It should mean that there is a "coinductively defined" set of typing rules for RMC which can circularly refer to itself.
So, I formulated a plan:
Take an ordinary implementation of RMC, but instead of making calls to simplified typing judgments to compute type components, "tie the knot" directly with the results of typechecking.
Take this knot-tying implementation, and then convert it to use the delay modality as described in "Productive Coprogramming with Guarded Recursion". This would establish the termination of the typechecker.
With this implementation, convert it back into inference rules, getting a coinductive rule set for RMC.
The good news is that (1) works: you can implement RMC with lazy evaluation, even solving the double vision problem involving opaque sealing. The key is that you can do a lazy substitution on the context when you enter a sealed module. I validated this with a fairly simple prototype implementation of RMC in Haskell.
The bad news is that the knot-tying is not actually coinductive at all, making (2) impossible (and (3) a moot point).
The crux of the issue is that guardedness is actually too strong of a restriction for user programs. Consider the process for typechecking this signature:
rec (X) sig structure A : SA where type u = X.B.u structure B : SB where type t = X.A.t end
In our proposed type system, the type of X is available tomorrow (after we finish typechecking this group.) But then we run into a problem: we need to produce a type for A.u today, but this type must be read off of X.B.u, which is only available tomorrow. The type system cannot guarantee that this dereference is OK (and indeed, it is NOT OK if a user wrote down a signature with a transparent type cycle.)
As usual, the theory is behind the implementation. Why does the implementation work? Well, for one, it doesn't: if you feed it a transparent type cycle it will infinite loop. But for "well-behaved" inputs, it works because the recursive reference goes to some other type which IS available today. But there is no obvious way to encode this in the type-system: the "proof" that this is the case would be some sort of cyclicity check.
The problem is that the delay modality is a technique for generating infinite data. Nothing about RMC typechecking is infinite: knot-tying is purely a convenient way to "get" finite data where it needs to be. The correct way to show termination is to not use coinductive fixpoint in the first place; you can't use the future-value in any useful way.
Perhaps there is an alternate type system which can express the dynamic correctness condition on such "finitary" knot-tying: the idea is that lazy values would track their (dynamic) data dependencies. Then at the fixpoint operator, we would have a graph. We check if the graph is acyclic; and if it is, we know that everything will terminate. I think this would be eminently implementable, and the API would like quite similar to the API for the delay modality (the applicative functor helps us accurately track dependencies), but as far as inference rules goes, it does not seem like much of an improvement over RMC.
So that's why I don't think it will work. Hello Ripley!
