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".


1 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.


Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

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