[ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
Stefan, The type preserving CPS translation with answer type polymorphism requires impredicativity. Cédille uses impredicativity heavily, so that might be a better place to look than Coq. Although I guess that's more examples of (things like) Church encodings. (For that matter, the CPS translation is too.) -- Sent from my phoneamajig > On Jul 5, 2019, at 22:33, William J. Bowman <[email protected]> wrote: > > Stefan, > > The type preserving CPS translation with answer type polymorphism requires > impredicativity.
