Isomorphisms of types in the presence of higher-order references (extended version)

TL;DR

This paper characterizes type isomorphisms in a finitary language with higher-order references using game semantics, proving a conjecture for finitely branching arenas and discovering new isomorphisms in infinite cases.

Contribution

It introduces a fully abstract game model for a language with sum types and higher-order references, solving Laurent's open problem for finitely branching arenas and exploring infinite branching scenarios.

Findings

Finitely branching arenas are isomorphic iff they are geometrically the same (Laurent's forest isomorphism).

A new equational theory characterizes type isomorphisms in the language.

Laurent's conjecture fails for infinitely branching arenas, revealing new non-trivial isomorphisms.

Abstract

We investigate the problem of type isomorphisms in the presence of higher-order references. We first introduce a finitary programming language with sum types and higher-order references, for which we build a fully abstract games model following the work 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. 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.