How to prove relations between “classes” of types?

Question

After reading Effects as Sessions, Sessions as Effects, I was wondering how would a proof of equivalence between both take place, or even, a proof of Sessions types being a Type and Effect System.

In a more generic fashion, how one can prove a relation (e.g. equivalence) between different "classes"* of types? Would that expressiveness test as done by Orchard and Yoshida be enough?

[*]: I don't know how to correctly define it, I don't want to use "kinds of types" or "types of types".

Answer 1

One approach to such questions is via encodings.

Say you have a language $L_1$ and a language $L_2$ and you want to show that they are somehow "the same", you can do this by finding an encoding

$$ \newcommand{\SEMBTYPE}[1]{\ulcorner #1 \urcorner} \newcommand{\SEMB}[1]{\lbrack\!\lbrack #1 \rbrack\!\rbrack} \SEMB{\cdot} : L_1 \rightarrow L_2 $$

and then show that for all $L_1$ programs $M, N$ the following holds:

$$ M \cong_1 N \qquad \text{iff} \qquad \SEMB{M_1} \cong_2 \SEMB{M_2} $$

Here $\cong_i$ is a chosen notion of program equivalence for $L_i$. In order to do this for typed languages, one typically also maps $L_1$-types to $L_2$ by way of a function $\SEMBTYPE{\cdot}$ which is extended to typing environments, such that something like the following holds:

$$ \Gamma \vdash_1 M : \alpha \qquad \text{implies} \qquad \SEMBTYPE{\Gamma} \vdash_2 \SEMB{M} : \SEMBTYPE{\alpha} $$ Here $\vdash_i$ is the typing judgement for $L_i$. The whole approach is called full abstraction.

In order to avoid the "curse of Church-Turing universality", one typically imposes conditions on $\SEMB{\cdot}$, e.g. that it's compositional, or closed under injective renaming. The more conditions $\SEMB{\cdot}$ meets, the stronger the full abstraction result.

This is also Orchard & Yoshida are attempting to do (Theorems 1- 5), although they don't quite achieve it.