[Agda] Proving Parametricity?

[Brandon Moore]

On Jan 19, 2011, at 11:43 AM, Alan Jeffrey <ajeffrey at bell-labs.com> wrote:

Funny you should mention this, I've been emailing Adam on this very topic...

My back-of-envelope thought is that a form of naturality might do the trick, that is rather than defining exp to be:

 exp = ∀ var → Exp var

we define it as:

 exp = ∃ λ e → ∀ {V W} (φ : V ↠ W) → (⟨Exp⟩ φ (e V) ≣ e W)

where V ↠ W  is the type of surjections from V to W, and ⟨Exp⟩ is the functorial action of Exp.  Code attached.

I don't think this is enough to prove exp_param, but something like it might go through.


You could certainly write a similar exp where the property in the sigma is based on a relation rather than a surjection. I don't know how to go about constructing values in this type.

One thing I tried was making another expression type using DeBruijn indices, parameterized by the number of free variables. Given a vector of variables for context this can be converted to an Exp over the same variable type, and it's clearly provable that any polymorphic Exp constructed that way has your naturally property. Unfortunately, in Agda it seems you have to provide the corresponding DeBruijn term manually, and in Coq that can be automated but it's such a huge pain inverting a (v : vec A (S n)) into a cons that I haven't finished the lemma.

Brandon. 


      
-------------- next part --------------
An HTML attachment was scrubbed...
URL: http://lists.chalmers.se/pipermail/agda/attachments/20110119/e0325a78/attachment.html