The Coq mailing list

[David Baelde <david.baelde AT gmail.com>]

Hi list,

We (at ProVal) were wondering to which extent Coq is tied to
parametric polymorphism.

There is certainly no way to define a non-parametric function in Coq.
For example, any function of type (forall A:Type, A -> bool) must be
equal (at least extensively) to a constant function. It also seems
that there is no model of (subsets) of the CIC that doesn't force
parametricity. But do we know whether this is ruled out by the
calculus itself? In other words, can we prove from inside Coq that any
function of type (forall A:Type, A -> bool) is extensively equal to
some constant function?

Any pointers related to that topic would be appreciated.

Thanks,
-- 
David