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

```
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?

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

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

If `conj`

would be an alias for `@prod Prop`

I'd also see the case for the behaviour as implemented

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).

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.

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

https://www.cs.au.dk/~spitters/extraction.pdf

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

Ah I see, thank your very much everybody! In C-Corn extraction is done to Haskell if I understand correctly (https://github.com/coq-community/corn/blob/master/util/Extract.v#L3), so there one can actually make use of the minimising behaviour of template polymorphism.

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

Last updated: Jan 28 2023 at 06:30 UTC