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.

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.

  • 1
    Hm, aren't your rules describing equi-recursive types instead of iso-recusive ones? – Andreas Rossberg Jun 13 '17 at 6:20
  • 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 Jun 13 '17 at 12:11
  • Yes, see my answer to this question for why I (incorrectly) thought I wanted something more expressive. – Jonathan Schuster Jun 13 '17 at 16:48
  • 1
    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 Jun 13 '17 at 16:50
  • Ah, @JonathanSchuster got ahead of me. – Andreas Rossberg Jun 13 '17 at 16:52
up vote 4 down vote accepted

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''])$.

  • 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 Jun 14 '17 at 0:35
  • 1
    You're right. Just fixed it, thanks. – Jonathan Schuster Jun 14 '17 at 1:27

Your Answer

By clicking "Post Your Answer", you acknowledge that you have read our updated terms of service, privacy policy and cookie policy, and that your continued use of the website is subject to these policies.

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