The Coq mailing list

[Yves Bertot <Yves.Bertot AT sophia.inria.fr>]

JAEGER, Eric (SGDN) wrote:
> > Variable var : Type.
> > Inductive test : Type :=
> > | A : var -> test
> > | B : test.
> > Goal forall T (f : T -> test) x y v, f x = A v -> exists v', f y = A v'.
>
> Sorry, but I do not understand either. Nothing prevents f to return B 
> for some y, even once you have exhibited a value x such that f x=A v. 
> In such a case your goal appears false.
>
> By the way, f var x=A v proves that var is not empty only if you 
> assume that T is not (but I agree that if T is empty then your goal is 
> trivially true).
>
>    Regards, Eric
I believe Taral wants to find a generic condition to impose on f that 
would ensure the goal he has in mind.  Somehow like Girard's idea, when 
studying second-order lambda-calculus, to say that polymorphic functions 
cannot be arbitrary and that the "meaning" of  a polymorphic type is the 
intersection of all possible meanings for instances the polymorphic 
parameter, instead of the reunion.  Just to explain the previous 
sentence in an example, there can be only one polymorphic function of 
type forall A:type,  A -> A, and this function is necessarily the 
identity function (you have to find the intersection of unit -> unit, 
nat -> nat, Z -> Z, bool -> bool, they all contain the identity function 
and it is the only function --or behavior-- that can be common to these 
types), because the behavior cannot depend on the specific structure of 
specific instances of A.  I believe this is what is meant by 
"parametricity".

Now, representing polymorphism by universal quantification does not 
provide this property because, as was rightly pointed out by everybody 
but Taral, you can always instantiate universal quantification in weird 
ways.  However none of these instantiations  falls in the 
"intersection".  So the problem could be re-phrased in: what is the 
condition that can be expressed on "f" that rejects all the weird instances?

Now, even if I believe I understood Taral's question, I still don't see 
how to answer it.  I don't see a way to express (inside Coq) that some 
function is at the same time in (nat -> nat) and in (Z -> Z).  You 
cannot speak about the function itself (each function basically has a 
single type and in some sense the types nat -> nat  and Z -> Z have an 
empty intersection), but about its "behavior", which should be some 
untyped information and can be shared with other functions in other 
types... 

I am not sure this helps,  but I still hope,

Yves