What's the definition of join on iso-recursive types?

Question

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.

Answer 1

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.

Answer 2

I thought I wanted something more like gasche proposed in his answer, 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''])$.