CODEWITHSUNDEEP
agdaparametric-polymorphismfree-theorem
Cactus
Cactus

Reputation: 27626

Parametricity-exploiting proofs in Agda

Reading this answer prompted me to try to construct, and then prove, the canonical form of polymorphic container functions. The construction was straightforward, but the proof stumps me. Below is a simplified-minimized version of how I tried to write the proof.

The simplified version is proving that sufficiently polymorphic functions, due to parametricity, can't change their behaviour only based on the choice of parameter. Let's say we have functions of two arguments, one of a fixed type and one parametric:

PolyFun : Set → Set _
PolyFun A = ∀ {X : Set} → A → X → A

the property I'd like to prove:

open import Relation.Binary.PropositionalEquality

parametricity : ∀ {A X Y} → (f : PolyFun A) → ∀ a x y → f {X} a x ≡ f {Y} a y
parametricity f a x y = {!!}

Are statements like that provable from inside Agda?

Upvotes: 3

Views: 358

Answers (1)

Saizan
Saizan

Reputation: 1401

Nope, there's no parametricity principle accessible in Agda (yet! [1]).

However you can use these combinators to build the type of the corresponding free theorem and postulate it:

http://wiki.portal.chalmers.se/agda/pmwiki.php?n=Libraries.LightweightFreeTheorems

[1] http://www.cse.chalmers.se/~mouling/share/PresheafModelParametericTT.pdf

Upvotes: 6

Related Questions