The Coq mailing list

[Matthieu Sozeau <Matthieu.Sozeau AT lri.fr>]

Hi everyone,

Le 19 nov. 08 à 09:32, Yves Bertot a écrit :

> 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,


It can be characterized in a way by saying that the function preserves  
any relation
between two arguments, e.g. for the polymorphic identity:
[forall (A : Type) (R : relation A), forall x y, R x y -> R (id x) (id  
y)]
Equivalently, you could say (using some new definitions found in  
Classes/Morphisms)
[forall A (R : relation A), Morphism (R ==> R) (@id A)] which unfolds  
to the same
statement.

In the particular example with [f : forall T, T -> Test], you would  
need the condition
[forall T (RT : relation T), Morphism (RT ==> eq) f].
By instantiating this with the trivial relation (fun x y : T, True),  
you get that
[forall x y, f T x = f T y].
I believe this is not provable for any variable [f] of type [forall T,  
T -> Test] but
by a parametricity theorem any instance for some concrete [f] should  
be derivable.
This characterization as relational parametricity goes back to  
Wadler's "Theorems for free!"
and possibly Reynolds and Girard as well. I don't know if it's been  
studied in the
particular setting of the Inductive Constructions though, but there  
ought to be
a similar meta-theorem. I hope someone more knowledgable on the  
metatheory can clear
it out!

Hope this helps,
-- Matthieu