Wadler's Blog

Thanks for suggesting impredicativity instead --- it's much more suitable. :)

Two comments:

1. I disagree that impredicativity is a 'category error'. Impredicativity is 'safe' if the entity being defined can also be defined by some other means. Universal properties and the proof for Goedel's Incompleteness Theorem are safe instances of impredicativity.

Whether having impredicative syntax is safe or not, such as the polymorphic lambda calculus, is a matter of taste ;).

2. Less seriously, the post's title is incorrect: these images are not impredicative, they only depict impredicativity. :)