7
$\begingroup$

Context

I realize that subtyping often doesn't admit principle types, and that inference in the presence of subtypes is undecidable. I'm working in a context where typechecking should simply fail there is not a single most general solution, and where annotations can be added to aid inference.

Suppose that we have a type system where, during typechecking, some types need to be inferred using unification, and may be type variables $\alpha, \beta$ etc.

If, at some point, the constraint $\alpha <: T_1 \to T_2$, where $\to$ is the usual function type constructor, then we can decompose this into $\alpha = \alpha_1 \to \alpha_2$, with $T_1 <: \alpha_1$ and $\alpha_2 <: T_2$.

The Problem

The problem arises if you have constraints $\alpha_2 <: \beta_1 \to \beta_2$, $\beta_2 <: \alpha_1 \to \alpha_2$.

In such a case, we get: $\alpha_2 = \alpha_{21} \to \alpha_{22}, \beta_1 <: \alpha_{21}, \alpha_{22} <: \beta_2 $ from the first constraint, and $\beta_2 = \beta_{21} \to \beta_{22}, \alpha_2 <: \beta_{21}, \beta_{22} <: \alpha_2$ from our second problem.

If we substitute from our equalities, we then get (among other constraints), $\alpha_{22} <: \beta_{21} \to \beta_{22}$ and $\beta_{22} <: \alpha_{21} \to \alpha_{22}$, which is identical to the form of our original problem. Clearly if we continue solving this way, we will never terminate.

When going to write a proof of termination, the problem is that substitution decreases the number of unsolved variables but increases the structural-size of the problems, and solving subtyping decreases the structural size of the problems, but increases the number of unsolved variables, so they don't work in a well-founded ordering.

My Solution Attempt

With my definition of subtyping, if $\alpha_2 <: \beta_1 \to \beta_2$, $\beta_2 <: \alpha_1 \to \alpha_2$ has no solution. The problem seems to be the "cycle", so if we do a sort of occurs check and fail when cycles are detected (or turn them into equality cycles, which will fail except for $\alpha <: \beta \wedge \beta <: \alpha$).

I'm not exactly certain how to formalize a cycle like this, and how such a check would give me something that I can use in a proof of termination.

My Question

My work is about the specifics of a particular subtyping system, but the problem here seems very general, so I'm wondering if this is a known problem, if there are known solutions to it, and if there is research that either formalizes or disproves my intuition about cycles.

What kind of cycles in subtyping constraints do I need to eliminate to avoid this infinite looping? Or is this a deeper problem with no solution?

$\endgroup$
  • $\begingroup$ How do you end up with a situation where α<:β∧β<:α, or a contradiction is the only thing that can imply that your system is correct? $\endgroup$ – VermillionAzure Mar 26 '18 at 23:06
  • $\begingroup$ @VermillionAzure I'm that subtyping is reflexive, so that situation can arise when $\alpha$ and $\beta$ are equal. $\endgroup$ – jmite Mar 26 '18 at 23:08
  • 1
    $\begingroup$ @domotorp: I can attempt some translation. Typically, you'd say that a typing judgment holds when there exists a finite proof tree whose root is that judgment. A proof tree is a tree whose nodes are labeled and for which the label on a node and the labels of its children fit one of a given fixed set of patterns (typing rules); for example, some such patterns may allow certain labels to not have children at all, and that's how the tree "ends". Now, the set of typing rules is fixed in advance, but it varies from a typing system to another. [...] $\endgroup$ – Radu GRIGore Mar 30 '18 at 6:07
  • 1
    $\begingroup$ @domotorp: ... The question points out that some rules, which are often included, lets you build an infinite branch. So, if you are using some simple enumeration (over rules) strategy for figuring out if there exists a proof tree, then you'd fail. So, the question is whether it is sufficient to combine an enumeration strategy with a check for "am I making an infinite branch now?" In my comment I tried to point to two concrete sets of typing rules, one for which the answer is 'no' and one for which the answer is 'yes. That still leaves open whether there is some sort of nice characterization of $\endgroup$ – Radu GRIGore Mar 30 '18 at 6:10
  • 1
    $\begingroup$ @domotorp: ... when the "cycle check" is sufficient. $\endgroup$ – Radu GRIGore Mar 30 '18 at 6:11
4
$\begingroup$

From what I understand, it is likely that your subtyping constraints will always be of the form $\alpha \subseteq A$ or $A \subseteq \alpha$, where $\alpha$ is a unification variable. If that is the case, then one idea would be to follow a kind of occurs-check discipline. One thing that you can do to eliminate cycles is to maintain the invariant that there is a solution to your system. The solution that is the easiest to built (but the least general in some sense) is to set $\alpha := A$ for all constraints of the form $\alpha \subseteq A$, and to set $\alpha := \top$ for all constraints of the form $A \subseteq \alpha$ (and there is probably some work to do if $\alpha$ appears to the left/right of several constraints). For this solution to be valid, the simultaneous instantiation of all the unification variables should not induce a cycle in their definition. To do that, you can construct a form of dependency graph on unification variables, in which $\alpha$ depends on the unification variables of $A$ for each constraint $\alpha \subseteq A$. You then need to ensure that the obtained graph does not contain cycles.

$\endgroup$

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service, privacy policy and cookie policy

Not the answer you're looking for? Browse other questions tagged or ask your own question.