<p>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.</p>

CC BY-SA 4.0
2018-05-22T16:40:01.457Z
2018-05-22T16:40:01.457Z
Rodolphe Lepigre
<h2>Context</h2>

<p>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.</p>

<p>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.</p>

<p>If, at some point, the constraint $\alpha &lt;: 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 &lt;: \alpha_1$ and $\alpha_2 &lt;: T_2$.</p>

<h2>The Problem</h2>

<p>The problem arises if you have constraints  $\alpha_2 &lt;: \beta_1 \to \beta_2$, $\beta_2 &lt;: \alpha_1 \to \alpha_2$.</p>

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

<p>If we substitute from our equalities, we then get (among other constraints), $\alpha_{22} &lt;: \beta_{21} \to \beta_{22}$ and $\beta_{22} &lt;: \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.</p>

<p>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.</p>

<h2>My Solution Attempt</h2>

<p>With my definition of subtyping, if $\alpha_2 &lt;: \beta_1 \to \beta_2$, $\beta_2 &lt;: \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 &lt;: \beta \wedge \beta &lt;: \alpha$).</p>

<p>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.</p>

<h2>My Question</h2>

<p>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.</p>

<p>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?</p>

CC BY-SA 3.0
2018-03-26T23:06:18.537Z
How do you end up with a situation where α<:β∧β<:α, or a contradiction is the only thing that can imply that your system is correct?
CinchBlue
CC BY-SA 3.0
2018-03-26T23:08:18.283Z
@VermillionAzure I'm that subtyping is reflexive, so that situation can arise when $\alpha$ and $\beta$ are equal.
Joey Eremondi
CC BY-SA 3.0
2018-03-26T23:11:30.487Z
If subtyping is reflexive, then that may be the problem. It is trivial to show that if you have a subtyping rule that allows $\alpha \rightarrow \alpha$ by the subtyping reduction, then it'll never terminate. IMO perhaps this can be solved by making sure that you cannot reduce a type to itself using the subtype relation.
CinchBlue
CC BY-SA 3.0
2018-03-26T23:13:18.563Z
Another idea: isn't this type inference and not type checking? Usually, you want to make sure that a type $\alpha$ can be type checked with another type $\beta$, which means that type checking can be seen as "building a bridge" rather than performing a reduction into a normal form (type inference).
CinchBlue
CC BY-SA 3.0
2018-03-26T23:26:28.507Z
@VermillionAzure I'm not really sure what you're talking about. Reflexive rules are very common in structural subtyping systems. When you call a function $f : A \to A$ with argument of type $A$, you don't want it to fail because $A$ and $A$ are equal! I'm not sure what you mean by "a rule that allows $\alpha \to \alpha$, and what you mean by reduction in this context.
Joey Eremondi
CC BY-SA 3.0
2018-03-26T23:27:47.533Z
@VermillionAzure Also, to be clear, by  α<:β∧β<:α I'm referring to the conjunction of two subtyping judgements, not an intersection type.
Joey Eremondi
CC BY-SA 3.0
2018-03-27T00:42:49.867Z
Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/75123/discussion-between-vermillionazure-and-jmite).
CinchBlue
CC BY-SA 3.0
2018-03-27T18:04:00.407Z
When I looked at Java's subtype checking, my intuition was that, although it was expected that ruling out cycles would lead to termination, that turned out to be false. (see https://arxiv.org/abs/1605.05274) One place where ruling out such cycles suffices is in C#: see the tech report by Viroli that I cite, or the reformulation in https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/
Radu GRIGore
CC BY-SA 3.0
2018-03-28T08:24:35.510Z
It would be great if someone could rephrase this question with poset/set system/hypergraph terminology for the typically challenged readers.
domotorp
CC BY-SA 3.0
2018-03-30T06:07:02.693Z
@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. [...]
Radu GRIGore
CC BY-SA 3.0
2018-03-30T06:10:50.363Z
@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
Radu GRIGore
CC BY-SA 3.0
2018-03-30T06:11:09.677Z
@domotorp: ... when the "cycle check" is sufficient.
Radu GRIGore
CC BY-SA 3.0
2018-03-30T06:51:37.383Z
@Radu Thanks, this certainly helped, though I still cannot understand the question. Each label is a formula, i.e., allowed word over some alphabet, or just one letter? What are possible typing rules? If you link to a short description, or provide some example, that would help, I guess.
domotorp
CC BY-SA 3.0
2018-04-02T05:33:01.530Z
@domotorp: I don't feel like I understand the question either, and I don't know a description that is brief. I can answer on best-effort basis. Labels (typing judgments) are first-order terms, over some specific vocabulary. More precisely, see Chapters 4 and 24 here: https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf
Radu GRIGore
<pl.programming-languages><type-theory><type-systems><type-inference>
Avoiding Cycles with Unification and Subtyping
Joey Eremondi
# Avoiding Cycles with Unification and Subtyping

(Asked by: username_0 on 2018-03-26)

## 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?

**Tags:** pl.programming-languages, type-theory, type-systems, type-inference
> **Comments:**
> **username_1**: How do you end up with a situation where α<:β∧β<:α, or a contradiction is the only thing that can imply that your system is correct?  
> **username_0**: @VermillionAzure I'm that subtyping is reflexive, so that situation can arise when $\alpha$ and $\beta$ are equal.  
> **username_1**: If subtyping is reflexive, then that may be the problem. It is trivial to show that if you have a subtyping rule that allows $\alpha \rightarrow \alpha$ by the subtyping reduction, then it'll never terminate. IMO perhaps this can be solved by making sure that you cannot reduce a type to itself using the subtype relation.  
> **username_1**: Another idea: isn't this type inference and not type checking? Usually, you want to make sure that a type $\alpha$ can be type checked with another type $\beta$, which means that type checking can be seen as "building a bridge" rather than performing a reduction into a normal form (type inference).  
> **username_0**: @VermillionAzure I'm not really sure what you're talking about. Reflexive rules are very common in structural subtyping systems. When you call a function $f : A \to A$ with argument of type $A$, you don't want it to fail because $A$ and $A$ are equal! I'm not sure what you mean by "a rule that allows $\alpha \to \alpha$, and what you mean by reduction in this context.  
> **username_0**: @VermillionAzure Also, to be clear, by  α<:β∧β<:α I'm referring to the conjunction of two subtyping judgements, not an intersection type.  
> **username_1**: Let us [continue this discussion in chat](https://chat.stackexchange.com/rooms/75123/discussion-between-vermillionazure-and-jmite).  
> **username_2**: When I looked at Java's subtype checking, my intuition was that, although it was expected that ruling out cycles would lead to termination, that turned out to be false. (see https://arxiv.org/abs/1605.05274) One place where ruling out such cycles suffices is in C#: see the tech report by Viroli that I cite, or the reformulation in https://www.microsoft.com/en-us/research/publication/on-decidability-of-nominal-subtyping-with-variance/  
> **username_3**: It would be great if someone could rephrase this question with poset/set system/hypergraph terminology for the typically challenged readers.  
> **username_2**: @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. [...]  
> **username_2**: @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  
> **username_2**: @domotorp: ... when the "cycle check" is sufficient.  
> **username_3**: @Radu Thanks, this certainly helped, though I still cannot understand the question. Each label is a formula, i.e., allowed word over some alphabet, or just one letter? What are possible typing rules? If you link to a short description, or provide some example, that would help, I guess.  
> **username_2**: @domotorp: I don't feel like I understand the question either, and I don't know a description that is brief. I can answer on best-effort basis. Labels (typing judgments) are first-order terms, over some specific vocabulary. More precisely, see Chapters 4 and 24 here: https://www.cs.cmu.edu/~rwh/pfpl/2nded.pdf  

---

## 1 answers

### Answer by username_4 on 2018-05-22. Score: 4

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.


---

