[TYPES] Example uses of impredicativity

[Benjamin C. Pierce]

Impredicativity is also useful in type-theoretic encodings of objects.  Objects with method interface M are represented as elements of

   Obj(M)  =  Exists X, X * (X -> M(X))

i.e., as pairs of a “hidden state” X and a transformation on that state yielding a result of shape M.  For example, if 

    M(X) = { push: Nat -> X, pop: Nat * X }

then Obj(M) can be viewed as a type of stack objects.  And since one natural way to represent a non-empty stack is as a pair of a number and another stack, we need the existential quantifier to range over a collection of types that includes Nat * Obj(M).

(This is basically a generalization of the typed closure encoding, though they were actually discovered in the other order!)

Best,

    - Benjamin

> On Jul 5, 2019, at 6:08 PM, Stefan Monnier <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
> 
>