[TYPES] Example uses of impredicativity

[William J. Bowman]

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 <wjb at williamjbowman.com> wrote:
> 
> Stefan,
> 
> The type preserving CPS translation with answer type polymorphism requires impredicativity.