3

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?

Community
  • 1
  • 1
Cactus
  • 27,075
  • 9
  • 69
  • 149

1 Answers1

6

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

Saizan
  • 1,391
  • 8
  • 4
  • Do you have a good real-life example of using that LFT library from your link? I tried using it to prove `parametricity`, but it's not at all obvious to me how the LFT-derived free theorem of my function type is useful here. My code is at https://gist.github.com/gergoerdi/0bedc9185cdeae7216f5 – Cactus Dec 23 '15 at 06:55
  • 2
    Oh, you're not polymorphic on A, that makes it harder, otherwise you could've taken [A] to be the equality. LFT lacks the identity extension lemma so in the abstract you can often only show that things are related, not equal. For a concrete type like Bool you can witness that [Bool] is actually equality though. For (A : Set0) it should be consistent to assume that [A] is equality though, see http://bentnib.org/dtt-parametricity.html – Saizan Dec 24 '15 at 07:50
  • The link [1] is now dead; paper can still be found at http://publications.lib.chalmers.se/records/fulltext/230735/local_230735.pdf – Jacques Carette Sep 08 '19 at 12:26