tag:blogger.com,1999:blog-11295132.post361364758521479897..comments2014-08-17T09:30:19.334-07:00Comments on A Neighborhood of Infinity: Products, Limits and Parametric PolymorphismDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger18125tag:blogger.com,1999:blog-11295132.post-74541780535847766372010-09-13T09:54:48.976-07:002010-09-13T09:54:48.976-07:00You all should have a look at Plotkin, Abadi. &quo...You all should have a look at <a href="http://www.springerlink.com/content/b72q837257g186v4" rel="nofollow">Plotkin, Abadi. "A logic for parametric polymorphism", TLCA 1993</a>.<br /><br />Although it has no diagrams, all the constructions are essentially categorical. And the free theorem for existentials is at the bottom of p. 11 below Thm 7—see the brief paragraph broken over pp. 11–12.<br /><br />Moreover, this paper finally enabled me to understand parametricity (i.e. Reynolds' "Abstraction Theorem", which Wadler renamed the "Parametricity Theorem"). Only after reading Plotkin and Abadi was I able to make sense of Reynolds' original papers and Wadler's follow up. In case anyone finds it helpful, I also have an <a href="http://www.ccs.neu.edu/home/matthias/369-s10/Transcript/parametricity.pdf" rel="nofollow">annotated bibliography for these papers</a> from a course last spring.Daniel Brownhttp://www.blogger.com/profile/04010336152800558441noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-28996994855948248442010-03-11T07:08:40.761-08:002010-03-11T07:08:40.761-08:00Dan, restricting yourself to the functional specia...Dan, restricting yourself to the functional specialization of the free theorems is slowing you down.<br /><br />The free theorem for (1) is (2), which can indeed be specialized to (3) by instantiating R as in (4). But if you instead let R be always satisfied, as in (5), you immediately get (6), a proof that c always returns the same value.<br /><br />(1) c : forall a. a → R<br />(2) c# : forall X Y R<br /> → (x : X)<br /> → (y : X)<br /> → R x y<br /> → c x == c y<br />(3) c#' : forall X Y f<br /> → (x : X)<br /> → c x == c (f x)<br />(4) R x y = (f x == y)<br />(5) R x y = true<br />(6) c#'' : forall X Y<br /> → (x : X)<br /> → (y : Y)<br /> → c x == c y<br /><br /><br />The second type (7) you state also guarantees that results are always the same, but as you have noticed, the functional specialization (9) of its free theorem (8) hides this fact behind an assumption. If you once again let R be always satisfied, as in (5), you easily obtain (10), a proof that d always returns the same value.<br /><br />(7) d : forall a. (a → a) → R<br />(8) d# : forall X Y R<br /> → (fx : X → X)<br /> → (fy : Y → Y)<br /> → (f# : forall x y → R x y → R (fx x) (fy y))<br /> → d fx == d fy<br />(9) d#' : forall X Y f<br /> → (fx : X → X)<br /> → (fy : Y → Y)<br /> → (f# : forall x → f (fx x) == fy (f x))<br /> → d fx == d fy<br />(10) d#'' : forall X Y<br /> → (fx : X → X)<br /> → (fy : Y → Y)<br /> → d fx == d fygelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-30797846900175784152010-03-10T16:46:47.275-08:002010-03-10T16:46:47.275-08:00I guess the interesting properties of existentials...I guess the interesting properties of existentials may be related to free theorems about their 'constructors'. For instance, one likes to think of (exists a. a) as isomorphic to the unit type. And the free theorem for:<br /><br />c :: forall a. a -> R<br /><br />is c = c . f, which if we take f to be of the form 'const y', can turn into<br /><br />forall x, y. c x = c y<br /><br />which, if c is the 'constructor' for exists a. a, states that all elements of that type are equal.<br /><br />forall a. (a -> a) -> R<br /><br />comes with a similar theorem, although it has a precondition that might limit it from saying that all elements are equal (I'm not really sure).Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-74186685570039998572010-03-10T14:37:59.115-08:002010-03-10T14:37:59.115-08:00Yes, I'd got as far as realizing these were th...Yes, I'd got as far as realizing these were theorems for the constructor type. But when I used the free theorem generator I was using it was taking me a long time to interpret the result. I just tried @free on #haskell and I'm finding it much easier to parse the result. I'll have to install the underlying generator.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-27759014033961340892010-03-10T14:31:59.101-08:002010-03-10T14:31:59.101-08:00I need to distinguish the A type from the A constr...I need to distinguish the A type from the A constructor, so let me give them distinct names.<br /><br />data T = forall a. C (a, a->Z)<br /><br />The theorem you gave is the free theorem for C, not T. The fact that T is an existential type plays no role in the derivation of the free theorem, since the type of C begins with a universal quantifier. If it is theorems like the one you gave which you want to derive, it suffices to follow the technique given in Wadler's paper, treating T as a constant type.<br /><br />For example, here is how to derive the theorem you gave using parametricity.<br /><br />The free theorem for (1) is (2), which can be specialized to the theorem you gave, (3), by instantiating R as in (4).<br /><br />(1) C : forall a. (a, a→Z) → T<br />(2) C# : forall X Y R<br /> → (x : X)<br /> → (y : Y)<br /> → R x y<br /> → (zx : X→Z)<br /> → (zy : Y→Z)<br /> → (forall u v → R u v → zx u == zy v)<br /> → C (x, zx) == C (y, zy)<br />(3) C#' : forall X Y R<br /> → (x : X)<br /> → (zy : Y→Z)<br /> → C (x, zy . f) == C (f x, zy)<br />(4) R x y = (f x == y)gelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-231689605950333072010-03-10T14:28:13.265-08:002010-03-10T14:28:13.265-08:00I still have a rudimentary understanding of free t...I still have a rudimentary understanding of free theorems. However, if you ask lambdabot for the free theorem for my encoding:<br /><br />ep : forall r. (forall a. a -> (a -> Z) -> r) -> r<br /><br />you get back:<br /><br />(forall g z h. f (x z (h . g)) = y (g z) h) => f (ep x) = ep y<br /><br />which obviously has something similar to your interchange in there (x z (h . g) vs. y (g z) h).<br /><br />But, really, your theorem is probably about the constructor, or whatever operation you want to call it, for putting things in an existential box. Thus we should probably look at:<br /><br />econ :: forall t. t -> (t -> Z)<br />-> (forall r. (forall a. a -> (a -> Z) -> r) -> r)<br /><br />And what @free spits back at us is:<br /><br />(forall k u p. h (y u (p . k)) = z (k u) p)<br />=> h (econ x (g . f) y) = econ (f x) g z<br /><br />But, if we ask for the free theorem of:<br /><br />z :: forall a. a -> (a -> Z) -> R<br /><br />we get:<br /><br />z x (g . f) = z (f x) g<br /><br />Which means that we can choose h = id and y = z in the free theorem for econ, giving:<br /><br />forall z. econ x (g . f) z = econ (f x) g z<br /><br />And then by extensionality, we get:<br /><br />econ x (g . f) = econ (f x) g<br /><br />So it turns out your theorem isn't as general as possible, I guess. But we've done it. :)Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31808964522702420322010-03-10T14:08:03.328-08:002010-03-10T14:08:03.328-08:00@Dan: The free theorem for () is that () == (). Th...@Dan: The free theorem for () is that () == (). This is because constant types, like Bool and (), are read as identity relations, which are only satisfied when both arguments are equal (see Wadler's paper, page 5, first paragraph).gelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-91371356597959933742010-03-10T13:32:44.949-08:002010-03-10T13:32:44.949-08:00Dan,
So can you derive that theorem about ∃a.(a,a...Dan,<br /><br />So can you derive that theorem about ∃a.(a,a->Z) from the free theorem theorem?<br /><br />I think these theorems for existentials are non-trivial and useful. They encode the folk knowledge that if a type is hidden behind an interface, and you can replace the type with an isomorphic one, people in front of the interface won't be able to tell. The free theorem theorem should tell you the precise meaning of 'isomorphism' for each type. (Actually, it doesn't have to be an *iso*morphism, just a morphism that doesn't lose too much information.)sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-47166956962022033472010-03-10T13:06:09.026-08:002010-03-10T13:06:09.026-08:00(Sorry for the double comment.)
Oh! I see what yo...(Sorry for the double comment.)<br /><br />Oh! I see what you're saying. You're saying that for:<br /><br />f : X -> Y<br />g : Y -> Z<br />a : X<br /><br />(f a, g) = (a, g . f) as existentials.<br /><br />Yes, I can believe this.Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-60881877155563376852010-03-10T12:51:47.207-08:002010-03-10T12:51:47.207-08:00Are you sure that's a theorem? If f : X -> ...Are you sure that's a theorem? If f : X -> Y, it seems to me we can't possibly use it with (a, g) : exists a. (a, a -> Z) because:<br /><br />1) We don't know if a = X, Y or something else entirely.<br />2) Even if we did, then<br /><br />(f a, g) : (Y, X -> Z) (in the a = X case)<br />(a, g . f) : (Y, X -> Z) (in the a = Y case)<br /><br />Neither of which has the right type to be exists a. (a, a -> Z). And in the other two combinations of rules with instantiations of the variable, there are just straight-forward type errors.<br /><br />I could believe something like:<br /><br />f : forall a. a -> a<br /><br />(f a, g) = (a, g . f)<br /><br />Perhaps this can even be derived in a roundabout way from the free theorem for<br /><br />forall r. (forall a. a -> (a -> Z) -> r) -> r.<br /><br />All that said, I don't think it's surprising that a type like 'exists a. a -> a' doesn't have an interesting free theorem. That type is isomorphic to the unit type. What is the free theorem for ()?Dan Doelhttp://www.blogger.com/profile/16761291400347369301noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-69890222583055189922010-03-10T09:20:00.740-08:002010-03-10T09:20:00.740-08:00Consider
data A = forall a. A (a, a->Z)
Then ...Consider<br /><br />data A = forall a. A (a, a->Z)<br /><br />Then we have that for all f:X -> Y,<br /><br />A (f a, g) = A (a, g . f)<br /><br />This is a non-trivial theorem (in the form of a universally quantified proposition) about an existential type.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-28200146047765237212010-03-09T22:55:18.193-08:002010-03-09T22:55:18.193-08:00This comment has been removed by the author.gelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-31480662056628031552010-03-09T22:02:48.847-08:002010-03-09T22:02:48.847-08:00Wait a minute; it's even worse than I thought....Wait a minute; it's even worse than I thought. We're not free to functionalize the relation since all we know is that there exists <i>some</i> relation such that so and so. Here is a detailed example of the mistake.<br /><br />The free theorem for (1) is (2), which we can specialize to (3) by instantiating R as in (4).<br /><br />(1) id : ∀ A → (A → A)<br />(2) id~ : ∀ X Y R<br /> → (x : X)<br /> → (y : Y)<br /> → R x y<br /> → R (id x) (id y)<br />(3) id~' : ∀ X Y<br /> → (f : X → Y)<br /> → (x : X)<br /> → (y : Y)<br /> → f (id x) == id (f x)<br />(4) R x y = (f x == y)<br /><br />But the free theorem for (5) is (6), which we can <i>not</i> specialize to (7) by instantiating R as in (4).<br /><br />(5) i : ∃ A → (A → A)<br />(6) i~ : ∃ X Y R<br /> → (x : X)<br /> → (y : Y)<br /> → R x y<br /> → R (id x) (id y)<br />(7) i~' : ∃ X Y f<br /> → (x : X)<br /> → (y : Y)<br /> → f (i x) == i (f x)gelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-9911834904740303452010-03-09T16:04:28.868-08:002010-03-09T16:04:28.868-08:00gelisam,
A nice example that illustrates what I&#...gelisam,<br /><br />A nice example that illustrates what I'm talking about. Try guessing the free theorem for<br /><br />exists a. (a, a -> a, a -> X)<br /><br />where X is a fixed type of your choosing.<br /><br />Or try<br /><br />exists a. ([a], a -> a -> a, a -> X).sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-87604319943518494102010-03-09T16:01:06.846-08:002010-03-09T16:01:06.846-08:00I've already guessed the free theorems for tho...I've already guessed the free theorems for those cases. A more interesting case is exists a.(a->X, F a) for functor F which I mentioned in my coend post. It gets more interesting for exists a.X a where X is an interesting algebraic structure of some sort.<br /><br />In each case, I have a handwavey argument for what the free theorem should be. But I haven't derived them formally yet.<br /><br />In some cases I think they are useful but they encode knowledge about the notion of an abstract interface that object oriented programmers already informally use.<br /><br />When I work out a rigorous and simple derivation I'll write about it.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-17121837478452152162010-03-09T15:51:24.826-08:002010-03-09T15:51:24.826-08:00Free theorems for existential types, at your servi...Free theorems for existential types, at your service.<br /><br />Suppose i has type (∃a. a → a). For example, it might be (+1), or (++"foo"). Then there exists a function f of type X → Y, for some types X and Y, such that f (i x) == i (f x). f = id, for example, does the trick.<br /><br />Similarly, suppose xs has type (∃a. [a]). For example, it might be [1, 2, 3], or ["foo", "bar"]. Then there exists a function f of type X → Y, for some types X and Y, such that fmap f xs == xs. f = id, for example, does the trick.<br /><br />All in all, free theorems for existential types don't seem that useful (so far).gelisamhttp://www.blogger.com/profile/10619127479176568208noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-46867900326231785782010-03-07T16:24:04.926-08:002010-03-07T16:24:04.926-08:00Janis Voigtländer pointed me to Types, abstraction...Janis Voigtländer pointed me to <a href="http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.39.6996" rel="nofollow">Types, abstraction, and parametric polymorphism, part 2</a> that might be just what I am after.sigfpehttp://www.blogger.com/profile/08096190433222340957noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-82839311331796058842010-03-07T16:07:40.325-08:002010-03-07T16:07:40.325-08:00There's an easy and direct way to prove that ∀...There's an easy and direct way to prove that ∀a.F(a) is the limit.<br /><br />We can describe cones in a nicely categorical way as simply natural transformations.<br /><br />A cone N over the functor F is the same thing as a natural transformation, KN → F where KN is the constantly N functor. Now L is a limit of a functor F, if Hom(-,L) ~ Nat(K-,F), which is to say, if L represents the cone functor. This can be shown to be equivalent to the definition of limit in your post.<br /><br />Nat(K-,F) is ∀a.K b a → f a or just ∀a.b → f a in Haskell. Then, essentially by continuity of Hom or by continuity of right adjoints, we can move the ∀ inwards and get: b → ∀a.f a, which, by Yoneda, means L is isomorphic to ∀a.f a. A similar manipulation can be done for colimits, and indeed, this was how Kan extensions, (co)ends, and (co)limits were derived for category-extras.Derek Elkinshttp://www.blogger.com/profile/13447153951050085981noreply@blogger.com