The Coq mailing list

[Daniel Schepler <dschepler AT gmail.com>]

On Wednesday 30 March 2011 07:13:22 David Baelde wrote:
> 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,

No, if you add

Axiom classic_dec: forall P:Prop, {P} + {~P}.

then you can define

Definition inhabited_bool (A:Type) : bool :=
  if classic_dec (inhabited A) then true else false.

That's clearly not constant, but classic_dec is consistent (in fact, it's 
easy 
to prove from classic and constructive_definite_description).
-- 
Daniel Schepler