[TYPES] Example uses of impredicativity

[Matthieu Sozeau]

> Le 6 juil. 2019 à 03:44, Martin Escardo <m.escardo at cs.bham.ac.uk> a écrit :
> 
> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
> 
> One example is the powerset P X of a type X, defined as the type X -> Prop of functions into Prop. Without the impredicativity of Prop, you are not able to construct a function P(P X) -> P X that gives the union of a set of sets. Also Prop itself wouldn't be a complete lattice with a join function P Prop -> Prop in the absence of impredictivity. 

… and this complete lattice gives you a Tarski fixed point theorem, on which the Paco library for coinductive reasoning is built, making use of Mendler-style recursion (also requiring impredicativity).
— Matthieu

> On 05/07/2019 23:08, monnier at iro.umontreal.ca wrote:
>> [ The Types Forum, http://lists.seas.upenn.edu/mailman/listinfo/types-list ]
>> Hi,
>> I was recently reminded that not only I only understand impredicativity
>> in a very superficial way, but on top of that, I don't know of many
>> uses of it.
>> Basically, I know of its use in Church encodings, in Shao et. al.'s λₕ
>> (from Type-safe Certified Binaries, which I also used in my "swiss
>> coercion"), as well as in type-preserving closure conversion, but that's
>> pretty much it.
>> When I started to look for examples in Coq, I soon realized that many
>> Coq libraries have definitions whose universe level is affected by
>> impredicativity but it's a lot more work to discover if the same
>> development would work as well without impredicativity.
>> Is there some place where I could find a kind of "collection" of
>> developments/techniques which rely on impredicativity?
>> Short of that, I'd be happy to hear from examples which
>> I could assemble to make such a collection.
>>         Stefan
> 
> -- 
> Martin Escardo
> http://www.cs.bham.ac.uk/~mhe