Revisiting catamorphisms over datatypes with embedded functions
Leonidas Fegaras · 2018
this paper we give numerous examples of why it is truly important to be able to define catamorphisms over datatypes with embedded functions and show how to define functions as catamorphisms even when no right inverse exists by using a trick that invents an approximate inverse instead. In order to ensure soundness of this trick we replace the restriction of the existence of a right inverse with another less demanding restriction and show how the type system can be used to statically enforce this restriction. 2 Structures with Functionals are Useful