tag:blogger.com,1999:blog-11295132.post2692688231726616322..comments2017-09-12T07:32:15.175-07:00Comments on A Neighborhood of Infinity: A Yonedic AddendumDan Piponihttps://plus.google.com/107913314994758123748noreply@blogger.comBlogger3125tag:blogger.com,1999:blog-11295132.post-66864292465437075642007-02-12T20:55:00.000-08:002007-02-12T20:55:00.000-08:00But Theorems for Free! also talks about functions ...<I>But Theorems for Free! also talks about functions that don't look like natural transformations. For example consider the type (a->a)->(a->a). The free theorem reflects the fact that any such function must simply raise its argument to some non-negative integer power. But it seems to me that when the free theorem is written in point-free style, then functions (ie. functions that map objects to arrows like the way natural transformations do) in a general category that satisfy this theorem are also in some sense 'natural'. So is there a wider sense of 'natural' in a category that I should know about?</I><BR/><BR/>Since the type variable occurs both covariantly and contravariantly a natural transformation is inappropriate (the functors would have to be both covariant and contravariant at the same time). Instead you may want to look at dinaturality, <A HREF="http://www.tac.mta.ca/tac/reprints/articles/10/tr10abs.html" REL="nofollow">Basic Concepts of Enriched Categories</A> is the best source of information (online) about them I'm aware of. It also covers indexed (co)limits, an unreasonably under-represented tool (and also (co)ends).<BR/><BR/>Dinaturality, or perhaps a special case of it, is often referred to as extraordinary naturality.Derek Elkinsnoreply@blogger.comtag:blogger.com,1999:blog-11295132.post-61468124840148037872006-12-04T17:30:00.000-08:002006-12-04T17:30:00.000-08:00For what it's worth, you can work out free theorem...For what it's worth, you can work out free theorems for arbitrary functors using the other one in lambdabot. It goes to a lot of trouble to make the theorems as point-free as possible.<br /><br />So in your example:<br /><br /><b>h1 (f1 x2) = g1 x2 => h1 (t1 f1 x1) = t1 g1 x1</b><br /><br />can be simplified by noting that the "if" part of the implication merely says that <b>g1 = h1 . f1</b>. And so, dropping the 1's:<br /><br /><b>h . t f = t (h . f)</b><br /><br />Setting <b>f = id</b> gives you the theorem.<br /><br />The free theorem for <b>test :: (C -> a) -> F a</b> is:<br /><br /><b>fmap f . test = test . (.) f</b><br /><br />This should be unsurprising, because <b>(.) f</b> is <b>fmap f</b> in the functor <b>((->) C)</b>. Once again, all this says is that <b>test</b> is a natural transformation.<br /><br />Applying <b>id</b> to both sides gives:<br /><br /><b>fmap f (test id) = test . f</b><br /><br />And a little rearrangement gives you the result you're after.<br /><br />As to your second question, about <b>(a->a) -> (a->a)</b>, it's not a mapping between functors, but it is a mapping between natural transformations! I haven't looked too hard into it, but I suspect that the free theorem for this is a consequence of whatever the obvious mapping property of these "supernatural transformations" would look be.<br /><br />There's another way to look at it, but you'll have to read my article in the next Monad.Reader to find out.Andrewhttps://www.blogger.com/profile/04272326070593532463noreply@blogger.comtag:blogger.com,1999:blog-11295132.post-14254454930004664672006-12-03T06:04:00.000-08:002006-12-03T06:04:00.000-08:00I really enjoy reading your blog. I was wondering ...I really enjoy reading your blog. I was wondering if you would consider writing something for the recently revived <a href=http://www.haskell.org/haskellwiki/TheMonadReader> Monad.Reader</a>. A lot of your blog posts could make great articles with a bit of polishing! Get in touch if you're interested,<br /><br /> <a href=http://www.cs.nott.ac.uk/~wss>Wouter Swierstra</a><br /><br />PS - As far as variable substitution is concerned, you might be interested in free monads - which are basically the same construction you described in your blog post. For some reason, they aren't very well-known in the functional programming community.Wouterhttps://www.blogger.com/profile/14457659882674009379noreply@blogger.com