Isomorphisms of types in the presence of higher-order references

Pierre Clairambault

We study the effect of higher-order references on isomorphisms of types in functional programming languages. We first introduce a finitary programming language with sum types and higher-order references, for which we describe a fully abstract games model following the approach of Abramsky, Honda and McCusker. Solving an open problem by Laurent, we show that two finitely branching arenas are isomorphic if and only if they are geometrically the same, up to renaming of moves (Laurent’s forest isomorphism). We deduce from this an equational theory characterizing isomorphisms of types in our language, that is conservative over the purely functional case. We show however that Laurent’s conjecture does not hold on infinitely branching arenas, yielding new non-trivial type isomorphisms in a variant of our language with natural numbers.