[Agda] Proving Parametricity?

[Alan Jeffrey]

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.

A.

On 01/19/2011 10:07 AM, Brandon Moore wrote:
> I've written the following code based on Adam Chlipala's paper on
> "Parametric Higher Order Abstract Syntax". I'm wondering if there's
> any way to prove the parammetricity assumption at the end.
> It's taken as an axiom in the Coq development.
>
> module phoas where
>
> open import Data.List
> open import Data.Product
>
> data Exp (var : Set) : Set where
>    Var : var ->  Exp var
>    App : Exp var ->  Exp var ->  Exp var
>    Abs : (var ->  Exp var) ->  Exp var
>
> -- an expression is an Exp parametric in the variable type
> exp = ∀ var → Exp var
>
> -- "apply"
> example : exp
> example var = Abs (λ x → Abs (λ y → App (Var x) (Var y)))
>
> data In {A : Set} : A ->  List A ->  Set where
>    InHd : ∀ x l → In x (x ∷ l)
>    InTl : ∀ x x' l → In x l ->  In x (x' ∷ l)
>
> data Exp_related {var1 var2 : Set} :
>    (Γ : List (var1 × var2)) → Exp var1 ->  Exp var2 ->  Set where
>    Related : ∀ Γ v1 v2 → In (v1 , v2) Γ → Exp_related Γ (Var v1) (Var v2)
>    RApp : ∀ Γ e1 e2 e1' e2' → Exp_related Γ e1 e1' → Exp_related Γ e2 e2' →
>      Exp_related Γ (App e1 e2) (App e1' e2')
>    RAbs : ∀ Γ f1 f2 → (∀ v1 v2 → Exp_related ((v1 , v2) ∷ Γ) (f1 v1) (f2 v2)) →
>      Exp_related Γ (Abs f1) (Abs f2)
>
> exp_param : ∀ (e : exp) var1 var2 → Exp_related [] (e var1) (e var2)
> exp_param = {!!}
>
>
>
>
> _______________________________________________
> Agda mailing list
> Agda at lists.chalmers.se
> https://lists.chalmers.se/mailman/listinfo/agda

-------------- next part --------------
module phoas where

open import Data.List
open import Data.Product
open import Relation.Binary.PropositionalEquality

-- Surjections

_↠_ : Set → Set → Set
V ↠ W = ∃ λ (f : V → W) → ∀ w → ∃ λ v → f v ≡ w

inj : ∀ {V W} → (V ↠ W) → (V → W)
inj (f , f⁻¹) v = f v

inv : ∀ {V W} → (V ↠ W) → (W → V)
inv (f , f⁻¹) w with f⁻¹ w
inv (f , f⁻¹) w | (v , fv≡w) = v

surj : ∀ {V W} (φ : V ↠ W) (w : W) → (inj φ (inv φ w) ≡ w)
surj (f , f⁻¹) w with f⁻¹ w
surj (f , f⁻¹) w | (v , fv≡w) = fv≡w

-- Action of Exp on sets

data Exp (var : Set) : Set where
  Var : var -> Exp var
  App : Exp var -> Exp var -> Exp var
  Abs : (var -> Exp var) -> Exp var

-- Syntactic identity on exps

data _≣_ {V : Set} : Exp V → Exp V → Set where
  Var : ∀ {v₁ v₂} → (v₁ ≡ v₂) → (Var v₁ ≣ Var v₂)
  App : ∀ {f₁ f₂ e₁ e₂} → (f₁ ≣ f₂) → (e₁ ≣ e₂) → (App f₁ e₁ ≣ App f₂ e₂)
  Abs : ∀ {f₁ f₂} → (∀ v → f₁ v ≣ f₂ v) → (Abs f₁ ≣ Abs f₂)

-- Action of Exp on surjections

⟨Exp⟩ : ∀ {V W} (φ : V ↠ W) → (Exp V → Exp W)
⟨Exp⟩ φ (Var v)   = Var (inj φ v)
⟨Exp⟩ φ (App f e) = App (⟨Exp⟩ φ f) (⟨Exp⟩ φ e)
⟨Exp⟩ φ (Abs f)   = Abs (λ w → ⟨Exp⟩ φ (f (inv φ w)))

-- an expression is an Exp parametric in the variable type

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

_[_] : exp → ∀ V → Exp V
(e , f) [ V ] = e V

-- "apply"

Example : ∀ V → Exp V
Example V = Abs (λ x → Abs (λ y → App (Var x) (Var y)))

example : exp
example = (Example , λ φ → Abs (λ x → Abs (λ y → App (Var (surj φ x)) (Var (surj φ y)))))

data In {A : Set} : A -> List A -> Set where
  InHd : ∀ x l → In x (x ∷ l)
  InTl : ∀ x x' l → In x l -> In x (x' ∷ l)

data Exp_related {var1 var2 : Set} :
  (Γ : List (var1 × var2)) → Exp var1 -> Exp var2 -> Set where
  Related : ∀ Γ v1 v2 → In (v1 , v2) Γ → Exp_related Γ (Var v1) (Var v2)
  RApp : ∀ Γ e1 e2 e1' e2' → Exp_related Γ e1 e1' → Exp_related Γ e2 e2' →
    Exp_related Γ (App e1 e2) (App e1' e2')
  RAbs : ∀ Γ f1 f2 → (∀ v1 v2 → Exp_related ((v1 , v2) ∷ Γ) (f1 v1) (f2 v2)) →
    Exp_related Γ (Abs f1) (Abs f2)

-- exp_param : ∀ (e : exp) var1 var2 → Exp_related [] (e var1) (e var2)
-- exp_param = {!!}