[TYPES] Example uses of impredicativity

[Beta Ziliani]

Hi Stefan,

In Mtac we use impredicativity to code a fixpoint for Coq’s meta-programs.
The details can be found in [1].

Roughly, the idea behind Mtac is to have an inductive datatype M : Type ->
Prop with primitives for meta-programming in Coq. For instance, you have
monadic operations (ret : forall A:Type, A -> M A, bind : forall A B :
Type, M A -> (A -> M B) -> M B) together with meta-operations, like
meta-variable creation (evar : forall A: Type, M A), etc.

It also has an unbounded fixpoint. However, the typical type for fixpoints
doesn’t work with Coq, as it requires a negative occurrence of M:

mfix : forall (A: Type) (P: A -> Type), ((forall x: A, *M (P x)*) ->
(forall x: A, M (P x))) -> (forall x: A, M (P x))

(note the first M). For this reason, we encode this using the “Mendler
style”, adding a parameter S:

mfix : forall (A: Type) (P: A -> Type) *(S: Type -> ????)*, *(forall
x: A, S (P x) -> M (P x)) ->* ((forall x: A, S (P x)) -> (forall x: A,
S (P x))) -> (forall x: A, M (P x))

(The ???? will become clear in a sec.) Now we avoid the negative occurrence
on M, but we have a new condition relating S and M: forall x: A, S (P x) ->
M (P x). This condition will be instantiated with the identity. But if S
and M where Types instead of Props, that would lead to a circularity in the
universes. Therefore, we need ???? to be a Prop, the same as M‘s co-domain.

Best,
Beta

[1] Mtac: A Monad for Typed Tactic Programming in Coq. B. Ziliani, D.
Dreyer, N. R. Krishnaswami, A. Nanevski, V. Vafeiadis. In Journal of
Functional Programming (JFP), Volume 25, August 2015.

On Sat, Jul 6, 2019 at 2:08 AM 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
>
>