Template polymorphism and extraction · Coq users

Template polymorphism chooses the least possible sort for an inductive type. For instance Check (prod True True : Prop). works perfectly fine. I thought that the reason for this choice would be extraction, otherwise placing prod True True to the least Type universe would seem more plausible to me. However,

Require Extraction.
Definition test := (I, I).
Extraction test.

Error:
The informative inductive type prod has a Prop instance
in test (or in its mutual block).
This happens when a sort-polymorphic singleton inductive type
has logical parameters, such as (I,I) : (True * True) : Prop.
The Ocaml extraction cannot handle this situation yet.
Instead, use a sort-monomorphic type such as (True /\ True)
or extract to Haskell.

So is the historic reason for the template polymorphism rule allowing prod True True : Prop to make extraction to Haskell work, or is there some reason not related to extraction as well?

Matthieu Sozeau (May 21 2021 at 11:30):

I guess the motivation was rather to let users mix Type and Prop in conjunctions easily, and it broke extraction. But @Hugo Herbelin might have a more precise recollection of why it was allowed

Yannick Forster (May 21 2021 at 12:18):

Thanks for the answer :) Just mixing would also work if the lowest universe for template polymorphism would be in Type, because Prop is included in Type, no? So the difference is that in such a free mix, one might end up with a Prop in some restricted cases

Yannick Forster (May 21 2021 at 12:19):

If conj would be an alias for @prod Prop I'd also see the case for the behaviour as implemented

Hugo Herbelin (May 25 2021 at 21:33):

Hi, the original motivation was for CoRN which was formalising logic mathematics in prod and (for some reason I don't remember) wanted it to land in Prop whenever possible.

Model-theoretically, and is a particular case of prod, so there are no internal reasons to have them different (like sum, sumor, sumbool, or sigT and sig). It is the way to think at them which makes that want them to be different (computation vs logic).

Regarding extraction not supporting Prop/Type-polymorphism, I suspect that it is similar to the nat->X mismatch we can have when X is lately instantiated by True, as in:

Definition f {X} (h:nat->X)(g:X->nat) := g (h 0).
Definition k := f (fun _ => I) (fun _ => 0).

which extracts to let f h g = g (h O) in f (Obj.magic __) (fun _ -> O) and which works at runtime only because __ is actually the function fun _ => fun _ => ... taking an arbitrary large number of arguments.

The mismatch could be fixed by adjusting a term in some type in Prop (here nat->True) to the expected type (here (((nat->X):Type)[X:=True]):Prop, extracting instead to let f h g = g (h O) in f (fun _ => __) (fun _ -> O). I suspect the same thing can be done for template polymorphism but I did not explore further (see #13486 for the start of a discussion).

Pierre-Marie Pédrot (May 26 2021 at 07:52):

Hmm, this is not true in the Set model though. In the first case you need to squash to remain a singleton, but in the second you have a real product.

Bas Spitters (May 26 2021 at 08:46):

The prod of two hProps is again an hProp, is I think related to what Hugo is pointing too.

Stream: Coq users

Topic: Template polymorphism and extraction

Yannick Forster (May 17 2021 at 18:26):