Hi,
I've discovered the following post on the internets: http://gelisam.blogspot.com/2009/09/samuels-really-straightforward-proof-of.html It contains an ingenious (to my mind) encoding of parametricity in Agda that makes the Free Theorems a trivial consequence. I've tried to formalize it in Coq, but, as of now, with no success. -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <[hidden email]> wrote:
> It contains an ingenious (to my mind) encoding of parametricity in > Agda that makes the Free Theorems a trivial consequence. Perhaps I don't understand Agda very well, but I don't see parametricity here. For one, there's no attempt to prove that: forall (P Q : forall a, a -> a), P = Q. which is what parametricity means to me. -- Taral <[hidden email]> "Please let me know if there's any further trouble I can give you." -- Unknown _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Under parametricity, I mean the Reynolds Abstraction Theorem, from
which free theorems follow. The encoding allows one to prove the theorem for any particular function by implementing this function in terms of "relativized" types. The type of the relativized function is precisely an instance of Reynolds theorem for it, and its implementation is a proof. 2009/9/23 Taral <[hidden email]>: > On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <[hidden email]> wrote: >> It contains an ingenious (to my mind) encoding of parametricity in >> Agda that makes the Free Theorems a trivial consequence. > > Perhaps I don't understand Agda very well, but I don't see > parametricity here. For one, there's no attempt to prove that: > > forall (P Q : forall a, a -> a), P = Q. > > which is what parametricity means to me. > > -- > Taral <[hidden email]> > "Please let me know if there's any further trouble I can give you." > -- Unknown > -- Eugene Kirpichov Web IR developer, market.yandex.ru _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Taral
On Wednesday 23 September 2009 12:21:00 pm Taral wrote:
> On Wed, Sep 23, 2009 at 6:46 AM, Eugene Kirpichov <[hidden email]> wrote: > > It contains an ingenious (to my mind) encoding of parametricity in > > Agda that makes the Free Theorems a trivial consequence. > > Perhaps I don't understand Agda very well, but I don't see > parametricity here. For one, there's no attempt to prove that: > > forall (P Q : forall a, a -> a), P = Q. > > which is what parametricity means to me. I've been playing with this, and the stuff in the post takes a bit of work to fully tease out. Working through the Theorems for Free paper along side the blog post should be helpful, but here's a fast version: ∀ A. A → A goes like: From a function from relations to relations Φ we get relations ∀α. Φ(α) where (φ, φ') ∈ ∀α. Φ(α) iff (A, A') ∈ α ⟶ (φ(A) , φ'(A')) ∈ Φ(R_A) or something close to that. And (f, f') ∈ α → α iff (x,x') ∈ α ⟶ (f x, f' x') ∈ α Parametricity states that: if f : ∀A. A → A then (f,f) ∈ ∀α. α → α And Theorems for Free goes on to suggest that using functions as the relations between two types gives us useful theorems. All together, this looks like: id : ∀A. A → A (id,id) ∈ ∀α. α → α (parametricity) suppose f : B → C (id_B, id_C) ∈ f → f (definition of the ∀ relation above) (x,f x) ∈ f (functions as a relation) (id_B x, id_C (f x)) ∈ f (definition of the → relation above) f (id_B x) ≡ id_C (f x) (functions as a relation) which, cleaning up a bit gives: f ∘ id ≡ id ∘ f the free theorem for id : ∀A. A → A So, that's how things are supposed to go (hopefully I got that roughly correct. I get a bit muddled with the types vs. relations on types and functions on both and whatnot). However, I don't think that Agda quite allows us to do all this. We can lift a function to one of these relations fine: record Set# : Set₁ where field A : Set A' : Set A~ : A → A' → Set record value# (A# : Set#) : Set where open Set# A# field x : A x' : A' x~ : A~ x x' Rel : ∀{A B : Set} → (f : A → B) → A → B → Set Rel f x y = f x ≡ y infix 40 _# _# : ∀{A B} → (A → B) → Set# _# {A} {B} f = record { A = A ; A' = B ; A~ = Rel f } _#'_ : ∀{A B} (f : A → B) → A → value# (f #) f #' x = record { x = x ; x' = f x ; x~ = refl } But, what about parametricity? I'll define an alias for the relation of the type for identity: ∀A,A→A# : Set₁ ∀A,A→A# = (A# : Set#) → value# A# → value# A# parametricity : (∀(A : Set) → A → A) → ∀A,A→A# parametricity id A# x# = record { x = id (Set#.A A#) (value#.x x#) ; x' = id (Set#.A' A#) (value#.x' x#) ; x~ = ? } I don't think there's anything to be filled in for that ? unless we use some postulates. We can do it for 'id A x = x', but that's a specific function (which happens to be the only function with that type, but I don't think we can prove that), and the point of parametricity (I think) is that it gives us this fact for every function, based only on the type. However, if we do take it as a postulate, we seem to be good to go: postulate param : ∀{B C} {x : B} {y : C} (_~_ : B → C → Set) → (id : (A : Set) → A → A) → x ~ y → id B x ~ id C y parametricity : (∀(A : Set) → A → A) → ∀A,A→A# parametricity id A# x# = record { x = id (Set#.A A#) (value#.x x#) ; x' = id (Set#.A' A#) (value#.x' x#) ; x~ = param (Set#.A~ A#) id (value#.x~ x#) } module Free-id {A B : Set} (id# : ∀A,A→A#) (f : A → B) where -- (id,id') ∈ ∀α. α ⟶ α -- (x,y) ∈ f : A → B f x ≡ y -- (id A x, id' B y) ∈ f f (id x) ≡ id' (f x) -- id# = (id,id') -- f #' x = (x, y) -- id# (f #' x) = (id A x, id' B y) free : A → value# (f #) free x = id# (f #) (f #' x) free' : (x : A) → _ free' x = value#.x~ (free x) free : ∀{B C} (f : B → C) (id : ∀ A → A → A) → (x : B) → f (id B x) ≡ id C (f x) free f id x = Free-id.free' id# f x where id# : ∀A,A→A# id# = parametricity id voila! Of course, I took parametricity for only one fairly specific type. I'm not sure how to make it much more general, so one may have to end up taking quite a lot of postulates if one wants to work this way (or work in a language that actually has/lets you prove parametricity). Hopefully I didn't steal the author's thunder too much. Cheers, -- Dan _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
In reply to this post by Eugene Kirpichov
Hi Taral, Eugene,
[Taral] >> Perhaps I don't understand Agda very well, but I don't see >> parametricity here. For one, there's no attempt to prove that: >> >> forall (P Q : forall a, a -> a), P = Q. [Eugene] > Under parametricity, I mean the Reynolds Abstraction Theorem, from > which free theorems follow. Would it help to say that the Abstraction Theorem states that every *definable* function is parametric, whereas Taral's formula states that *every* function of that type is parametric? (Both concepts are useful; Agda presumably has models where Taral's formula does not hold (if it's consistent, i.e. has models at all), so that formula presumably isn't provable in Agda without additional axioms.) All the best, - Benja _______________________________________________ Haskell-Cafe mailing list [hidden email] http://www.haskell.org/mailman/listinfo/haskell-cafe |
Free forum by Nabble | Edit this page |