Stream: Coq users

Topic: Template polymorphism and extraction

view this post on Zulip Yannick Forster (May 17 2021 at 18:26):

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.

fails with

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?

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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

view this post on Zulip 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).

view this post on Zulip Pierre-Marie Pédrot (May 26 2021 at 07:52):

Model-theoretically, and is a particular case of prod

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.

view this post on Zulip Bas Spitters (May 26 2021 at 08:46):

The reasons are to extract smaller programs. This was introduced in our paper with Luis

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

view this post on Zulip Yannick Forster (May 26 2021 at 12:28):

Ah I see, thank your very much everybody! In C-Corn extraction is done to Haskell if I understand correctly (, so there one can actually make use of the minimising behaviour of template polymorphism.

view this post on Zulip Bas Spitters (May 26 2021 at 12:46):

@Yannick Forster yes, we targeted haskell, but we've also used ocaml, IIRC.

Last updated: Jun 18 2024 at 22:01 UTC