Jeopardy: An Invertible Functional Programming Language

Reversible programming languages guarantee that their programs are invertible at the cost of restricting the permissible operations to those which are locally invertible. However, writing programs in a reversible style can be cumbersome, and may produce significantly different implementations than the conventional – even when the implemented algorithm is, in fact, invertible. We introduce Jeopardy, a functional programming language that guarantees global program invertibility without imposing local invertibility. In particular, Jeopardy allows the limited use of uninvertible – and even nondeterministic – operations, provided that they are used in a way that can be statically determined to be globally invertible. To this end, we outline an implicitly available arguments analysis and further approaches that can give a partial static guarantee to the (generally difficult) problem of guaranteeing invertibility.