On 1/27/12 7:56 PM, Ryan Ingram wrote:
Thus, you can in principle define plenty of natural transformations which do not have the type f :: forall X. M X -> N X.
Can you suggest one? I don't see how you can get around f needing to act at multiple types since it can occur before and after g's fmap:
Right. A natural transformation is a family of functions (one for each type). My point was, "forall" is one way of defining a family of functions, but it's not the only one. For instance, we could use a type class, or some fancy generics library, or a non-parametric forall in languages which allow type-case. Or we could use some way of defining it which is outside of the language in which the component functions exist. For example, consider the simply typed lambda calculus. STLC doesn't have quantifiers so we can't define (f :: forall X. M X -> N X) as a natural transformation from within the language, but we could still talk about the family of simply-typed functions { f_X :: M X -> N X | X <- type }. Calling a family of functions a natural transformation is an extralinguistic statement about the functions; there are, in general, more natural transformations than can be defined from within the language in question. Just as there are, in general, more endofunctors than can be defined within the language (let alone other functors). The "naturality" behind natural transformations is just the fact that (forall g, fmap g . f = f . fmap g). Satisfying the equation means that the family of fs is "parametric enough", regardless of how we've defined the family or how/whether we can implement the family as polymorphism within the language. -- Live well, ~wren