<p>I thought I wanted something more like gasche proposed in <a href="https://cstheory.stackexchange.com/a/38409/5356">his answer</a>, but after talking to some colleagues in my lab I realized I was just using iso-recursive types wrong in my examples, which led to me wanting a larger subtyping relation than iso-recursive types usually have (specifically, allowing types with different numbers of unrollings to be subtypes).</p>

<p>After fixing my code to use iso-recursive types properly, I found the standard subtyping based on the Amber rule (Cardelli 1986) would work just fine for my examples. Based on that, this seems to be the corresponding natural rule for join:</p>

<p>$\mu X. \tau \sqcup \mu X'. \tau' = \mu X''. \tau''$ where $X''$ is a fresh type variable and $\tau'' = (\tau[X \leftarrow X''] \sqcup \tau'[X' \leftarrow X''])$.</p>

CC BY-SA 3.0
2017-06-14T00:35:56.923Z
Shouldn't the 2nd line be $\tau'' = (\tau[X \leftarrow X''] \sqcup \tau'[X' \leftarrow X''])$, which has $\tau'$ instead of one occurrence of $\tau$? (I can't edit this myself because it's a one-char edit).
Blaisorblade
CC BY-SA 3.0
2017-06-13T16:47:38.093Z
2017-06-14T01:26:44.050Z
2017-06-14T01:26:44.050Z
Jonathan Schuster
<p>I thought a bit about this and I am afraid that it is harder than it
looks -- as you suspected! In the spirit of encouraging discussion,
I'll write my chain of thoughts.</p>

<p>The subtyping rules are often defined as judgments of the form <code>t1 &lt;:
t2</code>, where <code>---</code> is an inductive rule (you can only use them finitely
many times along each path in the derivation tree) and <code>===</code> is
a coinductive rule (you can use it infinitely many times).</p>

<pre><code>t1 &lt;: t2
t'1 &lt;: t'2
=================
t1*t'1  &lt;: t2*t'2

t1 :&gt; t2
t'1 &lt;: t'2
======================
t1 -&gt; t'1 &lt;: t2 -&gt; t'2

========
t &lt;: top

========
bot &lt;: t

------
t &lt;: t

t1 &lt;: t2
t2 &lt;: t3
--------
t1 &lt;: t3

t1[a \ mu a. t1] &lt;: t2
----------------------
(mu a. t1) &lt;: t2

t1 &lt;; t2[a \ mu a. t2]
----------------------
t1 &lt;: (mu a. t2)
</code></pre>

<p>I would think you can define the <code>/\</code> and <code>\/</code> by turning this into
a three-place judgment. Only showing one half:</p>

<pre><code>t1 /\ t2 = t3
t'1 /\ t'2 = t'3
=========================
t1*t'1 /\ t2*t'2 = t3*t'3

t1 \/ t2 = t3
t'1 /\ t'2 = t'3
==================================
t1 -&gt; t'1 /\ t2 -&gt; t'2 = t3 -&gt; t'3

===============
t1 /\ top &lt;: t1

================
top /\ t2 &lt;: tt2

================
t1 /\ bot &lt;: bot

================
bot /\ t1 &lt;: bot

----------
t /\ t = t

t1 /\ t2 = t12
t12 /\ t3 = t23
-----------------------
(t1 /\ t2) /\ t3 = t123

t1 /\ t23 = t123
t2 /\ t3 = t23
-----------------------
t1 /\ (t2 /\ t3) = t123
</code></pre>

<p>(The two halves, <code>/\</code> and <code>\/</code>, can be factorized with a parametrized
presentation where <code>/\^{-1}</code> is <code>\/</code> and <code>top^{-1}</code> is <code>bot</code>.)</p>

<p>The problem here are the mu-unfolding rules:</p>

<pre><code>t1[a \ mu a. t1] /\ t2 = t3
---------------------------
(mu a. t1) /\ t2 = t3

t1 /\ t2[a \ mu a. t2] = t3
---------------------------
t1 /\ (mu a. t2) = t3
</code></pre>

<p>Clearly there should be a rule that allows to build a (mu a. t3) on
the right-hand side; I think the rules above are probably not
complete.</p>

<p>Some presentations of recursive subtyping have rules of the form:</p>

<pre><code>Gamma, a &lt;: b |- t1 &lt;: t2
---------------------------------
Gamma |- (mu a. t1) &lt;: (mu b. t2)

-------------------------------
Gamma ∋ (t1 &lt;: t2) |- t1 &lt;: t2
</code></pre>

<p>(Technically these interact with the induction/coinduction
presentation: you may not use an hypothesis in Gamma without using one
of the coinductive/productive rules first.)</p>

<p>I guess that those could be adapted to:</p>

<pre><code>Gamma, a /\ b = c |- t1 /\ t2 = t3
-----------------------------------------------
Gamma |- (mu a. t1) /\ (mu b. t2) = (mu c . t3)

----------------------------------------
Gamma ∋ (t1 /\ t2 = t3) |- t1 &lt;: t2 = t3
</code></pre>

<p>I thought that the syntax/coinduction-based presentations of recursive
subtyping ("Coinductive axiomatization of recursive type equality and
subtyping", Brandt and Henglein, 1997; "Subtyping, Declaratively", Danielsson, 2010) would avoid having to think about the tree-form of mu-types,
but it looks like the syntax alone does not scale that nicely to
defining the meet/join, so maybe going back to the tree presentation
would better reveal what should happen.</p>

CC BY-SA 3.0
2017-06-13T06:20:49.503Z
Hm, aren't your rules describing equi-recursive types instead of iso-recusive ones?
Andreas Rossberg
CC BY-SA 3.0
2017-06-13T12:11:06.630Z
They are; it seems to me that (contrarily to equality) it is natural for subtyping and join to ignore the iso/equi difference (in an iso-recursive language they would elaborate to a coercion with fold/unfold operations). Is there a presentation of "iso-recursive subtyping" that is natural?
gasche
CC BY-SA 3.0
2017-06-13T16:48:22.250Z
Yes, see my answer to this question for why I (incorrectly) thought I wanted something more expressive.
Jonathan Schuster
CC BY-SA 3.0
2017-06-13T16:50:18.463Z
Not sure I see the difference between equality and subsumption in this regard, since iso-recursive types are inhabited by different values than their unrollings. I think the natural formulation is to require unrolling on both sides, e.g. mu a.t <: mu b.u <== t[a\mu a.t] <: u[b\mu b.u], which you can extend to joins.
Andreas Rossberg
CC BY-SA 3.0
2017-06-13T16:52:07.833Z
Ah, @JonathanSchuster got ahead of me.
Andreas Rossberg
CC BY-SA 3.0
2017-06-14T00:37:37.460Z
I think the question about equi-recursive types is still generally interesting (though maybe not for the OP).
Blaisorblade
CC BY-SA 3.0
2017-06-12T18:07:34.303Z
2017-06-12T18:07:34.303Z
gasche
<p>In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both the "then" and "else" branches of an if-statement.</p>

<p>What should the definition of join be for iso-recursive types such as $\mu X.\tau$? I started to write it myself, but realized it gets a little tricky if the recursion in each type is unrolled to a different depth.</p>

<p>If there's a standard reference for this, even better. Benjamin Pierce's "Types and Programming Languages" lists the necessary subtype rules near the end of chapter 21, but doesn't define the join rules.</p>

<pl.programming-languages><type-theory>
What's the definition of join on iso-recursive types?
Jonathan Schuster
# What's the definition of join on iso-recursive types?

(Asked by: username_0 on 2017-06-12)

In languages with subtyping, there is often a "join" operation defined to compute the least upper bound of two types. It's used in type-checking, for example to find the smallest type that covers both the "then" and "else" branches of an if-statement.

What should the definition of join be for iso-recursive types such as $\mu X.\tau$? I started to write it myself, but realized it gets a little tricky if the recursion in each type is unrolled to a different depth.

If there's a standard reference for this, even better. Benjamin Pierce's "Types and Programming Languages" lists the necessary subtype rules near the end of chapter 21, but doesn't define the join rules.

**Tags:** pl.programming-languages, type-theory

---

## 2 answers

### Answer by username_0 on 2017-06-13. Score: 4 | Accepted answer

I thought I wanted something more like gasche proposed in [his answer](https://cstheory.stackexchange.com/a/38409/5356), but after talking to some colleagues in my lab I realized I was just using iso-recursive types wrong in my examples, which led to me wanting a larger subtyping relation than iso-recursive types usually have (specifically, allowing types with different numbers of unrollings to be subtypes).

After fixing my code to use iso-recursive types properly, I found the standard subtyping based on the Amber rule (Cardelli 1986) would work just fine for my examples. Based on that, this seems to be the corresponding natural rule for join:

$\mu X. \tau \sqcup \mu X'. \tau' = \mu X''. \tau''$ where $X''$ is a fresh type variable and $\tau'' = (\tau[X \leftarrow X''] \sqcup \tau'[X' \leftarrow X''])$.

> **Comments:**
> **username_1**: Shouldn't the 2nd line be $\tau'' = (\tau[X \leftarrow X''] \sqcup \tau'[X' \leftarrow X''])$, which has $\tau'$ instead of one occurrence of $\tau$? (I can't edit this myself because it's a one-char edit).  

---

### Answer by username_2 on 2017-06-12. Score: 8

I thought a bit about this and I am afraid that it is harder than it
looks -- as you suspected! In the spirit of encouraging discussion,
I'll write my chain of thoughts.
The subtyping rules are often defined as judgments of the form t1 <:
t2, where --- is an inductive rule (you can only use them finitely
many times along each path in the derivation tree) and === is
a coinductive rule (you can use it infinitely many times).
t1 <: t2
t'1 <: t'2
=================
t1*t'1  <: t2*t'2

t1 :> t2
t'1 <: t'2
======================
t1 -> t'1 <: t2 -> t'2

========
t <: top

========
bot <: t

------
t <: t

t1 <: t2
t2 <: t3
--------
t1 <: t3

t1[a \ mu a. t1] <: t2
----------------------
(mu a. t1) <: t2

t1 <; t2[a \ mu a. t2]
----------------------
t1 <: (mu a. t2)

I would think you can define the /\ and \/ by turning this into
a three-place judgment. Only showing one half:
t1 /\ t2 = t3
t'1 /\ t'2 = t'3
=========================
t1*t'1 /\ t2*t'2 = t3*t'3

t1 \/ t2 = t3
t'1 /\ t'2 = t'3
==================================
t1 -> t'1 /\ t2 -> t'2 = t3 -> t'3

===============
t1 /\ top <: t1

================
top /\ t2 <: tt2

================
t1 /\ bot <: bot

================
bot /\ t1 <: bot

----------
t /\ t = t

t1 /\ t2 = t12
t12 /\ t3 = t23
-----------------------
(t1 /\ t2) /\ t3 = t123

t1 /\ t23 = t123
t2 /\ t3 = t23
-----------------------
t1 /\ (t2 /\ t3) = t123

(The two halves, /\ and \/, can be factorized with a parametrized
presentation where /\^{-1} is \/ and top^{-1} is bot.)
The problem here are the mu-unfolding rules:
t1[a \ mu a. t1] /\ t2 = t3
---------------------------
(mu a. t1) /\ t2 = t3

t1 /\ t2[a \ mu a. t2] = t3
---------------------------
t1 /\ (mu a. t2) = t3

Clearly there should be a rule that allows to build a (mu a. t3) on
the right-hand side; I think the rules above are probably not
complete.
Some presentations of recursive subtyping have rules of the form:
Gamma, a <: b |- t1 <: t2
---------------------------------
Gamma |- (mu a. t1) <: (mu b. t2)

-------------------------------
Gamma ∋ (t1 <: t2) |- t1 <: t2

(Technically these interact with the induction/coinduction
presentation: you may not use an hypothesis in Gamma without using one
of the coinductive/productive rules first.)
I guess that those could be adapted to:
Gamma, a /\ b = c |- t1 /\ t2 = t3
-----------------------------------------------
Gamma |- (mu a. t1) /\ (mu b. t2) = (mu c . t3)

----------------------------------------
Gamma ∋ (t1 /\ t2 = t3) |- t1 <: t2 = t3

I thought that the syntax/coinduction-based presentations of recursive
subtyping ("Coinductive axiomatization of recursive type equality and
subtyping", Brandt and Henglein, 1997; "Subtyping, Declaratively", Danielsson, 2010) would avoid having to think about the tree-form of mu-types,
but it looks like the syntax alone does not scale that nicely to
defining the meet/join, so maybe going back to the tree presentation
would better reveal what should happen.

> **Comments:**
> **username_3**: Hm, aren't your rules describing equi-recursive types instead of iso-recusive ones?  
> **username_2**: They are; it seems to me that (contrarily to equality) it is natural for subtyping and join to ignore the iso/equi difference (in an iso-recursive language they would elaborate to a coercion with fold/unfold operations). Is there a presentation of "iso-recursive subtyping" that is natural?  
> **username_0**: Yes, see my answer to this question for why I (incorrectly) thought I wanted something more expressive.  
> **username_3**: Not sure I see the difference between equality and subsumption in this regard, since iso-recursive types are inhabited by different values than their unrollings. I think the natural formulation is to require unrolling on both sides, e.g. mu a.t <: mu b.u <== t[a\mu a.t] <: u[b\mu b.u], which you can extend to joins.  
> **username_3**: Ah, @JonathanSchuster got ahead of me.  
> **username_1**: I think the question about equi-recursive types is still generally interesting (though maybe not for the OP).  

---

